Theory Conditional_Transfer_Rule.CTR
section‹‹CTR››
theory CTR
imports
"../UD/UD"
"HOL-Library.Conditional_Parametricity"
keywords "ctr_relator" :: thy_defn
and "ctr" :: thy_defn
and "trp"
and "synthesis"
and "relativization"
and "hybrid"
and "parametricity"
begin
subsection‹Import›
ML_file "CTR_Relators.ML"
ML_file "CTR_Foundations.ML"
ML_file "CTR_Algorithm.ML"
ML_file "CTR_Conversions.ML"
ML_file "CTR_Relativization.ML"
ML_file "CTR_Parametricity.ML"
ML_file "CTR_Postprocessing.ML"
ML_file "CTR.ML"
subsection‹Rewriting›
named_theorems ctr_blank
named_theorems ctr_simps
lemma ctr_simps_pred_fun_top_eq_range[ctr_simps]:
"pred_fun top (λx. x ∈ R) f = (range f ⊆ R)"
by auto
lemma ctr_simps_pred_prod_eq_cart[ctr_simps]:
"pred_prod (λx. x ∈ A) (λx. x ∈ B) = (λx. x ∈ A × B)"
by auto
lemma ctr_simps_pred_fun_eq_image[ctr_simps]:
"pred_fun (λx. x ∈ D) (λx. x ∈ R) f ⟷ (f ` D ⊆ R)"
by auto
lemma ctr_simps_in_iff[ctr_simps]: "(∀x∈A. x ∈ U) ⟷ A ⊆ U" by auto
lemma ctr_simps_subset_pow_iff[ctr_simps]: "(∀A∈S. A ⊆ U) ⟷ S ⊆ Pow U"
by auto
lemma ctr_simps_subset_pow_iff'[ctr_simps]:
"(∀A. A ∈ S ⟶ A ⊆ U) ⟷ S ⊆ Pow U"
by auto
lemma ctr_simps_subset_pow_iff''[ctr_simps]: "(S ⊆ {S. S ⊆ U}) ⟷ S ⊆ Pow U"
by (simp add: subset_eq)
lemma ctr_simps_range_ss_iff[ctr_simps]: "(∀x. f x ∈ U) ⟷ range f ⊆ U"
by auto
lemma ctr_simps_range_pow_ss_iff[ctr_simps]: "(∀x. f x ⊆ U) ⟷ range f ⊆ Pow U"
by auto
lemma ctr_simps_Ball_def'[ctr_simps]: "(∀x. x ∈ A ⟶ P x) ⟷ (∀x ∈ A. P x)"
by auto
lemma ctr_simps_True_imp[ctr_simps]: "(True ⟶ A) ⟷ A" by simp
lemma ctr_simps_True_conj[ctr_simps]: "(True ∧ A) ⟷ A" by simp
lemma ctr_simps_conj_True[ctr_simps]: "(A ∧ True) ⟷ A" by simp
lemma ctr_simps_top_True[ctr_simps]: "top A ⟷ True" by auto
lemma ctr_simps_Ball_True[ctr_simps]: "(∀x∈U. True) ⟷ True" by auto
lemma ctr_simps_Ball_UNIV[ctr_simps]: "(∀n∈UNIV. A n) ⟷ (∀n. A n)" by simp
lemma ctr_simps_Bex_UNIV[ctr_simps]: "(∃n∈UNIV. A n) ⟷ (∃n. A n)" by simp
lemma ctr_simps_subset_Pow[ctr_simps]: "{A. A ⊆ U} = Pow U" by blast
lemma ctr_simps_mem_Collect_eq[ctr_simps]: "(a ∈ Collect P) = P a"
by (rule mem_Collect_eq)
lemma ctr_simps_relation_top_empty_eq[ctr_simps]: "(λx. x ∈ UNIV) = top"
by auto
lemma ctr_simps_pred_fun_eq[ctr_simps]:
"pred_fun A B = (λf. ∀x. A x ⟶ B (f x))"
by simp
lemma ctr_simps_subset_eq_sym[ctr_simps]: "(∀x∈A. x ∈ B) ⟷ (A ⊆ B)" by auto
lemma ctr_simps_UNIV_I[ctr_simps]: "x ∈ UNIV" by simp
lemma ctr_simps_UNIV_def[ctr_simps]: "{x. True} = UNIV" by simp
lemma ctr_simps_conj_commute[ctr_simps]: "(P ∧ Q) ⟷ (Q ∧ P)" by auto
lemma ctr_simps_conj_absorb[ctr_simps]: "(A ∧ A) ⟷ A" by simp
lemma ctr_simps_conj_left_absorb[ctr_simps]: "(A ∧ A ∧ B) ⟷ (A ∧ B)" by simp
lemma ctr_simps_inf_idem[ctr_simps]: "inf a a = (a::'a::semilattice_inf)"
by simp
lemma ctr_simps_sup_idem[ctr_simps]: "sup a a = (a::'a::semilattice_sup)"
by simp
lemma ctr_simps_inf_assoc[ctr_simps]:
"inf (inf a b) c = inf (a::'a::semilattice_inf) (inf b c)"
by (auto simp: semilattice_inf_class.inf.assoc)
lemma ctr_simps_sup_assoc[ctr_simps]:
"sup (sup a b) c = sup (a::'a::semilattice_sup) (sup b c)"
by (auto simp: semilattice_sup_class.sup.assoc)
lemma ctr_simps_Collect_mem_eq[ctr_simps]: "{x. x ∈ U} = U" by simp
subsection‹tts relators›
ctr_relator rel_set
ctr_relator rel_filter
end