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.
*)


sectionCTR›
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]: "(xA. x  U)  A  U" by auto
lemma ctr_simps_subset_pow_iff[ctr_simps]: "(AS. 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]: "(xU. True)  True" by auto
lemma ctr_simps_Ball_UNIV[ctr_simps]: "(nUNIV. A n)  (n. A n)" by simp
lemma ctr_simps_Bex_UNIV[ctr_simps]: "(nUNIV. 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]: "(xA. 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