Theory CTR

(* Title: CTR/CTR.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins

Infrastructure for the synthesis of the transfer rules and relativized 
constants.
*)


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