From 3b50c288f55e88cec0ec7c4785adf778330e6ace Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Mon, 26 Feb 2024 17:57:13 +0000 Subject: [PATCH 1/7] Add operations for high level sugar until tvsubst --- ROOT | 2 + Tools/binder_induction.ML | 2 +- Tools/mrbnf_recursor.ML | 2 +- Tools/mrbnf_vvsubst.ML | 7 +- operations/Fixpoint.thy | 27 +- operations/Sugar.thy | 604 +++++++++++++++++++++++++++++++++++++ operations/VVSubst.thy | 6 +- thys/MRBNF_FP.thy | 337 +++++++++++++++++++++ thys/MRBNF_Recursor.thy | 338 +-------------------- thys/System_Fc/SystemF.thy | 5 + 10 files changed, 983 insertions(+), 347 deletions(-) create mode 100644 operations/Sugar.thy create mode 100644 thys/MRBNF_FP.thy diff --git a/ROOT b/ROOT index bd175f57..6282a03a 100644 --- a/ROOT +++ b/ROOT @@ -32,6 +32,7 @@ session Binders in "thys" = Prelim + "../Tools" theories MRBNF_Composition + MRBNF_FP MRBNF_Recursor Generic_Barendregt_Enhanced_Rule_Induction General_Customization @@ -43,6 +44,7 @@ session Operations in "operations" = Binders + Recursor VVSubst TVSubst + Sugar session Untyped_Lambda_Calculus in "thys/Untyped_Lambda_Calculus" = Binders + theories diff --git a/Tools/binder_induction.ML b/Tools/binder_induction.ML index 3c165677..08839588 100644 --- a/Tools/binder_induction.ML +++ b/Tools/binder_induction.ML @@ -482,7 +482,7 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking ]) ctxt ] end); - val rule_thm = Local_Defs.unfold0 ctxt @{thms MRBNF_Recursor.prod_sets_simps triv_forall_equality} rule_thm; + val rule_thm = Local_Defs.unfold0 ctxt @{thms MRBNF_FP.prod_sets_simps triv_forall_equality} rule_thm; val names = map (fst o dest_Free) ( fst (BNF_Util.mk_Frees "Bound" (map (K HOLogic.unitT) bound_prems) ctxt) ); diff --git a/Tools/mrbnf_recursor.ML b/Tools/mrbnf_recursor.ML index 1e19aaeb..280cc7a6 100644 --- a/Tools/mrbnf_recursor.ML +++ b/Tools/mrbnf_recursor.ML @@ -195,7 +195,7 @@ fun mk_quotient_model quot substitution qmodel = binding = #binding qmodel, UFVarss = map (Term.abs ("t", #T quot) o subst) (#FVars quot), Umap = fold_rev Term.abs (map (pair "f") Ts) ( - Term.abs ("t", #T quot) (Term.list_comb (#rename quot, map Bound (length Ts downto 1))) + Term.abs ("t", #T quot) (Term.list_comb (subst (#rename quot), map Bound (length Ts downto 1))) ), Uctor = #Uctor qmodel, validity = Option.map (fn v => { diff --git a/Tools/mrbnf_vvsubst.ML b/Tools/mrbnf_vvsubst.ML index 9b8e2190..d5e0b7ed 100644 --- a/Tools/mrbnf_vvsubst.ML +++ b/Tools/mrbnf_vvsubst.ML @@ -2046,17 +2046,18 @@ fun mrbnf_of_quotient_fixpoint vvsubst_bs qualify (fp_result : MRBNF_FP_Def_Suga val lthy = fold (fn (mrbnf, quot) => MRBNF_Def.register_mrbnf_raw (fst (dest_Type (#T quot))) mrbnf) (xs ~~ #quotient_fps fp_res) lthy; - val (notess, lthy) = @{fold_map 3} (fn quot => fn vvsubst_cctor => fn vvsubst_rrename => fn lthy => + val (notess, lthy) = @{fold_map 4} (fn quot => fn vvsubst_cctor => fn vvsubst_rrename => fn pset_simps => fn lthy => let val vname = short_type_name (fst (dest_Type (#T quot))); val notes = [(vname ^ "_cctor", [vvsubst_cctor]), - (vname ^ "_vvsubst_rrename", [vvsubst_rrename]) + (vname ^ "_vvsubst_rrename", [vvsubst_rrename]), + (vname ^ "_set_simps", pset_simps) ] |> (map (fn (thmN, thms) => ((Binding.name thmN, []), [(thms, [])]) )); in Local_Theory.notes notes lthy end - ) (#quotient_fps fp_res) vvsubst_cctors vvsubst_rrenames lthy; + ) (#quotient_fps fp_res) vvsubst_cctors vvsubst_rrenames pset_simpss lthy; val ress = map2 (fn t1 => fn t2 => { vvsubst_ctor = t1, diff --git a/operations/Fixpoint.thy b/operations/Fixpoint.thy index 15b7ffba..9bd61623 100644 --- a/operations/Fixpoint.thy +++ b/operations/Fixpoint.thy @@ -1,17 +1,34 @@ theory Fixpoint - imports "Binders.MRBNF_Recursor" + imports "Binders.MRBNF_FP" begin (* TODO: Show proofs as apply script *) +ML \ +val ctor_T1_Ts = [ + [@{typ 'var}], + [@{typ unit}], + [@{typ 'tyvar}], + [@{typ 'rec}, @{typ 'rec2}], + [@{typ 'bvar}, @{typ 'brec}], + [@{typ 'btyvar}, @{typ 'brec}], + [@{typ 'a}] +] +val ctor_T2_Ts = [ + [@{typ 'var}], + [@{typ 'tyvar}], + [@{typ 'rec}, @{typ 'rec2}], + [@{typ 'bvar}, @{typ "'brec list"}], + [@{typ 'btyvar}, @{typ 'brec2}], + [@{typ 'b}, @{typ 'rec}] +] +\ ML \ -val T1 = @{typ "(('var + unit) + 'tyvar + 'rec * 'rec2) + ('bvar * 'brec + 'btyvar * 'brec2) + 'a"} -val T2 = @{typ "('var + 'tyvar + 'rec * 'rec2) + 'bvar * 'brec + 'btyvar * 'brec2 + 'b * 'rec"}; +val T1 = BNF_FP_Util.mk_sumprodT_balanced ctor_T1_Ts +val T2 = BNF_FP_Util.mk_sumprodT_balanced ctor_T2_Ts val name1 = "T1"; val name2 = "T2"; val rel = [[1,3], [1]]; -(*val T1 = @{typ "'var + unit + 'tyvar + 'rec * 'rec2 + 'bvar * 'brec + 'btyvar * 'brec2 + 'a"} -val T2 = @{typ "'var + 'tyvar + 'rec * 'rec2 + 'bvar * 'brec + 'btyvar * 'brec2 + 'b * 'rec"};*) Multithreading.parallel_proofs := 4 \ diff --git a/operations/Sugar.thy b/operations/Sugar.thy new file mode 100644 index 00000000..d2f7b687 --- /dev/null +++ b/operations/Sugar.thy @@ -0,0 +1,604 @@ +theory Sugar + imports Fixpoint +begin + +ML \ +val res = the (MRBNF_FP_Def_Sugar.fp_result_of @{context} "Fixpoint.T1") +\ + +ML_file \../Tools/mrbnf_vvsubst.ML\ + +local_setup \fn lthy => +let + val (ress, lthy) = MRBNF_VVSubst.mrbnf_of_quotient_fixpoint + [@{binding vvsubst_T1}, @{binding vvsubst_T2}] I res lthy; + val lthy = @{fold 2} (fn (mrbnf, _) => fn quot => + MRBNF_Def.register_mrbnf_raw (fst (dest_Type (#T quot))) mrbnf + ) ress (#quotient_fps res) lthy; +in lthy end +\ +print_theorems +print_mrbnfs + +class var = var_T1_pre + var_T2_pre + +definition Var_T1 :: "'var \ ('var::var, 'tyvar::var, 'a::var, 'b) T1" where + "Var_T1 x \ T1_ctor (Abs_T1_pre (Inl (Inl x)))" +definition Arrow_T1 :: "('var::var, 'tyvar::var, 'a::var, 'b) T1" where + "Arrow_T1 \ T1_ctor (Abs_T1_pre (Inl (Inr (Inl ()))))" +definition TyVar_T1 :: "'tyvar \ ('var::var, 'tyvar::var, 'a::var, 'b) T1" where + "TyVar_T1 a \ T1_ctor (Abs_T1_pre (Inl (Inr (Inr a))))" +definition App_T1 :: "('var::var, 'tyvar::var, 'a::var, 'b) T1 \ ('var, 'tyvar, 'a, 'b) T2 \ ('var, 'tyvar, 'a, 'b) T1" where + "App_T1 t1 t2 \ T1_ctor (Abs_T1_pre (Inr (Inl (Inl (t1, t2)))))" +definition Lam_T1 :: "'var \ ('var::var, 'tyvar::var, 'a::var, 'b) T1 \ ('var, 'tyvar, 'a, 'b) T1" where + "Lam_T1 x t \ T1_ctor (Abs_T1_pre (Inr (Inl (Inr (x, t)))))" +definition TyLam_T1 :: "'tyvar \ ('var, 'tyvar, 'a, 'b) T1 \ ('var::var, 'tyvar::var, 'a::var, 'b) T1" where + "TyLam_T1 a t \ T1_ctor (Abs_T1_pre (Inr (Inr (Inl (a, t)))))" +definition Ext_T1 :: "'a \ ('var::var, 'tyvar::var, 'a::var, 'b) T1" where + "Ext_T1 x \ T1_ctor (Abs_T1_pre (Inr (Inr (Inr x))))" + +definition Var_T2 :: "'var \ ('var::var, 'tyvar::var, 'a::var, 'b) T2" where + "Var_T2 x \ T2_ctor (Abs_T2_pre (Inl (Inl x)))" +definition TyVar_T2 :: "'tyvar \ ('var::var, 'tyvar::var, 'a::var, 'b) T2" where + "TyVar_T2 a \ T2_ctor (Abs_T2_pre (Inl (Inr (Inl a))))" +definition App_T2 :: "('var, 'tyvar, 'a, 'b) T1 \ ('var, 'tyvar, 'a, 'b) T2 \ ('var::var, 'tyvar::var, 'a::var, 'b) T2" where + "App_T2 t1 t2 \ T2_ctor (Abs_T2_pre (Inl (Inr (Inr (t1, t2)))))" +definition Lam_T2 :: "'var \ ('var, 'tyvar, 'a, 'b) T1 list \ ('var::var, 'tyvar::var, 'a::var, 'b) T2" where + "Lam_T2 x t \ T2_ctor (Abs_T2_pre (Inr (Inl (x, t))))" +definition TyLam_T2 :: "'tyvar \ ('var, 'tyvar, 'a, 'b) T2 \ ('var::var, 'tyvar::var, 'a::var, 'b) T2" where + "TyLam_T2 x t \ T2_ctor (Abs_T2_pre (Inr (Inr (Inl (x, t)))))" +definition Ext_T2 :: "'b \ ('var, 'tyvar, 'a, 'b) T1 \ ('var::var, 'tyvar::var, 'a::var, 'b) T2" where + "Ext_T2 b t \ T2_ctor (Abs_T2_pre (Inr (Inr (Inr (b, t)))))" + +lemmas T1_ctors_defs = Var_T1_def Arrow_T1_def TyVar_T1_def App_T1_def Lam_T1_def TyLam_T1_def Ext_T1_def +lemmas T2_ctors_defs = Var_T2_def TyVar_T2_def App_T2_def Lam_T2_def TyLam_T2_def Ext_T2_def + +lemmas T1_pre_set_defs = set1_T1_pre_def set2_T1_pre_def set3_T1_pre_def set4_T1_pre_def set5_T1_pre_def set6_T1_pre_def set7_T1_pre_def set8_T1_pre_def set9_T1_pre_def set10_T1_pre_def +lemmas T2_pre_set_defs = set1_T2_pre_def set2_T2_pre_def set3_T2_pre_def set4_T2_pre_def set5_T2_pre_def set6_T2_pre_def set7_T2_pre_def set8_T2_pre_def set9_T2_pre_def set10_T2_pre_def + +lemma T1_T2_strong_induct: + fixes t1::"('var::var, 'tyvar::var, 'a::var, 'b) T1" and t2::"('var::var, 'tyvar::var, 'a::var, 'b) T2" + assumes + "\\. |K1 \| \. |K2 \| x \. P (Var_T1 x) \" + "\\. P Arrow_T1 \" + "\a \. P (TyVar_T1 a) \" + "\t1 t2 \. \\. P t1 \ \ \\. P2 t2 \ \ P (App_T1 t1 t2) \" + "\x t \. x \ K1 \ \ \\. P t \ \ P (Lam_T1 x t) \" + "\a t \. a \ K2 \ \ \\. P t \ \ P (TyLam_T1 a t) \" + "\a \. P (Ext_T1 a) \" + + "\x \. P2 (Var_T2 x) \" + "\a \. P2 (TyVar_T2 a) \" + "\t1 t2 \. \\. P t1 \ \ \\. P2 t2 \ \ P2 (App_T2 t1 t2) \" + "\x ts \. x \ K1 \ \ (\t \. t \ set ts \ P t \) \ P2 (Lam_T2 x ts) \" + "\a t \. a \ K2 \ \ \\. P2 t \ \ P2 (TyLam_T2 a t) \" + "\b t \. \\. P t \ \ P2 (Ext_T2 b t) \" + shows "\\. P t1 \ \ P2 t2 \" + apply (unfold ball_UNIV[symmetric]) + apply (rule T1.TT_fresh_co_induct_param[of _ K1 K2 P P2 t1 t2]) + apply (rule assms(1,2)[THEN spec])+ + subgoal for v1 \ + apply (tactic \resolve_tac @{context} [infer_instantiate' @{context} [SOME @{cterm v1}] ( + BNF_FP_Util.mk_absumprodE @{thm type_definition_T1_pre} (map length ctor_T1_Ts) + )] 1\; hypsubst_thin) + (* REPEAT_DETERM *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(1)) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(2)) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(3)) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(4)) + (* REPEAT_DETERM *) + apply (rule allI) + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(1)) (* nonbinding occurence of T1 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* repeated *) + apply (rule allI) + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(3)) (* nonbinding occurence of T2 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* END REPEAT_DETERM *) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(5)) + (* REPEAT_DETERM *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(5)) (* bound var of type 'var *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* repeated *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(2)) (* binding occurence of T1 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* END REPEAT_DETERM *) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(6)) + (* REPEAT_DETERM *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(6)) (* bound var of type 'tyvar *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* repeated *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(2)) (* binding occurence of T1 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* END REPEAT_DETERM *) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T1_ctors_defs[symmetric] Abs_T1_pre_inverse[OF UNIV_I] + T1_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(7)) + (* END REPEAT_DETERM *) + done + + subgoal for v2 \ + apply (tactic \resolve_tac @{context} [infer_instantiate' @{context} [SOME @{cterm v2}] ( + BNF_FP_Util.mk_absumprodE @{thm type_definition_T2_pre} (map length ctor_T2_Ts) + )] 1\; hypsubst_thin) + (* REPEAT_DETERM *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T2_ctors_defs[symmetric] Abs_T2_pre_inverse[OF UNIV_I] + T2_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(8)) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T2_ctors_defs[symmetric] Abs_T2_pre_inverse[OF UNIV_I] + T2_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(9)) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T2_ctors_defs[symmetric] Abs_T2_pre_inverse[OF UNIV_I] + T2_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(10)) + (* repeated *) + (* REPEAT_DETERM *) + apply (rule allI) + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(1)) (* nonbinding occurence of T1 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* repeated *) + apply (rule allI) + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(3)) (* nonbinding occurence of T2 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* END REPEAT_DETERM *) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T2_ctors_defs[symmetric] Abs_T2_pre_inverse[OF UNIV_I] + T2_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(11)) + (* REPEAT_DETERM *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(5)) (* bound var of type 'var *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* repeated *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(2)) (* binding occurence of T1 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I prems)+ + done + (* END REPEAT_DETERM *) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T2_ctors_defs[symmetric] Abs_T2_pre_inverse[OF UNIV_I] + T2_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(12)) + (* REPEAT_DETERM *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(6)) (* bound var of type 'tyvar *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I)+ + done + (* repeated *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(4)) (* binding occurence of T2 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I prems)+ + done + (* END REPEAT_DETERM *) + (* repeated *) + apply (subst unit_eq)? + apply (unfold sum.set_map prod.set_map UN_empty2 Un_empty_left Un_empty_right comp_def + UN_singleton sum_set_simps prod_set_simps UN_single UN_empty + T2_ctors_defs[symmetric] Abs_T2_pre_inverse[OF UNIV_I] + T2_pre_set_defs + )[1] + apply (subst (asm) list.set_map, ((rule supp_id_bound bij_id)+)?)? (* For nested BNFs *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule IHs(13)) + (* REPEAT_DETERM *) + apply (rule allI)? + apply (rule disjointI)? + subgoal premises prems + apply (rule prems(1)) (* nonbinding occurence of T1 *) + apply (unfold UN_empty UN_empty2 Un_empty_left Un_empty_right)? + apply (rule singletonI UNIV_I UN_I prems)+ + done + (* END REPEAT_DETERM *) + done + done + +lemmas T1_T2_induct = T1_T2_strong_induct[of "\_. {}" "\_. {}" "\t \. _ t" "\t \. _ t", + unfolded HOL.simp_thms(35), OF emp_bound emp_bound, + unfolded notin_empty_eq_True Int_empty_right HOL.simp_thms(6) HOL.True_implies_equals +] + +lemmas set_simp_thms = sum.set_map prod.set_map comp_def UN_empty UN_empty2 Un_empty_left Un_empty_right + UN_singleton UN_single sum_set_simps prod_set_simps Diff_empty UN_Un empty_Diff + +lemma set_T1_simps[simp]: + "FFVars_T11 (Var_T1 x) = {x}" + "FFVars_T11 Arrow_T1 = {}" + "FFVars_T11 (TyVar_T1 a) = {}" + "FFVars_T11 (App_T1 t1 t2) = FFVars_T11 t1 \ FFVars_T21 t2" + "FFVars_T11 (Lam_T1 x t) = FFVars_T11 t - {x}" + "FFVars_T11 (TyLam_T1 a t) = FFVars_T11 t" + "FFVars_T11 (Ext_T1 a) = {}" + + "FFVars_T12 (Var_T1 x) = {}" + "FFVars_T12 Arrow_T1 = {}" + "FFVars_T12 (TyVar_T1 a) = {a}" + "FFVars_T12 (App_T1 t1 t2) = FFVars_T12 t1 \ FFVars_T22 t2" + "FFVars_T12 (Lam_T1 x t) = FFVars_T12 t" + "FFVars_T12 (TyLam_T1 a t) = FFVars_T12 t - {a}" + "FFVars_T12 (Ext_T1 a) = {}" + + "set3_T1 (Var_T1 x) = {}" + "set3_T1 Arrow_T1 = {}" + "set3_T1 (TyVar_T1 a) = {}" + "set3_T1 (App_T1 t1 t2) = set3_T1 t1 \ set3_T2 t2" + "set3_T1 (Lam_T1 x t) = set3_T1 t" + "set3_T1 (TyLam_T1 a t) = set3_T1 t" + "set3_T1 (Ext_T1 a) = {a}" + + "set4_T1 (Var_T1 x) = {}" + "set4_T1 Arrow_T1 = {}" + "set4_T1 (TyVar_T1 a) = {}" + "set4_T1 (App_T1 t1 t2) = set4_T1 t1 \ set4_T2 t2" + "set4_T1 (Lam_T1 x t) = set4_T1 t" + "set4_T1 (TyLam_T1 a t) = set4_T1 t" + "set4_T1 (Ext_T1 a) = {}" + apply (unfold set_simp_thms T1_ctors_defs T1.FFVars_cctors + T1_pre_set_defs Abs_T1_pre_inverse[OF UNIV_I] + T1_set_simps + ) + apply (rule refl)+ + done + +lemma set_T2_simps[simp]: + "FFVars_T21 (Var_T2 x) = {x}" + "FFVars_T21 (TyVar_T2 a) = {}" + "FFVars_T21 (App_T2 t1 t2) = FFVars_T11 t1 \ FFVars_T21 t2" + "FFVars_T21 (Lam_T2 x ts) = \(FFVars_T11 ` set ts)- {x}" + "FFVars_T21 (TyLam_T2 a t) = FFVars_T21 t" + "FFVars_T21 (Ext_T2 b t1) = FFVars_T11 t1" + + "FFVars_T22 (Var_T2 x) = {}" + "FFVars_T22 (TyVar_T2 a) = {a}" + "FFVars_T22 (App_T2 t1 t2) = FFVars_T12 t1 \ FFVars_T22 t2" + "FFVars_T22 (Lam_T2 x ts) = \(FFVars_T12 ` set ts)" + "FFVars_T22 (TyLam_T2 a t) = FFVars_T22 t" + "FFVars_T22 (Ext_T2 b t1) = FFVars_T12 t1" + + "set3_T2 (Var_T2 x) = {}" + "set3_T2 (TyVar_T2 a) = {}" + "set3_T2 (App_T2 t1 t2) = set3_T1 t1 \ set3_T2 t2" + "set3_T2 (Lam_T2 x ts) = \(set3_T1 ` set ts)" + "set3_T2 (TyLam_T2 a t) = set3_T2 t" + "set3_T2 (Ext_T2 b t1) = set3_T1 t1" + + "set4_T2 (Var_T2 x) = {}" + "set4_T2 (TyVar_T2 a) = {}" + "set4_T2 (App_T2 t1 t2) = set4_T1 t1 \ set4_T2 t2" + "set4_T2 (Lam_T2 x ts) = \(set4_T1 ` set ts)" + "set4_T2 (TyLam_T2 a t) = set4_T2 t" + "set4_T2 (Ext_T2 b t1) = {b} \ set4_T1 t1" +apply (unfold set_simp_thms T2_ctors_defs T1.FFVars_cctors + T2_pre_set_defs Abs_T2_pre_inverse[OF UNIV_I] + T2_set_simps + ) + apply (rule refl)+ + done + +lemma T1_distinct[simp]: + "Var_T1 x \ Arrow_T1" + "Var_T1 x \ TyVar_T1 a" + "Var_T1 x \ App_T1 t1 t2" + "Var_T1 x \ Lam_T1 a1 t" + "Var_T1 x \ TyLam_T1 a2 t1" + "Var_T1 x \ Ext_T1 a3" + + "Arrow_T1 \ Var_T1 x" + "Arrow_T1 \ TyVar_T1 a" + "Arrow_T1 \ App_T1 t1 t2" + "Arrow_T1 \ Lam_T1 a1 t" + "Arrow_T1 \ TyLam_T1 a2 t1" + "Arrow_T1 \ Ext_T1 a3" + + "TyVar_T1 a \ Var_T1 x" + "TyVar_T1 a \ Arrow_T1" + "TyVar_T1 a \ App_T1 t1 t2" + "TyVar_T1 a \ Lam_T1 a1 t" + "TyVar_T1 a \ TyLam_T1 a2 t1" + "TyVar_T1 a \ Ext_T1 a3" + + "App_T1 t1 t2 \ Var_T1 x" + "App_T1 t1 t2 \ Arrow_T1" + "App_T1 t1 t2 \ TyVar_T1 a" + "App_T1 t1 t2 \ Lam_T1 a1 t" + "App_T1 t1 t2 \ TyLam_T1 a2 t1" + "App_T1 t1 t2 \ Ext_T1 a3" + + "Lam_T1 a1 t \ Var_T1 x" + "Lam_T1 a1 t \ Arrow_T1" + "Lam_T1 a1 t \ TyVar_T1 a" + "Lam_T1 a1 t \ App_T1 t1 t2" + "Lam_T1 a1 t \ TyLam_T1 a2 t1" + "Lam_T1 a1 t \ Ext_T1 a3" + + "TyLam_T1 a2 t1 \ Var_T1 x" + "TyLam_T1 a2 t1 \ Arrow_T1" + "TyLam_T1 a2 t1 \ TyVar_T1 a" + "TyLam_T1 a2 t1 \ App_T1 t1 t2" + "TyLam_T1 a2 t1 \ Lam_T1 a1 t" + "TyLam_T1 a2 t1 \ Ext_T1 a3" + + "Ext_T1 a3 \ Var_T1 x" + "Ext_T1 a3 \ Arrow_T1" + "Ext_T1 a3 \ TyVar_T1 a" + "Ext_T1 a3 \ App_T1 t1 t2" + "Ext_T1 a3 \ Lam_T1 a1 t" + "Ext_T1 a3 \ TyLam_T1 a2 t1" + apply (unfold comp_def map_sum.simps map_prod_simp sum.inject + T1_ctors_defs T1.TT_injects0 map_T1_pre_def + Abs_T1_pre_inverse[OF UNIV_I] Abs_T1_pre_inject[OF UNIV_I UNIV_I] +) + apply (rule notI, (erule exE conjE sum.distinct[THEN notE])+)+ + done + +lemma T2_distinct[simp]: + "Var_T2 x \ TyVar_T2 a" + "Var_T2 x \ App_T2 t1 t2" + "Var_T2 x \ Lam_T2 x1 t3" + "Var_T2 x \ TyLam_T2 a2 t4" + "Var_T2 x \ Ext_T2 a3 t5" + + "TyVar_T2 a \ Var_T2 x" + "TyVar_T2 a \ App_T2 t1 t2" + "TyVar_T2 a \ Lam_T2 x1 t3" + "TyVar_T2 a \ TyLam_T2 a2 t4" + "TyVar_T2 a \ Ext_T2 a3 t5" + + "App_T2 t1 t2 \ Var_T2 x" + "App_T2 t1 t2 \ TyVar_T2 a" + "App_T2 t1 t2 \ Lam_T2 x1 t3" + "App_T2 t1 t2 \ TyLam_T2 a2 t4" + "App_T2 t1 t2 \ Ext_T2 a3 t5" + + "Lam_T2 x1 t3 \ Var_T2 x" + "Lam_T2 x1 t3 \ TyVar_T2 a" + "Lam_T2 x1 t3 \ App_T2 t1 t2" + "Lam_T2 x1 t3 \ TyLam_T2 a2 t4" + "Lam_T2 x1 t3 \ Ext_T2 a3 t5" + + "TyLam_T2 a2 t4 \ Var_T2 x" + "TyLam_T2 a2 t4 \ TyVar_T2 a" + "TyLam_T2 a2 t4 \ App_T2 t1 t2" + "TyLam_T2 a2 t4 \ Lam_T2 x1 t3" + "TyLam_T2 a2 t4 \ Ext_T2 a3 t5" + + "Ext_T2 a3 t5 \ Var_T2 x" + "Ext_T2 a3 t5 \ TyVar_T2 a" + "Ext_T2 a3 t5 \ App_T2 t1 t2" + "Ext_T2 a3 t5 \ Lam_T2 x1 t3" + "Ext_T2 a3 t5 \ TyLam_T2 a2 t4" + apply (unfold comp_def map_sum.simps map_prod_simp sum.inject + T2_ctors_defs T1.TT_injects0 map_T2_pre_def + Abs_T2_pre_inverse[OF UNIV_I] Abs_T2_pre_inject[OF UNIV_I UNIV_I] +) + apply (rule notI, (erule exE conjE sum.distinct[THEN notE])+)+ + done + +abbreviation "eta11 (x::_::var) \ Abs_T1_pre (Inl (Inl x))" +abbreviation "eta12 (x::_::var) \ Abs_T1_pre (Inl (Inr (Inr x)))" +abbreviation "eta21 (x::_::var) \ Abs_T2_pre (Inl (Inl x))" + +lemma eta_frees: + "set1_T1_pre (eta11 x) = {x}" + "set2_T1_pre (eta12 x2) = {x2}" + "set1_T2_pre (eta21 x3) = {x3}" + apply (unfold set_simp_thms T1_pre_set_defs Abs_T1_pre_inverse[OF UNIV_I] + T2_pre_set_defs Abs_T2_pre_inverse[OF UNIV_I]) + apply (rule refl)+ + done + +lemma eta_injs: + "eta11 a = eta11 a' \ a = a'" + "eta12 a2 = eta12 a2' \ a2 = a2'" + "eta21 a3 = eta21 a3' \ a3 = a3'" + apply (unfold sum.inject Abs_T1_pre_inject[OF UNIV_I UNIV_I] Abs_T2_pre_inject[OF UNIV_I UNIV_I]) + apply assumption+ + done + +lemma eta_compl_frees: + "x \ range eta11 \ set1_T1_pre x = {}" + "x2 \ range eta12 \ set2_T1_pre x2 = {}" + "x3 \ range eta21 \ set1_T2_pre x3 = {}" + subgoal + apply (unfold set_simp_thms T1_pre_set_defs) + apply (rule Abs_T1_pre_cases[of x]) + apply hypsubst_thin + apply (unfold image_iff bex_UNIV Abs_T1_pre_inverse[OF UNIV_I] Abs_T1_pre_inject[OF UNIV_I UNIV_I]) + apply (erule contrapos_np) + apply (drule iffD2[OF ex_in_conv]) + apply (erule exE) + apply (erule UN_E)+ + apply (erule setl.cases setr.cases)+ + apply hypsubst + apply (rule exI) + apply (rule refl) + done + subgoal + apply (unfold set_simp_thms T1_pre_set_defs) + apply (rule Abs_T1_pre_cases[of x2]) + apply hypsubst_thin + apply (unfold image_iff bex_UNIV Abs_T1_pre_inverse[OF UNIV_I] Abs_T1_pre_inject[OF UNIV_I UNIV_I]) + apply (erule contrapos_np) + apply (drule iffD2[OF ex_in_conv]) + apply (erule exE) + apply (erule UN_E)+ + apply (erule setl.cases setr.cases)+ + apply hypsubst + apply (rule exI) + apply (rule refl) + done + subgoal + apply (unfold set_simp_thms T2_pre_set_defs) + apply (rule Abs_T2_pre_cases[of x3]) + apply hypsubst_thin + apply (unfold image_iff bex_UNIV Abs_T2_pre_inverse[OF UNIV_I] Abs_T2_pre_inject[OF UNIV_I UNIV_I]) + apply (erule contrapos_np) + apply (drule iffD2[OF ex_in_conv]) + apply (erule exE) + apply (erule UN_E)+ + apply (erule setl.cases setr.cases)+ + apply hypsubst + apply (rule exI) + apply (rule refl) + done + done + +lemma eta_naturals: + fixes f1::"('x1::var \ 'x1)" and f2::"('x2::var \ 'x2)" + and f3::"('x3::var \ 'x3)" and f4::"('x4::var \ 'x4)" + assumes "|supp f1| eta11 = eta11 \ f1" + "map_T1_pre f1 f2 id id f3 f4 f5 f6 f7 f8 \ eta12 = eta12 \ f2" + "map_T2_pre f1 f2 id id f3 f4 f5 f6 f7 f8 \ eta21 = eta21 \ f1" + apply (unfold comp_def map_sum.simps Abs_T1_pre_inverse[OF UNIV_I] + map_T1_pre_def map_T2_pre_def Abs_T2_pre_inverse[OF UNIV_I] + ) + apply (rule refl)+ + done + +end \ No newline at end of file diff --git a/operations/VVSubst.thy b/operations/VVSubst.thy index a31e2dae..277be175 100644 --- a/operations/VVSubst.thy +++ b/operations/VVSubst.thy @@ -5269,7 +5269,11 @@ subclass (in var_T1) var_T1_pre apply (rule large) apply (rule regular) done -subclass (in var_T1) var_T2_pre by standard +subclass (in var_T1) var_T2_pre + apply standard + apply (rule large) + apply (rule regular) + done mrbnf "('var, 'tyvar, 'a, 'b) T1" map: vvsubst_T1 diff --git a/thys/MRBNF_FP.thy b/thys/MRBNF_FP.thy new file mode 100644 index 00000000..59bb3b6b --- /dev/null +++ b/thys/MRBNF_FP.thy @@ -0,0 +1,337 @@ +theory MRBNF_FP + imports "MRBNF_Composition" + (*keywords "binder_inductive" :: thy_goal*) +begin + +lemma card_of_subset_bound: "\ B \ A ; |A| \ |B| |A - B| o |UNIV::'b set|" "|U \ S::'b set| B. U \ B = {} \ B \ S = {} \ |U| =o |B|" +proof - + have 1: "|U| S)| =o |UNIV::'b set|" + using card_of_Un_diff_infinite[OF + cinfinite_imp_infinite[OF cinfinite_mono[OF assms(2) conjunct1[OF assms(1)]]] + ordLess_ordLeq_trans[OF assms(3,2)] + ] + by (simp add: Compl_eq_Diff_UNIV) + then have "|U| S)|" using ordLess_ordLeq_trans[OF 1 assms(2)] ordIso_symmetric ordLess_ordIso_trans by fast + then obtain B where 1: "B \ -(U \ S)" "|U| =o |B|" + by (meson internalize_card_of_ordLeq2 ordLess_imp_ordLeq) + then have "U \ B = {}" "B \ S = {}" by blast+ + then show ?thesis using 1 by blast +qed + +lemma exists_suitable_aux: + assumes "Cinfinite r" "r \o |UNIV::'a set|" "P \ |U \ (S - U)::'a set| (u::'a \ 'a). P \ bij u \ |supp u| imsupp u \ (S - U) = {} \ u ` U \ S = {}" +proof - + have 1: "P \ |U| U \ B = {}" "P \ B \ (S - U) = {}" "P \ |U| =o |B|" + using exists_subset_compl[OF assms(1,2,3)] by blast + obtain u where 3: "bij u" "P \ |supp u| bij_betw u U B" "P \ imsupp u \ (S - U) = {}" + using ordIso_ex_bij_betw_supp[OF assms(1) 1 2(3,1) Diff_disjoint 2(2)] by blast + then have "P \ u ` U \ B" unfolding bij_betw_def by blast + then have "P \ u ` U \ S = {}" using 2 by blast + then show ?thesis using 3 by blast +qed + +lemma fst_comp_map_prod: "h \ fst = fst \ map_prod h id" by auto + +lemma imsupp_same_subset: "\ a \ B ; a \ A ; imsupp f \ A \ B \ \ f a = a" + unfolding imsupp_def supp_def by blast + +lemma arg_cong3: "\ a1 = a2 ; b1 = b2 ; c1 = c2 \ \ h a1 b1 c1 = h a2 b2 c2" + by simp + +definition eq_bij_betw where + "eq_bij_betw r u w g A B x y f1 f2 h L R \ + bij u \ |supp u| imsupp u \ g (A x) = {} \ u ` f1 (A x) \ f1 (A x) = {} + \ bij w \ |supp w| imsupp w \ g (B y) = {} \ w ` f1 (B y) \ f1 (B y) = {} + \ eq_on (f2 y) (u \ L \ h) (w \ R)" + +lemma exists_bij_betw: + fixes L R h::"'a \ 'a" + assumes "Cinfinite r" "r \o |UNIV::'a set|" "bij R" "bij L" "bij h" "f2 x = h ` f2 y" + and u: "|f1 (A x) \ g (A x)::'a set| g (A x) = {}" "f1 (A x) = L ` f2 x" + and w: "|(f1 (B y)) \ (g (B y))::'a set| g (B y) = {}" "f1 (B y) = R ` f2 y" + shows "\(u::'a \ 'a) (w::'a \ 'a). + bij u \ |supp u| imsupp u \ g (A x) = {} \ u ` f1 (A x) \ f1 (A x) = {} + \ bij w \ |supp w| imsupp w \ g (B y) = {} \ w ` f1 (B y) \ f1 (B y) = {} + \ eq_on (f2 y) (u \ L \ h) (w \ R)" +proof - + have 1: "|f1 (A x)| g (A x) \ f1 (B y) \ g (B y)| -?A" "|f1 (A x)| =o |C|" + using ordLess_imp_ordLeq[THEN iffD1[OF internalize_card_of_ordLeq2]] by metis + then have 3: "f1 (A x) \ C = {}" "C \ g (A x) = {}" "f1 (B y) \ C = {}" "C \ g (B y) = {}" by blast+ + + obtain u::"'a \ 'a" where x: "bij u" "|supp u| g (A x) = {}" + using ordIso_ex_bij_betw_supp[OF assms(1) 1(1) C(2) 3(1) u(2) 3(2)] by blast + + have "bij_betw (inv R) (f1 (B y)) (f2 y)" unfolding bij_betw_def by (simp add: assms(3) inj_on_def w(3)) + moreover have "bij_betw h (f2 y) (f2 x)" using bij_imp_bij_betw assms(5,6) by auto + moreover have "bij_betw L (f2 x) (f1 (A x))" unfolding bij_betw_def by (simp add: assms(4) inj_on_def u(3)) + ultimately have 4: "bij_betw (u \ L \ h \ inv R) (f1 (B y)) C" using bij_betw_trans x(3) by blast + + obtain w::"'a \ 'a" where y: "bij w" "|supp w| g (B y) = {}" "eq_on (f1 (B y)) w (u \ L \ h \ inv R)" + using ex_bij_betw_supp[OF assms(1) 1(2) 4 3(3) w(2) 3(4)] by blast + + have "eq_on (f2 y) (u \ L \ h) (w \ R)" using y(5) unfolding eq_on_def using assms(3) w(3) by auto + moreover have "u ` f1 (A x) \ f1 (A x) = {}" "w ` f1 (B y) \ f1 (B y) = {}" using bij_betw_imp_surj_on x(3) y(3) 3(1,3) by blast+ + ultimately show ?thesis using x(1,2,4) y(1,2,4) by blast +qed + +lemmas exists_bij_betw_def = exists_bij_betw[unfolded eq_bij_betw_def[symmetric]] + +definition eq_bij_betw_refl where + "eq_bij_betw_refl r u w g A B x y f1 f2 L R \ + bij u \ |supp u| imsupp u \ g (A x) = {} \ u ` f1 (A x) \ f1 (A x) = {} + \ bij w \ |supp w| imsupp w \ g (B y) = {} \ w ` f1 (B y) \ f1 (B y) = {} + \ eq_on f2 (u \ L) (w \ R)" + +lemmas exists_bij_betw_refl = exists_bij_betw[OF _ _ _ _ bij_id image_id[symmetric], unfolded o_id] +lemmas exists_bij_betw_refl_UNIV = exists_bij_betw_refl[OF conjI[OF iffD2[OF cinfinite_iff_infinite] card_of_Card_order] ordLeq_refl[OF card_of_Card_order]] + +lemmas exists_bij_betw_refl_def = exists_bij_betw_refl[unfolded eq_bij_betw_refl_def[symmetric]] + +lemma imsupp_id_on: "imsupp u \ A = {} \ id_on A u" + unfolding imsupp_def supp_def id_on_def by blast + +lemma imsupp_image_subset: "u ` A \ A = {} \ A \ imsupp u" + unfolding imsupp_def supp_def by auto + +lemma Int_subset_empty1: "A \ B = {} \ C \ A \ C \ B = {}" by blast +lemma Int_subset_empty2: "A \ B = {} \ C \ B \ A \ C = {}" by blast +lemma exists_map_prod_id: "(a, b) \ map_prod f id ` A \ \c. (c, b) \ A \ a = f c" by auto + +lemma image_prod_f_g: "(a, b) \ (\x. (u x, g (u x))) ` A \ a \ u ` A \ b = g a" by blast +lemma Int_Un_empty: "A \ (B \ C \ D) = {} \ A \ B = {} \ A \ (C \ D) = {}" by blast + +lemma image_prod_f_g': "(a, b) \ (\x. (w x, g x)) ` A = (\x. x \ A \ a = w x \ b = g x)" by blast +lemma inv_id_middle: "bij u \ inv w (g (u z)) = u z \ (inv u \ (inv w \ g \ u)) z = id z" by simp +lemma inv_id_middle2: "bij R \ bij g \ (g \ R) z2 = (u \ L) z2 \ (inv R \ (inv g \ u \ L)) z2 = id z2" + by (metis bij_inv_eq_iff comp_apply id_apply) + +lemma eq_onD: "eq_on A u w \ z \ A \ u z = w z" + unfolding eq_on_def by blast + +lemma comp_pair: + "(\(a, b). (a, u a b)) \ (\t. (g t, w t)) = (\t. (g t, u (g t) (w t)))" + "(\(a, b). (z a, u a b)) \ (\t. (g t, w t)) = (\t. (z (g t), u (g t) (w t)))" + by auto + +lemma bij_if: "bij g \ bij (if P then id else g)" by simp +lemma supp_if: "|supp (u::'a \ 'a)| |supp (if P then id else u)| |supp u| |supp (if P then id else u)| A = {} \ imsupp (if P then id else u) \ A = {}" unfolding imsupp_def supp_def by simp +lemma image_if_empty: "u ` A \ B = {} \ (P \ A \ B = {}) \ (if P then id else u) ` A \ B = {}" by simp + +lemma Int_Un_emptyI1: "A \ (B \ C) = {} \ A \ B = {}" by blast +lemma Int_Un_emptyI2: "A \ (B \ C) = {} \ A \ C = {}" by blast + +lemma imsupp_comp_image: "bij f \ imsupp (f \ g \ inv f) = f ` imsupp g" + apply (auto simp: supp_def imsupp_def bij_inv_eq_iff image_in_bij_eq) + by (smt (verit, del_insts) imageI inv_simp1 mem_Collect_eq) + +lemma id_on_comp3: "c z = z \ b (c z) = c z \ a z = z \ (a \ b \ c) z = z" + by simp +lemma id_on_comp2: "b z = z \ a z = z \ (a \ b) z = z" by simp +lemma id_on_both: "a z = z \ b z = z \ a z = b z" by simp + +lemma not_imageI: "bij f \ a \ A \ f a \ f ` A" by force + +lemma Un_bound: + assumes inf: "infinite (UNIV :: 'a set)" + and "|A1| A2| |imsupp g| |supp g| imsupp f \ A" + unfolding imsupp_def supp_def by auto + +lemma Un_mono': "A \ C \ X \ B \ D \ X \ A \ B \ C \ D \ X" by blast +lemma Diff_Un_disjunct: "B \ C = {} \ A - B \ C = (A \ C) - B" by blast +lemma UN_empty': "A = {} \ \ (B ` A) = {}" by auto + +lemma subset_If: "(P \ X \ A) \ (\P \ X \ B) \ X \ (if P then A else B)" + by simp + +lemma not_in_imsupp_same: "z \ imsupp f \ f z = z" + unfolding imsupp_def supp_def by blast +lemma not_in_imsupp_same2: "z \ imsupp f \ imsupp g \ f z = g z" + using not_in_imsupp_same by (metis UnCI) +lemma Diff_image_not_in_imsupp: "(\x. x \ B \ x \ imsupp f) \ f ` A - B = f ` (A - B)" + unfolding supp_def imsupp_def by fastforce +lemma ball_not_eq_imsupp: "x \ B \ x \ A \ (\x. x \ B \ x \ imsupp f) \ \xa\A. x \ f xa" + unfolding imsupp_def supp_def by fastforce + +definition compSS :: "('a \ 'a) \ ('a \ 'a) \ ('a \ 'a)" where + "compSS f g \ f \ g \ inv f" + +lemma compSS_comp0: + fixes f g h::"'a \ 'a" + assumes "infinite (UNIV::'a set)" "bij f" "|supp f| compSS g) h = compSS (f \ g) h" +proof - + have "|supp (g \ h \ inv g)| 'a" + assumes "bij f" "|supp p| a. a \ imsupp p \ f a = a" + shows "compSS f p = p" +proof - + have 1: "imsupp f \ imsupp p = {}" + by (meson Int_emptyI assms(1) bij_imsupp_supp_ne cong not_in_supp_alt) + then show ?thesis unfolding compSS_def using imsupp_commute + by (metis assms(1) bij_is_surj inv_inv_eq o_inv_o_cancel surj_imp_inj_inv) +qed + +lemma imsupp_compSS: + fixes f::"'a \ 'a" + assumes "infinite (UNIV::'a set)" "bij f" "|supp f| g (h z) = h z \ (f \ g \ h) z = h z" + by simp + +(* tvsubst helper lemmas *) +lemma bij_not_eq_twice: "bij g \ g a \ a \ g (g a) \ g a" + by simp +lemma bij_not_equal_iff: "bij f \ a \ b \ f a \ f b" + by simp +lemma bij_id_imsupp: "bij f \ f a = a \ a \ imsupp f" + unfolding imsupp_def supp_def + by (simp add: bij_inv_eq_iff image_in_bij_eq) +lemma id_o_commute: "id \ f = f \ id" by simp +lemma fst_o_f: "fst \ (\(x, y). (f x, g x y)) = f \ fst" + by auto +lemma exists_fresh: "|A::'a set| \a::'a. a \ A" + by (metis UNIV_eq_I ordLess_irreflexive) +lemma swap_fresh: "y \ A \ x \ id(x := y, y := x) ` A \ False" + by auto +lemma forall_in_eq_UNIV: "\c. (c::'a) \ X \ X = (UNIV :: 'a set)" by blast +lemma image_const: "a \ X \ \c. c \ (\_. c) ` X" by simp +lemma ordIso_ordLess_False: "a =o b \ a False" + by (simp add: not_ordLess_ordIso) +lemma Union_UN_swap: "\ (\x\A. P x) = (\x\A. \(P x))" by blast +lemma UN_cong: "(\x. x \ A \ P x = Q x) \ \(P ` A) = \(Q ` A)" by simp +lemma supp_swap_bound: "infinite (UNIV :: 'a set) \ |supp (id (x := y, y := x :: 'a))| (f ` {a}) = f a" by simp + +lemma disjointI: "(\x. x \ A \ x \ B) \ A \ B = {}" + by blast +lemma notin_empty_eq_True: "x \ {} = True" + by simp +lemma disjoint_single: "{x} \ A = {} \ x \ A" + by blast + +lemma finite_singleton: "finite {x}" by blast + +lemma ex_avoiding_bij: + fixes f :: "'a \ 'a" and I D A :: "'a set" + assumes "|supp f| A = {}" "|A| (g::'a \ 'a). bij g \ |supp g| imsupp g \ A = {} \ + (\a. a \ (imsupp f - A) \ D \ f a \ A \ g a = f a) \ id_on I g" + apply (rule exI[of _ "avoiding_bij f I D A"]) + apply (rule conjI avoiding_bij assms)+ + done + +lemma id_on_empty: "id_on {} f" + unfolding id_on_def by simp + +lemma image_Int_empty: "bij f \ f ` A \ B = {} \ A \ inv f ` B = {}" + by force +lemma eq_bij_betw_refl_prems: + assumes "eq_bij_betw_refl r u w g A B x y f1 f2 L R" + shows "bij u" "|supp u| g (A x) = {} \ imsupp w \ g (B y) = {}" + using assms unfolding eq_bij_betw_refl_def by auto +lemma eq_bij_betw_prems: + assumes "eq_bij_betw r u w g A B x y f1 f2 h L R" + shows "bij u" "|supp u| id_on B g \ A = B \ x \ A \ f x = g x" + unfolding id_on_def by simp + +lemma notin_supp: "x \ supp f \ f x = x" + unfolding supp_def by blast + +lemmas imsupp_id_empty = trans[OF arg_cong2[OF imsupp_id refl, of "(\)"] Int_empty_left] + +lemma pred_fun_If: "pred_fun P Q f \ pred_fun P Q (\x. if P x then f x else undefined)" + by simp +lemma snd_comp_mk_prod: "snd \ (\x. (g x, f x)) = f" + by auto + +lemma supp_id_bound_cmin: "Card_order r \ |supp (id::'a \ _)| |supp (id::'a \ _)| A = {} \ A \ f ` B = {} \ A \ B = {}" + unfolding imsupp_def supp_def by (smt (verit) UnCI disjoint_iff image_iff mem_Collect_eq) + +lemma Collect_prod_beta: "{(x, y). P x y} = {p. P (fst p) (snd p)}" + by auto + +lemma prod_sets_simps: + "\(Basic_BNFs.fsts ` A) = fst ` A" + "\(Basic_BNFs.snds ` A) = snd ` A" + by force+ + +lemmas induct_impliesI = impI[unfolded HOL.induct_implies_def[symmetric]] +lemmas induct_impliesE = impE[unfolded HOL.induct_implies_def[symmetric]] +lemmas induct_mp = mp[unfolded HOL.induct_implies_def[symmetric]] +lemmas induct_conjI = conjI[unfolded HOL.induct_conj_def[symmetric]] +lemmas induct_forallI = allI[unfolded HOL.induct_forall_def[symmetric]] + +lemma induct_equal_refl: "HOL.induct_equal x x" + unfolding HOL.induct_equal_def by (rule refl) + +ML_file \../Tools/mrbnf_fp_tactics.ML\ +ML_file \../Tools/mrbnf_fp_def_sugar.ML\ +ML_file \../Tools/mrbnf_fp.ML\ + +ML_file \../Tools/mrbnf_recursor_tactics.ML\ +ML_file \../Tools/mrbnf_recursor.ML\ + +end diff --git a/thys/MRBNF_Recursor.thy b/thys/MRBNF_Recursor.thy index d1d9c84e..81ab02b3 100644 --- a/thys/MRBNF_Recursor.thy +++ b/thys/MRBNF_Recursor.thy @@ -1,348 +1,14 @@ theory MRBNF_Recursor - imports "MRBNF_Composition" - (*keywords "binder_inductive" :: thy_goal*) + imports MRBNF_FP begin -lemma card_of_subset_bound: "\ B \ A ; |A| \ |B| |A - B| o |UNIV::'b set|" "|U \ S::'b set| B. U \ B = {} \ B \ S = {} \ |U| =o |B|" -proof - - have 1: "|U| S)| =o |UNIV::'b set|" - using card_of_Un_diff_infinite[OF - cinfinite_imp_infinite[OF cinfinite_mono[OF assms(2) conjunct1[OF assms(1)]]] - ordLess_ordLeq_trans[OF assms(3,2)] - ] - by (simp add: Compl_eq_Diff_UNIV) - then have "|U| S)|" using ordLess_ordLeq_trans[OF 1 assms(2)] ordIso_symmetric ordLess_ordIso_trans by fast - then obtain B where 1: "B \ -(U \ S)" "|U| =o |B|" - by (meson internalize_card_of_ordLeq2 ordLess_imp_ordLeq) - then have "U \ B = {}" "B \ S = {}" by blast+ - then show ?thesis using 1 by blast -qed - -lemma exists_suitable_aux: - assumes "Cinfinite r" "r \o |UNIV::'a set|" "P \ |U \ (S - U)::'a set| (u::'a \ 'a). P \ bij u \ |supp u| imsupp u \ (S - U) = {} \ u ` U \ S = {}" -proof - - have 1: "P \ |U| U \ B = {}" "P \ B \ (S - U) = {}" "P \ |U| =o |B|" - using exists_subset_compl[OF assms(1,2,3)] by blast - obtain u where 3: "bij u" "P \ |supp u| bij_betw u U B" "P \ imsupp u \ (S - U) = {}" - using ordIso_ex_bij_betw_supp[OF assms(1) 1 2(3,1) Diff_disjoint 2(2)] by blast - then have "P \ u ` U \ B" unfolding bij_betw_def by blast - then have "P \ u ` U \ S = {}" using 2 by blast - then show ?thesis using 3 by blast -qed - -lemma fst_comp_map_prod: "h \ fst = fst \ map_prod h id" by auto - -lemma imsupp_same_subset: "\ a \ B ; a \ A ; imsupp f \ A \ B \ \ f a = a" - unfolding imsupp_def supp_def by blast - -lemma arg_cong3: "\ a1 = a2 ; b1 = b2 ; c1 = c2 \ \ h a1 b1 c1 = h a2 b2 c2" - by simp - -definition eq_bij_betw where - "eq_bij_betw r u w g A B x y f1 f2 h L R \ - bij u \ |supp u| imsupp u \ g (A x) = {} \ u ` f1 (A x) \ f1 (A x) = {} - \ bij w \ |supp w| imsupp w \ g (B y) = {} \ w ` f1 (B y) \ f1 (B y) = {} - \ eq_on (f2 y) (u \ L \ h) (w \ R)" - -lemma exists_bij_betw: - fixes L R h::"'a \ 'a" - assumes "Cinfinite r" "r \o |UNIV::'a set|" "bij R" "bij L" "bij h" "f2 x = h ` f2 y" - and u: "|f1 (A x) \ g (A x)::'a set| g (A x) = {}" "f1 (A x) = L ` f2 x" - and w: "|(f1 (B y)) \ (g (B y))::'a set| g (B y) = {}" "f1 (B y) = R ` f2 y" - shows "\(u::'a \ 'a) (w::'a \ 'a). - bij u \ |supp u| imsupp u \ g (A x) = {} \ u ` f1 (A x) \ f1 (A x) = {} - \ bij w \ |supp w| imsupp w \ g (B y) = {} \ w ` f1 (B y) \ f1 (B y) = {} - \ eq_on (f2 y) (u \ L \ h) (w \ R)" -proof - - have 1: "|f1 (A x)| g (A x) \ f1 (B y) \ g (B y)| -?A" "|f1 (A x)| =o |C|" - using ordLess_imp_ordLeq[THEN iffD1[OF internalize_card_of_ordLeq2]] by metis - then have 3: "f1 (A x) \ C = {}" "C \ g (A x) = {}" "f1 (B y) \ C = {}" "C \ g (B y) = {}" by blast+ - - obtain u::"'a \ 'a" where x: "bij u" "|supp u| g (A x) = {}" - using ordIso_ex_bij_betw_supp[OF assms(1) 1(1) C(2) 3(1) u(2) 3(2)] by blast - - have "bij_betw (inv R) (f1 (B y)) (f2 y)" unfolding bij_betw_def by (simp add: assms(3) inj_on_def w(3)) - moreover have "bij_betw h (f2 y) (f2 x)" using bij_imp_bij_betw assms(5,6) by auto - moreover have "bij_betw L (f2 x) (f1 (A x))" unfolding bij_betw_def by (simp add: assms(4) inj_on_def u(3)) - ultimately have 4: "bij_betw (u \ L \ h \ inv R) (f1 (B y)) C" using bij_betw_trans x(3) by blast - - obtain w::"'a \ 'a" where y: "bij w" "|supp w| g (B y) = {}" "eq_on (f1 (B y)) w (u \ L \ h \ inv R)" - using ex_bij_betw_supp[OF assms(1) 1(2) 4 3(3) w(2) 3(4)] by blast - - have "eq_on (f2 y) (u \ L \ h) (w \ R)" using y(5) unfolding eq_on_def using assms(3) w(3) by auto - moreover have "u ` f1 (A x) \ f1 (A x) = {}" "w ` f1 (B y) \ f1 (B y) = {}" using bij_betw_imp_surj_on x(3) y(3) 3(1,3) by blast+ - ultimately show ?thesis using x(1,2,4) y(1,2,4) by blast -qed - -lemmas exists_bij_betw_def = exists_bij_betw[unfolded eq_bij_betw_def[symmetric]] - -definition eq_bij_betw_refl where - "eq_bij_betw_refl r u w g A B x y f1 f2 L R \ - bij u \ |supp u| imsupp u \ g (A x) = {} \ u ` f1 (A x) \ f1 (A x) = {} - \ bij w \ |supp w| imsupp w \ g (B y) = {} \ w ` f1 (B y) \ f1 (B y) = {} - \ eq_on f2 (u \ L) (w \ R)" - -lemmas exists_bij_betw_refl = exists_bij_betw[OF _ _ _ _ bij_id image_id[symmetric], unfolded o_id] -lemmas exists_bij_betw_refl_UNIV = exists_bij_betw_refl[OF conjI[OF iffD2[OF cinfinite_iff_infinite] card_of_Card_order] ordLeq_refl[OF card_of_Card_order]] - -lemmas exists_bij_betw_refl_def = exists_bij_betw_refl[unfolded eq_bij_betw_refl_def[symmetric]] - -lemma imsupp_id_on: "imsupp u \ A = {} \ id_on A u" - unfolding imsupp_def supp_def id_on_def by blast - -lemma imsupp_image_subset: "u ` A \ A = {} \ A \ imsupp u" - unfolding imsupp_def supp_def by auto - -lemma Int_subset_empty1: "A \ B = {} \ C \ A \ C \ B = {}" by blast -lemma Int_subset_empty2: "A \ B = {} \ C \ B \ A \ C = {}" by blast -lemma exists_map_prod_id: "(a, b) \ map_prod f id ` A \ \c. (c, b) \ A \ a = f c" by auto - -lemma image_prod_f_g: "(a, b) \ (\x. (u x, g (u x))) ` A \ a \ u ` A \ b = g a" by blast -lemma Int_Un_empty: "A \ (B \ C \ D) = {} \ A \ B = {} \ A \ (C \ D) = {}" by blast - -lemma image_prod_f_g': "(a, b) \ (\x. (w x, g x)) ` A = (\x. x \ A \ a = w x \ b = g x)" by blast -lemma inv_id_middle: "bij u \ inv w (g (u z)) = u z \ (inv u \ (inv w \ g \ u)) z = id z" by simp -lemma inv_id_middle2: "bij R \ bij g \ (g \ R) z2 = (u \ L) z2 \ (inv R \ (inv g \ u \ L)) z2 = id z2" - by (metis bij_inv_eq_iff comp_apply id_apply) - -lemma eq_onD: "eq_on A u w \ z \ A \ u z = w z" - unfolding eq_on_def by blast - -lemma comp_pair: - "(\(a, b). (a, u a b)) \ (\t. (g t, w t)) = (\t. (g t, u (g t) (w t)))" - "(\(a, b). (z a, u a b)) \ (\t. (g t, w t)) = (\t. (z (g t), u (g t) (w t)))" - by auto - -lemma bij_if: "bij g \ bij (if P then id else g)" by simp -lemma supp_if: "|supp (u::'a \ 'a)| |supp (if P then id else u)| |supp u| |supp (if P then id else u)| A = {} \ imsupp (if P then id else u) \ A = {}" unfolding imsupp_def supp_def by simp -lemma image_if_empty: "u ` A \ B = {} \ (P \ A \ B = {}) \ (if P then id else u) ` A \ B = {}" by simp - -lemma Int_Un_emptyI1: "A \ (B \ C) = {} \ A \ B = {}" by blast -lemma Int_Un_emptyI2: "A \ (B \ C) = {} \ A \ C = {}" by blast - -lemma imsupp_comp_image: "bij f \ imsupp (f \ g \ inv f) = f ` imsupp g" - apply (auto simp: supp_def imsupp_def bij_inv_eq_iff image_in_bij_eq) - by (smt (verit, del_insts) imageI inv_simp1 mem_Collect_eq) - -lemma id_on_comp3: "c z = z \ b (c z) = c z \ a z = z \ (a \ b \ c) z = z" - by simp -lemma id_on_comp2: "b z = z \ a z = z \ (a \ b) z = z" by simp -lemma id_on_both: "a z = z \ b z = z \ a z = b z" by simp - -lemma not_imageI: "bij f \ a \ A \ f a \ f ` A" by force - -lemma Un_bound: - assumes inf: "infinite (UNIV :: 'a set)" - and "|A1| A2| |imsupp g| |supp g| imsupp f \ A" - unfolding imsupp_def supp_def by auto - -lemma Un_mono': "A \ C \ X \ B \ D \ X \ A \ B \ C \ D \ X" by blast -lemma Diff_Un_disjunct: "B \ C = {} \ A - B \ C = (A \ C) - B" by blast -lemma UN_empty': "A = {} \ \ (B ` A) = {}" by auto - -lemma subset_If: "(P \ X \ A) \ (\P \ X \ B) \ X \ (if P then A else B)" - by simp - -lemma not_in_imsupp_same: "z \ imsupp f \ f z = z" - unfolding imsupp_def supp_def by blast -lemma not_in_imsupp_same2: "z \ imsupp f \ imsupp g \ f z = g z" - using not_in_imsupp_same by (metis UnCI) -lemma Diff_image_not_in_imsupp: "(\x. x \ B \ x \ imsupp f) \ f ` A - B = f ` (A - B)" - unfolding supp_def imsupp_def by fastforce -lemma ball_not_eq_imsupp: "x \ B \ x \ A \ (\x. x \ B \ x \ imsupp f) \ \xa\A. x \ f xa" - unfolding imsupp_def supp_def by fastforce - -definition compSS :: "('a \ 'a) \ ('a \ 'a) \ ('a \ 'a)" where - "compSS f g \ f \ g \ inv f" - -lemma compSS_comp0: - fixes f g h::"'a \ 'a" - assumes "infinite (UNIV::'a set)" "bij f" "|supp f| compSS g) h = compSS (f \ g) h" -proof - - have "|supp (g \ h \ inv g)| 'a" - assumes "bij f" "|supp p| a. a \ imsupp p \ f a = a" - shows "compSS f p = p" -proof - - have 1: "imsupp f \ imsupp p = {}" - by (meson Int_emptyI assms(1) bij_imsupp_supp_ne cong not_in_supp_alt) - then show ?thesis unfolding compSS_def using imsupp_commute - by (metis assms(1) bij_is_surj inv_inv_eq o_inv_o_cancel surj_imp_inj_inv) -qed - -lemma imsupp_compSS: - fixes f::"'a \ 'a" - assumes "infinite (UNIV::'a set)" "bij f" "|supp f| g (h z) = h z \ (f \ g \ h) z = h z" - by simp - -(* tvsubst helper lemmas *) -lemma bij_not_eq_twice: "bij g \ g a \ a \ g (g a) \ g a" - by simp -lemma bij_not_equal_iff: "bij f \ a \ b \ f a \ f b" - by simp -lemma bij_id_imsupp: "bij f \ f a = a \ a \ imsupp f" - unfolding imsupp_def supp_def - by (simp add: bij_inv_eq_iff image_in_bij_eq) -lemma id_o_commute: "id \ f = f \ id" by simp -lemma fst_o_f: "fst \ (\(x, y). (f x, g x y)) = f \ fst" - by auto -lemma exists_fresh: "|A::'a set| \a::'a. a \ A" - by (metis UNIV_eq_I ordLess_irreflexive) -lemma swap_fresh: "y \ A \ x \ id(x := y, y := x) ` A \ False" - by auto -lemma forall_in_eq_UNIV: "\c. (c::'a) \ X \ X = (UNIV :: 'a set)" by blast -lemma image_const: "a \ X \ \c. c \ (\_. c) ` X" by simp -lemma ordIso_ordLess_False: "a =o b \ a False" - by (simp add: not_ordLess_ordIso) -lemma Union_UN_swap: "\ (\x\A. P x) = (\x\A. \(P x))" by blast -lemma UN_cong: "(\x. x \ A \ P x = Q x) \ \(P ` A) = \(Q ` A)" by simp -lemma supp_swap_bound: "infinite (UNIV :: 'a set) \ |supp (id (x := y, y := x :: 'a))| (f ` {a}) = f a" by simp - -lemma disjointI: "(\x. x \ A \ x \ B) \ A \ B = {}" - by blast -lemma notin_empty_eq_True: "x \ {} = True" - by simp -lemma disjoint_single: "{x} \ A = {} \ x \ A" - by blast - -lemma finite_singleton: "finite {x}" by blast - -lemma ex_avoiding_bij: - fixes f :: "'a \ 'a" and I D A :: "'a set" - assumes "|supp f| A = {}" "|A| (g::'a \ 'a). bij g \ |supp g| imsupp g \ A = {} \ - (\a. a \ (imsupp f - A) \ D \ f a \ A \ g a = f a) \ id_on I g" - apply (rule exI[of _ "avoiding_bij f I D A"]) - apply (rule conjI avoiding_bij assms)+ - done - -lemma id_on_empty: "id_on {} f" - unfolding id_on_def by simp - -lemma image_Int_empty: "bij f \ f ` A \ B = {} \ A \ inv f ` B = {}" - by force -lemma eq_bij_betw_refl_prems: - assumes "eq_bij_betw_refl r u w g A B x y f1 f2 L R" - shows "bij u" "|supp u| g (A x) = {} \ imsupp w \ g (B y) = {}" - using assms unfolding eq_bij_betw_refl_def by auto -lemma eq_bij_betw_prems: - assumes "eq_bij_betw r u w g A B x y f1 f2 h L R" - shows "bij u" "|supp u| id_on B g \ A = B \ x \ A \ f x = g x" - unfolding id_on_def by simp - -lemma notin_supp: "x \ supp f \ f x = x" - unfolding supp_def by blast - -lemmas imsupp_id_empty = trans[OF arg_cong2[OF imsupp_id refl, of "(\)"] Int_empty_left] - -lemma pred_fun_If: "pred_fun P Q f \ pred_fun P Q (\x. if P x then f x else undefined)" - by simp -lemma snd_comp_mk_prod: "snd \ (\x. (g x, f x)) = f" - by auto - -lemma supp_id_bound_cmin: "Card_order r \ |supp (id::'a \ _)| |supp (id::'a \ _)| A = {} \ A \ f ` B = {} \ A \ B = {}" - unfolding imsupp_def supp_def by (smt (verit) UnCI disjoint_iff image_iff mem_Collect_eq) - -lemma Collect_prod_beta: "{(x, y). P x y} = {p. P (fst p) (snd p)}" - by auto - -lemma prod_sets_simps: - "\(Basic_BNFs.fsts ` A) = fst ` A" - "\(Basic_BNFs.snds ` A) = snd ` A" - by force+ - -lemmas induct_impliesI = impI[unfolded HOL.induct_implies_def[symmetric]] -lemmas induct_impliesE = impE[unfolded HOL.induct_implies_def[symmetric]] -lemmas induct_mp = mp[unfolded HOL.induct_implies_def[symmetric]] -lemmas induct_conjI = conjI[unfolded HOL.induct_conj_def[symmetric]] -lemmas induct_forallI = allI[unfolded HOL.induct_forall_def[symmetric]] - -lemma induct_equal_refl: "HOL.induct_equal x x" - unfolding HOL.induct_equal_def by (rule refl) - -ML_file \../Tools/mrbnf_fp_tactics.ML\ -ML_file \../Tools/mrbnf_fp_def_sugar.ML\ -ML_file \../Tools/mrbnf_fp.ML\ - -ML_file \../Tools/mrbnf_recursor_tactics.ML\ -ML_file \../Tools/mrbnf_recursor.ML\ - ML_file \../Tools/mrbnf_vvsubst.ML\ ML_file \../Tools/mrbnf_tvsubst.ML\ ML_file \../Tools/mrbnf_sugar.ML\ -(*ML_file \../Tools/binder_inductive.ML\*) - context begin ML_file \../Tools/binder_induction.ML\ end -end +end \ No newline at end of file diff --git a/thys/System_Fc/SystemF.thy b/thys/System_Fc/SystemF.thy index bf91b4d9..23e42e5a 100644 --- a/thys/System_Fc/SystemF.thy +++ b/thys/System_Fc/SystemF.thy @@ -33,6 +33,11 @@ val tyspec = { } \ +ML_file \../../Tools/mrbnf_sugar.ML\ +ML \ +Multithreading.parallel_proofs := 0 +\ + declare [[mrbnf_internals]] local_setup \fn lthy => let From 2821494d35fbbff335e985e91e6a9dda57208932 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Tue, 5 Mar 2024 17:14:03 +0000 Subject: [PATCH 2/7] Allow passive positions and mutual recursion for tvsubst axioms and constants --- Tools/mrbnf_tvsubst.ML | 578 ++++++++++++++++++++----------------- operations/Sugar.thy | 52 +++- operations/TVSubst.thy | 1 - thys/System_Fc/SystemF.thy | 51 +++- 4 files changed, 412 insertions(+), 270 deletions(-) diff --git a/Tools/mrbnf_tvsubst.ML b/Tools/mrbnf_tvsubst.ML index 356bbc00..a01a1f69 100644 --- a/Tools/mrbnf_tvsubst.ML +++ b/Tools/mrbnf_tvsubst.ML @@ -8,7 +8,7 @@ sig }; type 'a tvsubst_model = { - fp_result: MRBNF_FP_Def_Sugar.fp_result, + binding: binding, etas: (term * 'a eta_axioms) option list }; @@ -22,8 +22,9 @@ sig tvsubst_cctor_not_isVVr: thm }; - val create_tvsubst_of_mrbnf: binding -> (binding -> binding) -> (Proof.context -> tactic) tvsubst_model - -> local_theory -> tvsubst_result * local_theory + val create_tvsubst_of_mrbnf: (binding -> binding) -> MRBNF_FP_Def_Sugar.fp_result + -> (Proof.context -> tactic) tvsubst_model list -> local_theory + -> tvsubst_result * local_theory end structure MRBNF_TVSubst : MRBNF_TVSUBST = @@ -42,7 +43,7 @@ type 'a eta_axioms = { }; type 'a tvsubst_model = { - fp_result: MRBNF_FP_Def_Sugar.fp_result, + binding: binding, etas: (term * 'a eta_axioms) option list }; @@ -58,283 +59,331 @@ type tvsubst_result = { val names = map (fst o dest_Free); -fun prove_model_axioms binding qualify (model : (Proof.context -> tactic) tvsubst_model) lthy = +fun prove_model_axioms qualify res (models : (Proof.context -> tactic) tvsubst_model list) lthy = let - val eta_names = lthy - |> mk_Frees "\" (map_filter (Option.map (fastype_of o fst)) (#etas model)) + val eta_namess = lthy + |> mk_Freess "\" (map (map_filter (Option.map (fastype_of o fst)) o #etas) models) |> fst - |> map (fst o dest_Free) - |> map (fn s => s ^ "_" ^ short_type_name (fst (dest_Type (#T (hd (#quotient_fps (#fp_result model))))))); - val eta_names_opt = fst (fold_map (fn x => fn names => case x of - SOME _ => (SOME (hd names), tl names) - | NONE => (NONE, names) - ) (#etas model) eta_names); - val mrbnf = hd (#pre_mrbnfs (#fp_result model)); - val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf - val (etas, (_, lthy)) = @{fold_map 3} (fn set => fn eta_opt => fn eta_name => fn (i, lthy) => let val eta_opt' = Option.map (fn (eta, tacs) => - let - val (aT, preT) = dest_funT (fastype_of eta); - val args = snd (dest_Type preT); - val old_vars = rev (map TVar (Term.add_tvars set []) @ map TFree (Term.add_tfrees set [])); - val set' = Term.subst_atomic_types (old_vars ~~ args) set; - val vars = fold (Term.add_tfreesT) args []; - - val (args_live, args_rest) = fold_rev ( - fn (MRBNF_Def.Live_Var, x) => (fn (a, b) => (x::a, b)) - | (_, x) => fn (a, b) => (a, x::b) - ) (var_types ~~ args) ([], []); - - val names_lthy = fold (Variable.declare_constraints o Logic.mk_type o TFree) vars lthy; - val ((((a, b), x), Bs), names_lthy) = names_lthy - |> apfst hd o mk_Frees "a" [aT] - ||>> apfst hd o mk_Frees "b" [aT] - ||>> apfst hd o mk_Frees "x" [preT] - ||>> mk_TFrees (length args_live); - - val live_Ts = map2 (curry op-->) args_live Bs; - val fTs = cond_interlace live_Ts (map (fn T => T --> T) args_rest) - (map (fn MRBNF_Def.Live_Var => true | _ => false) var_types); - - val (fs, _) = names_lthy - |> mk_Frees "f" fTs; - - val lthy = snd (Local_Theory.begin_nested lthy); - val (raw_eta, lthy) = mk_def_t false binding qualify (the eta_name) 0 eta lthy - val (lthy, old_lthy) = `Local_Theory.end_nested lthy; - val phi = Proof_Context.export_morphism old_lthy lthy; - - val eta' = Morphism.term phi (fst raw_eta); - val vars = snd (dest_Type (range_type (fastype_of eta'))); - val eta = (Term.subst_atomic_types (vars ~~ args) eta', Morphism.thm phi (snd raw_eta)); - - val eta_free = Goal.prove_sorry lthy (names [a]) [] - (mk_Trueprop_eq (set' $ (fst eta $ a), mk_singleton a)) - (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_free tacs context); - - val eta_inj = Goal.prove_sorry lthy (names [a, b]) [] - (Logic.mk_implies (mk_Trueprop_eq (fst eta $ a, fst eta $ b), mk_Trueprop_eq (a, b))) - (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_inj tacs context); - - val eta_compl_free = Goal.prove_sorry lthy [] [] - (Logic.all x (Logic.mk_implies ( - HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_mem ( - x, mk_image (fst eta) $ HOLogic.mk_UNIV aT - ))), - mk_Trueprop_eq (set' $ x, mk_bot aT) - ))) - (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_compl_free tacs context); - - val f_types = var_types ~~ fs; - val f_prems = maps ( - fn (MRBNF_Def.Free_Var, f) => [mk_supp_bound f] - | (MRBNF_Def.Bound_Var, f) => [mk_bij f, mk_supp_bound f] - | _ => [] - ) f_types; - val (free_fs, bound_fs, live_fs) = fold_rev ( - fn (MRBNF_Def.Free_Var, x) => (fn (a, b, c) => (x::a, b, c)) - | (MRBNF_Def.Bound_Var, x) => (fn (a, b, c) => (a, x::b, c)) - | (_, x) => (fn (a, b, c) => (a, b, x::c)) - ) f_types ([], [], []); - - val eta' = + |> map (map (fst o dest_Free)) + |> map2 (fn quot => map (fn s => s ^ "_" ^ short_type_name (fst (dest_Type (#T quot))))) (#quotient_fps res); + + val eta_names_opts = map2 (fn model => fn eta_names => + fst (fold_map (fn x => fn names => case x of + SOME _ => (SOME (hd names), tl names) + | NONE => (NONE, names) + ) (#etas model) eta_names) + ) models eta_namess; + + val mrbnfs = #pre_mrbnfs res; + val nvars = length (#binding_relation res); + val pfree = MRBNF_Def.free_of_mrbnf (hd mrbnfs) - nvars; + val plive = MRBNF_Def.live_of_mrbnf (hd mrbnfs) - foldl1 (op+) (#rec_vars res); + val pbound = MRBNF_Def.bound_of_mrbnf (hd mrbnfs) - nvars; + + val (etass, lthy) = @{fold_map 3} (fn model => fn mrbnf => fn eta_names_opt => fn lthy => + let val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf in apsnd snd ( + @{fold_map 3} (fn set => fn eta_opt => fn eta_name => fn (i, lthy) => let val eta_opt' = Option.map (fn (eta, tacs) => let - val (n, T) = dest_Const (fst eta); - val (n2, Ts) = dest_Type (range_type T); - val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf; - val Ts' = fst (fold_map (fn (var, ty) => fn acc => case var of - MRBNF_Def.Live_Var => (hd acc, tl acc) - | _ => (ty, acc) - ) (var_types ~~ Ts) Bs); - in Const (n, domain_type T --> Type (n2, Ts')) end; - val eta_natural = Goal.prove_sorry lthy (names fs) [] - (fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop) f_prems (mk_Trueprop_eq ( - HOLogic.mk_comp ( - MRBNF_Def.mk_map_comb_of_mrbnf (MRBNF_Def.deads_of_mrbnf mrbnf) live_fs bound_fs free_fs mrbnf, - fst eta - ), - HOLogic.mk_comp (eta', nth free_fs i) - ))) - (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_natural tacs context); - in ((eta, { - eta_free = eta_free, - eta_inj = eta_inj, - eta_compl_free = eta_compl_free, - eta_natural = eta_natural - }), lthy) end - ) eta_opt in (Option.map fst eta_opt', (i + 1, the_default lthy (Option.map snd eta_opt'))) end) - (map_filter (fn (MRBNF_Def.Free_Var, set) => SOME set | _ => NONE) ( - var_types ~~ MRBNF_Def.sets_of_mrbnf mrbnf - )) (#etas model) eta_names_opt (0, lthy); - - val vars_opt = map (Option.map (fst o dest_funT o fastype_of o fst)) (#etas model); - val vars = map_filter (Option.map dest_TFree) vars_opt; - val names_lthy = fold (Variable.declare_constraints o Logic.mk_type o TFree) vars lthy; - val n = MRBNF_Def.free_of_mrbnf mrbnf - length vars; - val (Ts, _) = names_lthy - |> mk_TFrees' (replicate n (MRBNF_Def.class_of_mrbnf mrbnf)); - val var_T = #T (hd (#quotient_fps (#fp_result model))); - val old_vars = map TVar (rev (Term.add_tvarsT var_T [])) @ map TFree (rev (Term.add_tfreesT var_T [])); - val new_vars = fst (fold_map (fn SOME a => (fn xs => (a, xs)) | NONE => fn xs => (hd xs, tl xs)) vars_opt Ts); - - in (map_filter (Option.map (snd o fst)) etas, { - fp_result = MRBNF_FP_Def_Sugar.substitute_vars (old_vars ~~ new_vars) (#fp_result model), - etas = map (Option.map (apfst fst)) etas - } : thm tvsubst_model, lthy) end; - -fun define_tvsubst_consts b qualify (model : thm tvsubst_model) lthy = + val (aT, preT) = dest_funT (fastype_of eta); + val args = snd (dest_Type preT); + val old_vars = rev (map TVar (Term.add_tvars set []) @ map TFree (Term.add_tfrees set [])); + val set' = Term.subst_atomic_types (old_vars ~~ args) set; + val vars = rev (fold (Term.add_tfreesT) args []); + + val (((((frees, pfrees), plives), pbounds), bounds), rec_vars) = args + |> chop nvars + ||>> chop pfree + ||>> chop plive + ||>> chop pbound + ||>> chop nvars; + + val names_lthy = fold (Variable.declare_constraints o Logic.mk_type o TFree) vars lthy; + val ((((a, b), x), Bs), names_lthy) = names_lthy + |> apfst hd o mk_Frees "a" [aT] + ||>> apfst hd o mk_Frees "b" [aT] + ||>> apfst hd o mk_Frees "x" [preT] + ||>> mk_TFrees (length rec_vars); + + val fTs = map (fn a => a --> a) (frees @ bounds) @ map2 (curry op-->) rec_vars Bs; + + val ((free_fs, bound_fs), live_fs) = names_lthy + |> mk_Frees "f" fTs + |> fst + |> chop nvars + ||>> chop nvars; + val fs = free_fs @ bound_fs @ live_fs; + + val lthy = snd (Local_Theory.begin_nested lthy); + val (raw_eta, lthy) = mk_def_t false (#binding model) qualify (the eta_name) 0 eta lthy + val (lthy, old_lthy) = `Local_Theory.end_nested lthy; + val phi = Proof_Context.export_morphism old_lthy lthy; + + val eta' = Morphism.term phi (fst raw_eta); + val vars = snd (dest_Type (range_type (fastype_of eta'))); + val eta = (Term.subst_atomic_types (vars ~~ args) eta', Morphism.thm phi (snd raw_eta)); + + val eta_free = Goal.prove_sorry lthy (names [a]) [] + (mk_Trueprop_eq (set' $ (fst eta $ a), mk_singleton a)) + (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_free tacs context); + + val eta_inj = Goal.prove_sorry lthy (names [a, b]) [] + (Logic.mk_implies (mk_Trueprop_eq (fst eta $ a, fst eta $ b), mk_Trueprop_eq (a, b))) + (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_inj tacs context); + + val eta_compl_free = Goal.prove_sorry lthy [] [] + (Logic.all x (Logic.mk_implies ( + HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_mem ( + x, mk_image (fst eta) $ HOLogic.mk_UNIV aT + ))), + mk_Trueprop_eq (set' $ x, mk_bot aT) + ))) + (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_compl_free tacs context); + + val f_prems = map mk_supp_bound free_fs @ maps (fn f => [mk_bij f, mk_supp_bound f]) bound_fs; + + val eta' = + let + val (n, T) = dest_Const (fst eta); + val (n2, _) = dest_Type (range_type T); + val Ts' = frees @ pfrees @ plives @ pbounds @ bounds @ Bs; + in Const (n, domain_type T --> Type (n2, Ts')) end; + val eta_natural = Goal.prove_sorry lthy (names fs) [] + (fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop) f_prems (mk_Trueprop_eq ( + HOLogic.mk_comp ( + MRBNF_Def.mk_map_comb_of_mrbnf (MRBNF_Def.deads_of_mrbnf mrbnf) + (map HOLogic.id_const plives @ live_fs) + (map HOLogic.id_const pbounds @ bound_fs) + (free_fs @ map HOLogic.id_const pfrees) mrbnf, + fst eta + ), + HOLogic.mk_comp (eta', nth free_fs i) + ))) + (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_natural tacs context); + in ((eta, { + eta_free = eta_free, + eta_inj = eta_inj, + eta_compl_free = eta_compl_free, + eta_natural = eta_natural + }), lthy) end + ) eta_opt in (Option.map fst eta_opt', (i + 1, the_default lthy (Option.map snd eta_opt'))) end) + (take nvars (map_filter (fn (MRBNF_Def.Free_Var, set) => SOME set | _ => NONE) ( + var_types ~~ MRBNF_Def.sets_of_mrbnf mrbnf + ))) (#etas model) eta_names_opt (0, lthy) + ) end + ) models mrbnfs eta_names_opts lthy; + + val sort = foldl1 (Sign.inter_sort (Proof_Context.theory_of lthy)) ( + map MRBNF_Def.class_of_mrbnf mrbnfs + ); + val (Ts, _) = mk_TFrees' ( + replicate (nvars + pfree) sort @ replicate plive @{sort type} @ replicate pbound sort + ) lthy; + val ctor = #ctor (hd (#quotient_fps res)); + val vars = rev (Term.add_tvars ctor []); + val res = MRBNF_FP_Def_Sugar.substitute_vars (map TVar vars ~~ Ts) res + val ctor = #ctor (hd (#quotient_fps res)); + val args = snd (dest_Type (domain_type (fastype_of ctor))); + + val etass = map (map (Option.map (fn ((eta, eta_def), thms) => + let + val Ts' = snd (dest_Type (range_type (fastype_of eta))); + val eta' = Term.subst_atomic_types (Ts' ~~ args) eta; + in ((eta', eta_def), thms) end + ))) etass; + val Ts' = Ts + |> chop nvars + ||>> chop pfree + ||>> chop plive + + in (res, maps (map_filter (Option.map (snd o fst))) etass, Ts', + map2 (fn model => fn etas => { + binding = #binding model, + etas = map (Option.map (apfst fst)) etas + } : thm tvsubst_model) models etass, lthy + ) end; + +fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models : thm tvsubst_model list) lthy = let - val (_, lthy) = Local_Theory.begin_nested lthy; - val mk_def_public = mk_def_t true b (Binding.suffix_name ("_" ^ Binding.name_of b)); - val mk_def_t = mk_def_t false b qualify; - val quotient = hd (#quotient_fps (#fp_result model)); - val ctor = #ctor quotient; - val FVarss = #FVars quotient; - val rename = #rename quotient; - val vars = snd (dest_Type (body_type (fastype_of rename))); val nvars = length vars; - val (preT, qT) = dest_funT (fastype_of ctor); - val suffix = case map_filter I (#etas model) of - [_] => map (Option.map (K "")) (#etas model) - | _ => fst (fold_map (fn eta_opt => fn i => case eta_opt of - NONE => (NONE, i) - | SOME _ => (SOME (string_of_int i), i + 1) - ) (#etas model) 1); - - val (defs, lthy) = @{fold_map 3} (fn eta_opt => fn suffix => fn i => fn lthy => let val opt = Option.map (fn (eta, _) => - let - val (eta_name, etaT) = dest_Const eta - val aT = fst (dest_funT etaT); - val eta' = Const (eta_name, aT --> preT); - val (VVr, lthy) = mk_def_t ("VVr" ^ the suffix) 0 (HOLogic.mk_comp (ctor, eta')) lthy; - - val ((h, t), _) = lthy - |> apfst hd o mk_Frees "f" [aT --> qT] - ||>> apfst hd o mk_Frees "t" [qT]; - - val (SSupp, lthy) = mk_def_public ("SSupp" ^ the suffix) 1 (Term.absfree (dest_Free h) ( - HOLogic.mk_Collect ("a", aT, HOLogic.mk_not (HOLogic.mk_eq ( - h $ Bound 0, fst VVr $ Bound 0 - ))) - )) lthy; - - val (IImsupps, lthy) = @{fold_map 2} (fn FVars => fn s => mk_def_public ("IImsupp" ^ the suffix ^ s) 1 ( - Term.absfree (dest_Free h) ( - let val UN = mk_UNION (fst SSupp $ h) (HOLogic.mk_comp (FVars, h)); - in if fastype_of (fst SSupp $ h) = range_type (fastype_of FVars) then - mk_Un (fst SSupp $ h, UN) - else UN end - ))) FVarss (if nvars = 1 then [""] else map string_of_int (1 upto nvars)) lthy; - - val (isVVr, lthy) = mk_def_t ("isVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( - HOLogic.mk_exists ("a", aT, HOLogic.mk_eq (t, fst VVr $ Bound 0)) - )) lthy; - - val (asVVr, lthy) = mk_def_t ("asVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( - BNF_FP_Util.mk_If (fst isVVr $ t) - (HOLogic.choice_const aT $ Term.abs ("a", aT) (HOLogic.mk_eq (fst VVr $ Bound 0, t))) - (BNF_GFP_Util.mk_undefined aT) - )) lthy; - - val (fs, _) = lthy - |> mk_Frees "f" (map (fn v => v --> v) vars); - - val (compSS, lthy) = mk_def_t ("compSS" ^ the suffix) nvars ( - fold_rev Term.absfree (map dest_Free fs) ( - Term.absfree (dest_Free h) (HOLogic.mk_comp ( - HOLogic.mk_comp ( - Term.list_comb (#rename quotient, fs), - h - ), - mk_inv (nth fs i) - )) - ) - ) lthy; - in ({ - aT = aT, - SSfun = fastype_of h, - VVr = VVr, - SSupp = SSupp, - IImsupps = IImsupps, - isVVr = isVVr, - asVVr = asVVr, - compSS = compSS - }, lthy) end - ) eta_opt in (Option.map fst opt, the_default lthy (Option.map snd opt)) end) - (#etas model) suffix (0 upto nvars - 1) lthy; - - val (name, args) = (dest_Type o fst o dest_funT o fastype_of) ctor; - val mrbnf = hd (#pre_mrbnfs (#fp_result model)); - val deads = MRBNF_Def.deads_of_mrbnf mrbnf; - val live = MRBNF_Def.live_of_mrbnf mrbnf; - val P_Ts = map_filter (Option.map #SSfun) defs; - val P_T = HOLogic.mk_tupleT P_Ts; - val live_T = HOLogic.mk_prodT (#T quotient, P_T --> #T quotient); - - val arg_types = (MRBNF_Def.var_types_of_mrbnf mrbnf ~~ args); - val new_args = map (fn (MRBNF_Def.Live_Var, _) => live_T | (_, arg) => arg) arg_types; - val ids = map HOLogic.id_const vars; - val map_id_fst = ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads - (replicate live (fst_const live_T)) ids ids mrbnf $ Bound (length P_Ts)); - - val (ps, _) = lthy - |> mk_Frees "p" P_Ts; - - val (Uctor, lthy) = mk_def_t "Uctor" 0 (Term.abs ("F", Type (name, new_args)) (mk_case_tuple (map dest_Free ps) ( - fold (fn (p, def) => BNF_FP_Util.mk_If (fst (#isVVr def) $ map_id_fst) - (p $ (fst (#asVVr def) $ map_id_fst)) - ) (ps ~~ map_filter I defs) (ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads - (replicate live (HOLogic.mk_comp ( - Term.abs ("R", P_T --> #T quotient) (Bound 0 $ HOLogic.mk_tuple ps), - snd_const live_T - ))) - ids ids mrbnf $ Bound (length P_Ts)) - )))) lthy; + val mk_def_t = MRBNF_Util.mk_def_t false (Binding.conglomerate (map #binding models)) qualify; + val mk_def_public = MRBNF_Util.mk_def_t true Binding.empty I; + + val suffixes = + let fun mk_ss s etas = case map_filter I etas of + [_] => map (Option.map (K s)) etas + | _ => fst (fold_map (fn eta_opt => fn i => case eta_opt of + NONE => (NONE, i) | SOME _ => (SOME (s ^ string_of_int i), i + 1) + ) etas 1); + in case models of + [m] => [mk_ss "" (#etas m)] + | _ => map2 (fn i => mk_ss (string_of_int i) o #etas) (1 upto length models) models + end; val (fs, _) = lthy |> mk_Frees "f" (map (fn a => a --> a) vars); + + val (_, lthy) = Local_Theory.begin_nested lthy; - val card = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); - val some_defs = map_filter I defs; - val (Pmap, lthy) = mk_def_t "Pmap" nvars (fold_rev Term.absfree (map dest_Free fs) ( - mk_case_tuple (map dest_Free ps) (HOLogic.mk_tuple (map2 (fn p => fn def => - Term.list_comb (fst (#compSS def), fs @ [p])) ps some_defs - )) - )) lthy; - val (valid_P, lthy) = mk_def_t "valid_P" 1 (mk_case_tuple (map dest_Free ps) ( - foldr1 HOLogic.mk_conj (map2 (fn def => fn t => - mk_ordLess (mk_card_of (fst (#SSupp def) $ t)) card - ) some_defs ps) - )) lthy; + val (consts, lthy) = @{fold_map 4} (fn mrbnf => fn quot => fn model => fn suffix => fn lthy => + let + val ctor = #ctor quot; + + val (defs, lthy) = @{fold_map 3} (fn eta_opt => fn suffix => fn i => fn lthy => let val opt = Option.map (fn (eta, _) => + let + val qT = #T quot; + val aT = domain_type (fastype_of eta); + val (VVr, lthy) = mk_def_t ("VVr" ^ the suffix) 0 (HOLogic.mk_comp (ctor, eta)) lthy; + + val ((h, t), _) = lthy + |> apfst hd o mk_Frees "f" [aT --> qT] + ||>> apfst hd o mk_Frees "t" [qT]; + + val (SSupp, lthy) = mk_def_public ("SSupp" ^ the suffix ^ "_" ^ Binding.name_of (#binding model)) + 1 (Term.absfree (dest_Free h) (HOLogic.mk_Collect ("a", aT, HOLogic.mk_not (HOLogic.mk_eq ( + h $ Bound 0, fst VVr $ Bound 0 + ))) + )) lthy; + + val (IImsupps, lthy) = @{fold_map 2} (fn FVars => fn s => mk_def_public ("IImsupp" ^ the suffix ^ "_" ^ s) 1 ( + Term.absfree (dest_Free h) ( + let val UN = mk_UNION (fst SSupp $ h) (HOLogic.mk_comp (FVars, h)); + in if fastype_of (fst SSupp $ h) = range_type (fastype_of FVars) then + mk_Un (fst SSupp $ h, UN) + else UN end + ))) (#FVars quot) (if nvars = 1 then [""] else map string_of_int (1 upto nvars)) lthy; + + val (isVVr, lthy) = mk_def_t ("isVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( + HOLogic.mk_exists ("a", aT, HOLogic.mk_eq (t, fst VVr $ Bound 0)) + )) lthy; + + val (asVVr, lthy) = mk_def_t ("asVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( + BNF_FP_Util.mk_If (fst isVVr $ t) + (HOLogic.choice_const aT $ Term.abs ("a", aT) (HOLogic.mk_eq (fst VVr $ Bound 0, t))) + (BNF_GFP_Util.mk_undefined aT) + )) lthy; + + val (fs, _) = lthy + |> mk_Frees "f" (map (fn v => v --> v) vars); + + val (compSS, lthy) = mk_def_t ("compSS" ^ the suffix) nvars ( + fold_rev Term.absfree (map dest_Free fs) ( + Term.absfree (dest_Free h) (HOLogic.mk_comp ( + HOLogic.mk_comp ( + Term.list_comb (#rename quot, fs), + h + ), + mk_inv (nth fs i) + )) + ) + ) lthy; + in ({ + aT = aT, + SSfun = fastype_of h, + VVr = VVr, + SSupp = SSupp, + IImsupps = IImsupps, + isVVr = isVVr, + asVVr = asVVr, + compSS = compSS + }, lthy) end + ) eta_opt in ( + Option.map fst opt, the_default lthy (Option.map snd opt)) + end) (#etas model) suffix (0 upto nvars - 1) lthy; + + val P_Ts = map_filter (Option.map #SSfun) defs; + val P_T = HOLogic.mk_tupleT P_Ts; + val (ps, _) = lthy + |> mk_Frees "p" P_Ts; + + val (name, (args, rec_args)) = dest_Type (fst (dest_funT (fastype_of ctor))) + |> apsnd (chop (nvars * 2 + length pfrees + length plives + length pbounds)); + val rec_args' = map (fn T => HOLogic.mk_prodT (T, P_T --> T)) rec_args; + val args = args @ rec_args'; + + val free_ids = map HOLogic.id_const (vars @ pfrees); + val bound_ids = map HOLogic.id_const (pbounds @ vars); + + val deads = MRBNF_Def.deads_of_mrbnf mrbnf; + val map_id_fst = ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads + (map HOLogic.id_const plives @ map fst_const rec_args') + bound_ids free_ids mrbnf $ Bound (length P_Ts)); + val mk_def_t = MRBNF_Util.mk_def_t false (#binding model) qualify + + val (Uctor, lthy) = mk_def_t "Uctor" 0 (Term.abs ("F", Type (name, args)) ( + mk_case_tuple (map dest_Free ps) (@{fold 2} (fn p => fn def => + BNF_FP_Util.mk_If (fst (#isVVr def) $ map_id_fst) + (p $ (fst (#asVVr def) $ map_id_fst)) + ) ps (map_filter I defs) (ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads + (map HOLogic.id_const plives @ map (fn T => HOLogic.mk_comp ( + Term.abs ("R", snd (HOLogic.dest_prodT T)) (Bound 0 $ HOLogic.mk_tuple ps), + snd_const T + )) rec_args') bound_ids free_ids mrbnf $ Bound (length P_Ts))) + ))) lthy; + + val card = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); + val some_defs = map_filter I defs; + val (Pmap, lthy) = mk_def_t "Pmap" nvars (fold_rev Term.absfree (map dest_Free fs) ( + mk_case_tuple (map dest_Free ps) (HOLogic.mk_tuple (map2 (fn p => fn def => + Term.list_comb (fst (#compSS def), fs @ [p])) ps some_defs + )) + )) lthy; + val (valid_P, lthy) = mk_def_t "valid_P" 1 (mk_case_tuple (map dest_Free ps) ( + foldr1 HOLogic.mk_conj (map2 (fn def => fn t => + mk_ordLess (mk_card_of (fst (#SSupp def) $ t)) card + ) some_defs ps) + )) lthy; + + in ({ + defs = defs, + Uctor = Uctor, + Pmap = Pmap, + valid_P = valid_P + }, lthy) end + ) (#pre_mrbnfs fp_res) (#quotient_fps fp_res) models suffixes lthy; val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; - fun morph (t, thm) phi = - let val t' = Morphism.term phi t - in ( - Term.subst_atomic_types (map TVar (Term.add_tvars t' []) ~~ map TFree (Term.add_tfrees t [])) t', + val morph = + let + val uctor = fst (#Uctor (hd consts)); + val uctor' = Morphism.term phi uctor; + val tyenv = Sign.typ_match (Proof_Context.theory_of lthy) (fastype_of uctor', fastype_of uctor) Vartab.empty; + val subst = Envir.subst_term (tyenv, Vartab.empty); + in fn (t, thm) => ( + Morphism.term (phi $> Morphism.term_morphism "fix_tyvars" subst) t, Morphism.thm phi thm ) end; - val defs = map (Option.map (fn def => { - aT = #aT def, - SSfun = #SSfun def, - VVr = morph (#VVr def) phi, - SSupp = morph (#SSupp def) phi, - IImsupps = map (fn t => morph t phi) (#IImsupps def), - isVVr = morph (#isVVr def) phi, - asVVr = morph (#asVVr def) phi, - compSS = morph (#compSS def) phi - })) defs; - - in (morph Uctor phi, morph Pmap phi, morph valid_P phi, defs, vars, lthy) end; - -fun create_tvsubst_of_mrbnf b qualify model lthy = + val consts = map (fn { defs, Uctor, Pmap, valid_P } => { + defs = map (Option.map (fn { aT, SSfun, VVr, SSupp, IImsupps, isVVr, asVVr, compSS } => { + aT = aT, + SSfun = SSfun, + VVr = morph VVr, + SSupp = morph SSupp, + IImsupps = map morph IImsupps, + isVVr = morph isVVr, + asVVr = morph asVVr, + compSS = morph compSS + })) defs, + Uctor = morph Uctor, + Pmap = morph Pmap, + valid_P = morph valid_P + }) consts; + + in (consts, lthy) end; + +fun create_tvsubst_of_mrbnf qualify fp_res models lthy = let - val (eta_defs, model, lthy) = prove_model_axioms b qualify model lthy; - val (Uctor, Pmap, valid_P, defs, vars, lthy) = define_tvsubst_consts b qualify model lthy; + val (fp_res, eta_defs, vars, models, lthy) = prove_model_axioms qualify fp_res models lthy; + val (((vars, pfrees), plives), pbounds) = vars; + + val (tvsubst_consts, lthy) = define_tvsubst_consts qualify fp_res + (vars, pfrees, plives, pbounds) models lthy; - val nvars = length vars; + val _ = @{print} tvsubst_consts + + (*val nvars = length vars; val mrbnf = hd (#pre_mrbnfs (#fp_result model)); val quotient = hd (#quotient_fps (#fp_result model)); val live = MRBNF_Def.live_of_mrbnf mrbnf; @@ -1547,6 +1596,7 @@ fun create_tvsubst_of_mrbnf b qualify model lthy = )); val (_, lthy) = Local_Theory.notes notes lthy - in (result, lthy) end; + in (result, lthy) end;*) + in error "end" end end \ No newline at end of file diff --git a/operations/Sugar.thy b/operations/Sugar.thy index d2f7b687..fb9068eb 100644 --- a/operations/Sugar.thy +++ b/operations/Sugar.thy @@ -517,9 +517,12 @@ lemma T2_distinct[simp]: apply (rule notI, (erule exE conjE sum.distinct[THEN notE])+)+ done -abbreviation "eta11 (x::_::var) \ Abs_T1_pre (Inl (Inl x))" -abbreviation "eta12 (x::_::var) \ Abs_T1_pre (Inl (Inr (Inr x)))" -abbreviation "eta21 (x::_::var) \ Abs_T2_pre (Inl (Inl x))" +abbreviation eta11 :: "'a \ ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g, 'h, 'i, 'j) T1_pre" where + "eta11 x \ Abs_T1_pre (Inl (Inl x))" +abbreviation eta12 :: "'b \ ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g, 'h, 'i, 'j) T1_pre" where + "eta12 x \ Abs_T1_pre (Inl (Inr (Inr x)))" +abbreviation eta21 :: "'a \ ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g, 'h, 'i, 'j) T2_pre" where + "eta21 x \ Abs_T2_pre (Inl (Inl x))" lemma eta_frees: "set1_T1_pre (eta11 x) = {x}" @@ -601,4 +604,47 @@ lemma eta_naturals: apply (rule refl)+ done +ML \ +val T1_model = { + binding = @{binding tvsubst_T1}, + etas = [ + SOME (@{term "eta11"}, { + eta_free = fn ctxt => resolve_tac ctxt @{thms eta_frees} 1, + eta_inj = fn ctxt => eresolve_tac ctxt @{thms eta_injs} 1, + eta_compl_free = fn ctxt => eresolve_tac ctxt @{thms eta_compl_frees} 1, + eta_natural = fn ctxt => HEADGOAL (resolve_tac ctxt @{thms eta_naturals} THEN_ALL_NEW assume_tac ctxt) + }), + SOME (@{term "eta12"}, { + eta_free = fn ctxt => resolve_tac ctxt @{thms eta_frees} 1, + eta_inj = fn ctxt => eresolve_tac ctxt @{thms eta_injs} 1, + eta_compl_free = fn ctxt => eresolve_tac ctxt @{thms eta_compl_frees} 1, + eta_natural = fn ctxt => HEADGOAL (resolve_tac ctxt @{thms eta_naturals} THEN_ALL_NEW assume_tac ctxt) + }) + ] +}; +val T2_model = { + binding = @{binding tvsubst_T2}, + etas = [ + SOME (@{term "eta21"}, { + eta_free = fn ctxt => resolve_tac ctxt @{thms eta_frees} 1, + eta_inj = fn ctxt => eresolve_tac ctxt @{thms eta_injs} 1, + eta_compl_free = fn ctxt => eresolve_tac ctxt @{thms eta_compl_frees} 1, + eta_natural = fn ctxt => HEADGOAL (resolve_tac ctxt @{thms eta_naturals} THEN_ALL_NEW assume_tac ctxt) + }), + NONE + ] +}; +\ + +ML_file \../Tools/mrbnf_tvsubst.ML\ + +ML \ +Multithreading.parallel_proofs := 0 +\ +declare [[ML_print_depth=100000]] +local_setup \fn lthy => +let + val (res', lthy) = MRBNF_TVSubst.create_tvsubst_of_mrbnf I res [T1_model, T2_model] lthy +in lthy end\ + end \ No newline at end of file diff --git a/operations/TVSubst.thy b/operations/TVSubst.thy index 10bef483..83d099a3 100644 --- a/operations/TVSubst.thy +++ b/operations/TVSubst.thy @@ -2859,7 +2859,6 @@ lemma IImsupp_Diffs: (* apply (rule sym) *) apply assumption apply assumption - thm in_IImsupps apply (frule in_IImsupps(3)) apply assumption apply (drule trans[OF Int_commute]) diff --git a/thys/System_Fc/SystemF.thy b/thys/System_Fc/SystemF.thy index 23e42e5a..7946c229 100644 --- a/thys/System_Fc/SystemF.thy +++ b/thys/System_Fc/SystemF.thy @@ -54,9 +54,56 @@ thm \.subst (* binder_datatype ('a,'b) term = Var 'b | App "('a,'b) term" "('a,'b) term" -| Lam x::'b ty::"'a \" t::"('a,'b) term" binds x in t -| TyApp "('a,'b) term" "'a \" +| Lam x::'b ty::"('a, 'b) \" t::"('a,'b) term" binds x in t +| TyApp "('a,'b) term" "'a \ list" | TyLam \::'a body::"('a,'b) term" binds \ in body +*) +(* + +definition U1ctor :: "('var::{var_T1_pre, var_T2_pre}, 'tyvar::{var_T1_pre, var_T2_pre}, 'var, 'tyvar, ('var, 'tyvar) T1 \ (('var, 'tyvar) P \ ('var, 'tyvar) U1), ('var, 'tyvar, 'a, 'b) T1 \ (('var, 'tyvar, 'a, 'b) P \ ('var, 'tyvar, 'a, 'b) U1), + ('var, 'tyvar, 'a, 'b) T2 \ (('var, 'tyvar, 'a, 'b) P \ ('var, 'tyvar, 'a, 'b) U2), ('var, 'tyvar, 'a, 'b) T2 \ (('var, 'tyvar, 'a, 'b) P \ ('var, 'tyvar, 'a, 'b) U2)) T1_pre \ ('var, 'tyvar, 'a, 'b) P \ ('var, 'tyvar, 'a, 'b) U1" where + "U1ctor y p \ case p of (f1, f2, f3) \ if isVVr11 (T1_ctor (map_T1_pre id id id id id id fst fst fst fst y)) then + f1 (asVVr11 (T1_ctor (map_T1_pre id id id id id id fst fst fst fst y))) else ( + if isVVr12 (T1_ctor (map_T1_pre id id id id id id fst fst fst fst y)) then + f2 (asVVr12 (T1_ctor (map_T1_pre id id id id id id fst fst fst fst y))) else ( + T1_ctor (map_T1_pre id id id id id id ((\R. R (f1, f2, f3)) \ snd) ((\R. R (f1, f2, f3)) \ snd) ((\R. R (f1, f2, f3)) \ snd) ((\R. R (f1, f2, f3)) \ snd) (case y of + Lam x t1 t2 \ Lam x (tvsubst_\ f1 t1) t2 + | TyApp t1 ts \ TyApp t1 (map (tvsubst_\ f1) ts) + | x \ x + )) +))" +*) +(* + +'a \ 'a 'm +ctor \ eta + +type ('a, 'b, 'c) term_internal = + Var 'b +| App "('a,'b, 'c) term" "('a,'b, 'c) term" +| Lam x::'b ty::'c t::"('a,'b, 'c) term" binds x in t +| TyApp "('a,'b,'c) term" 'c +| TyLam \::'a body::"('a,'b,'c) term" binds \ in body + +map_term_internal : ('a \ 'a) \ ('b \ 'b) \ ('c \ 'c') \ ('a, 'b, 'c) term_internal \ ('a, 'b, 'c') term_internal +eta : 'b \ ('a, 'b, 'c) term_internal_pre +\ tvsubst_term_internal ('b \ ('a, 'b, 'c) term_internal) \ ('a, 'b, 'c) term_internal \ ('a, 'b, 'c') term_internal + +typedef ('a, 'b) term = "UNIV::('a, 'b, 'a \) term_internal set" + +tvsubst_nested_term f1 t = case t of + Lam x t t1 \ Lam x (tvsubst_\ f1 t1) + | + +tvsubst_\ : ('a \ 'a \) \ 'a \ \ 'a \ + +tvsubst_term : ('b \ ('a, 'b) term) \ ('a, 'b) term \ ('a, 'b) term +tvsubst_\_term : ('a \ 'a \) \ ('a, 'b) term \ ('a, 'b) term + + +tvsubst_term : ('a \ 'a \) \ ('b \ ('a, 'b) term) \ ('a, 'b) term \ ('a, 'b) term +tvsubst_term f1 f2 t \ tvsubst_term_internal f2 (map_term_internal id id (tvsubst_\ f1) t) + *) ML \ From 92c7cd06a012720ecb7ed8c33bb12fb7ae74578d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Mon, 25 Mar 2024 17:49:02 +0000 Subject: [PATCH 3/7] Adjust first half of tvsubst theorems to mutual types --- Tools/mrbnf_tvsubst.ML | 434 +++++++++++++++++------------------ thys/POPLmark/SystemFSub.thy | 175 ++++++-------- 2 files changed, 277 insertions(+), 332 deletions(-) diff --git a/Tools/mrbnf_tvsubst.ML b/Tools/mrbnf_tvsubst.ML index a01a1f69..895bdbc4 100644 --- a/Tools/mrbnf_tvsubst.ML +++ b/Tools/mrbnf_tvsubst.ML @@ -89,47 +89,47 @@ fun prove_model_axioms qualify res (models : (Proof.context -> tactic) tvsubst_m val old_vars = rev (map TVar (Term.add_tvars set []) @ map TFree (Term.add_tfrees set [])); val set' = Term.subst_atomic_types (old_vars ~~ args) set; val vars = rev (fold (Term.add_tfreesT) args []); - + val (((((frees, pfrees), plives), pbounds), bounds), rec_vars) = args |> chop nvars ||>> chop pfree ||>> chop plive ||>> chop pbound ||>> chop nvars; - + val names_lthy = fold (Variable.declare_constraints o Logic.mk_type o TFree) vars lthy; val ((((a, b), x), Bs), names_lthy) = names_lthy |> apfst hd o mk_Frees "a" [aT] ||>> apfst hd o mk_Frees "b" [aT] ||>> apfst hd o mk_Frees "x" [preT] ||>> mk_TFrees (length rec_vars); - + val fTs = map (fn a => a --> a) (frees @ bounds) @ map2 (curry op-->) rec_vars Bs; - + val ((free_fs, bound_fs), live_fs) = names_lthy |> mk_Frees "f" fTs |> fst |> chop nvars ||>> chop nvars; val fs = free_fs @ bound_fs @ live_fs; - + val lthy = snd (Local_Theory.begin_nested lthy); val (raw_eta, lthy) = mk_def_t false (#binding model) qualify (the eta_name) 0 eta lthy val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; - + val eta' = Morphism.term phi (fst raw_eta); val vars = snd (dest_Type (range_type (fastype_of eta'))); val eta = (Term.subst_atomic_types (vars ~~ args) eta', Morphism.thm phi (snd raw_eta)); - + val eta_free = Goal.prove_sorry lthy (names [a]) [] (mk_Trueprop_eq (set' $ (fst eta $ a), mk_singleton a)) (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_free tacs context); - + val eta_inj = Goal.prove_sorry lthy (names [a, b]) [] (Logic.mk_implies (mk_Trueprop_eq (fst eta $ a, fst eta $ b), mk_Trueprop_eq (a, b))) (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_inj tacs context); - + val eta_compl_free = Goal.prove_sorry lthy [] [] (Logic.all x (Logic.mk_implies ( HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_mem ( @@ -138,9 +138,9 @@ fun prove_model_axioms qualify res (models : (Proof.context -> tactic) tvsubst_m mk_Trueprop_eq (set' $ x, mk_bot aT) ))) (fn {context, ...} => unfold_thms_tac context [snd eta] THEN #eta_compl_free tacs context); - + val f_prems = map mk_supp_bound free_fs @ maps (fn f => [mk_bij f, mk_supp_bound f]) bound_fs; - + val eta' = let val (n, T) = dest_Const (fst eta); @@ -172,9 +172,7 @@ fun prove_model_axioms qualify res (models : (Proof.context -> tactic) tvsubst_m ) end ) models mrbnfs eta_names_opts lthy; - val sort = foldl1 (Sign.inter_sort (Proof_Context.theory_of lthy)) ( - map MRBNF_Def.class_of_mrbnf mrbnfs - ); + val sort = snd (dest_TFree (domain_type (fastype_of (fst (fst (hd (map_filter I (flat etass)))))))); val (Ts, _) = mk_TFrees' ( replicate (nvars + pfree) sort @ replicate plive @{sort type} @ replicate pbound sort ) lthy; @@ -221,132 +219,127 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models val (fs, _) = lthy |> mk_Frees "f" (map (fn a => a --> a) vars); - + val (_, lthy) = Local_Theory.begin_nested lthy; - val (consts, lthy) = @{fold_map 4} (fn mrbnf => fn quot => fn model => fn suffix => fn lthy => + val (defss, lthy) = @{fold_map 4} (fn mrbnf => fn quot => fn model => fn suffix => + @{fold_map 3} (fn eta_opt => fn suffix => fn i => fn lthy => let val opt = Option.map (fn (eta, _) => + let + val qT = #T quot; + val aT = domain_type (fastype_of eta); + val (VVr, lthy) = mk_def_t ("VVr" ^ the suffix) 0 (HOLogic.mk_comp (#ctor quot, eta)) lthy; + + val ((h, t), _) = lthy + |> apfst hd o mk_Frees "f" [aT --> qT] + ||>> apfst hd o mk_Frees "t" [qT]; + + val (SSupp, lthy) = mk_def_public ("SSupp" ^ the suffix ^ "_" ^ Binding.name_of (#binding model)) + 1 (Term.absfree (dest_Free h) (HOLogic.mk_Collect ("a", aT, HOLogic.mk_not (HOLogic.mk_eq ( + h $ Bound 0, fst VVr $ Bound 0 + ))) + )) lthy; + + val (IImsupps, lthy) = @{fold_map 2} (fn FVars => fn s => mk_def_public ("IImsupp" ^ the suffix ^ "_" ^ s) 1 ( + Term.absfree (dest_Free h) ( + let val UN = mk_UNION (fst SSupp $ h) (HOLogic.mk_comp (FVars, h)); + in if fastype_of (fst SSupp $ h) = range_type (fastype_of FVars) then + mk_Un (fst SSupp $ h, UN) + else UN end + ))) (#FVars quot) (if nvars = 1 then [""] else map string_of_int (1 upto nvars)) lthy; + + val (isVVr, lthy) = mk_def_t ("isVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( + HOLogic.mk_exists ("a", aT, HOLogic.mk_eq (t, fst VVr $ Bound 0)) + )) lthy; + + val (asVVr, lthy) = mk_def_t ("asVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( + BNF_FP_Util.mk_If (fst isVVr $ t) + (HOLogic.choice_const aT $ Term.abs ("a", aT) (HOLogic.mk_eq (fst VVr $ Bound 0, t))) + (BNF_GFP_Util.mk_undefined aT) + )) lthy; + + val (fs, _) = lthy + |> mk_Frees "f" (map (fn v => v --> v) vars); + + val (compSS, lthy) = mk_def_t ("compSS" ^ the suffix) nvars ( + fold_rev Term.absfree (map dest_Free fs) ( + Term.absfree (dest_Free h) (HOLogic.mk_comp ( + HOLogic.mk_comp ( + Term.list_comb (#rename quot, fs), + h + ), + mk_inv (nth fs i) + )) + ) + ) lthy; + in ({ + aT = aT, + SSfun = fastype_of h, + VVr = VVr, + SSupp = SSupp, + IImsupps = IImsupps, + isVVr = isVVr, + asVVr = asVVr, + compSS = compSS + }, lthy) end + ) eta_opt in ( + Option.map fst opt, the_default lthy (Option.map snd opt)) + end) (#etas model) suffix (0 upto nvars - 1) + ) (#pre_mrbnfs fp_res) (#quotient_fps fp_res) models suffixes lthy; + + val P_Tss = map (map_filter (Option.map #SSfun)) defss; + val P_T = HOLogic.mk_tupleT (flat P_Tss); + val (pss, _) = lthy + |> mk_Freess "p" P_Tss; + + val (Uctors, lthy) = @{fold_map 5} (fn ps => fn defs => fn mrbnf => fn quot => fn model => fn lthy => let val ctor = #ctor quot; - - val (defs, lthy) = @{fold_map 3} (fn eta_opt => fn suffix => fn i => fn lthy => let val opt = Option.map (fn (eta, _) => - let - val qT = #T quot; - val aT = domain_type (fastype_of eta); - val (VVr, lthy) = mk_def_t ("VVr" ^ the suffix) 0 (HOLogic.mk_comp (ctor, eta)) lthy; - - val ((h, t), _) = lthy - |> apfst hd o mk_Frees "f" [aT --> qT] - ||>> apfst hd o mk_Frees "t" [qT]; - - val (SSupp, lthy) = mk_def_public ("SSupp" ^ the suffix ^ "_" ^ Binding.name_of (#binding model)) - 1 (Term.absfree (dest_Free h) (HOLogic.mk_Collect ("a", aT, HOLogic.mk_not (HOLogic.mk_eq ( - h $ Bound 0, fst VVr $ Bound 0 - ))) - )) lthy; - - val (IImsupps, lthy) = @{fold_map 2} (fn FVars => fn s => mk_def_public ("IImsupp" ^ the suffix ^ "_" ^ s) 1 ( - Term.absfree (dest_Free h) ( - let val UN = mk_UNION (fst SSupp $ h) (HOLogic.mk_comp (FVars, h)); - in if fastype_of (fst SSupp $ h) = range_type (fastype_of FVars) then - mk_Un (fst SSupp $ h, UN) - else UN end - ))) (#FVars quot) (if nvars = 1 then [""] else map string_of_int (1 upto nvars)) lthy; - - val (isVVr, lthy) = mk_def_t ("isVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( - HOLogic.mk_exists ("a", aT, HOLogic.mk_eq (t, fst VVr $ Bound 0)) - )) lthy; - - val (asVVr, lthy) = mk_def_t ("asVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( - BNF_FP_Util.mk_If (fst isVVr $ t) - (HOLogic.choice_const aT $ Term.abs ("a", aT) (HOLogic.mk_eq (fst VVr $ Bound 0, t))) - (BNF_GFP_Util.mk_undefined aT) - )) lthy; - - val (fs, _) = lthy - |> mk_Frees "f" (map (fn v => v --> v) vars); - - val (compSS, lthy) = mk_def_t ("compSS" ^ the suffix) nvars ( - fold_rev Term.absfree (map dest_Free fs) ( - Term.absfree (dest_Free h) (HOLogic.mk_comp ( - HOLogic.mk_comp ( - Term.list_comb (#rename quot, fs), - h - ), - mk_inv (nth fs i) - )) - ) - ) lthy; - in ({ - aT = aT, - SSfun = fastype_of h, - VVr = VVr, - SSupp = SSupp, - IImsupps = IImsupps, - isVVr = isVVr, - asVVr = asVVr, - compSS = compSS - }, lthy) end - ) eta_opt in ( - Option.map fst opt, the_default lthy (Option.map snd opt)) - end) (#etas model) suffix (0 upto nvars - 1) lthy; - - val P_Ts = map_filter (Option.map #SSfun) defs; - val P_T = HOLogic.mk_tupleT P_Ts; - val (ps, _) = lthy - |> mk_Frees "p" P_Ts; - - val (name, (args, rec_args)) = dest_Type (fst (dest_funT (fastype_of ctor))) - |> apsnd (chop (nvars * 2 + length pfrees + length plives + length pbounds)); - val rec_args' = map (fn T => HOLogic.mk_prodT (T, P_T --> T)) rec_args; - val args = args @ rec_args'; - - val free_ids = map HOLogic.id_const (vars @ pfrees); - val bound_ids = map HOLogic.id_const (pbounds @ vars); - - val deads = MRBNF_Def.deads_of_mrbnf mrbnf; - val map_id_fst = ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads - (map HOLogic.id_const plives @ map fst_const rec_args') - bound_ids free_ids mrbnf $ Bound (length P_Ts)); - val mk_def_t = MRBNF_Util.mk_def_t false (#binding model) qualify - - val (Uctor, lthy) = mk_def_t "Uctor" 0 (Term.abs ("F", Type (name, args)) ( - mk_case_tuple (map dest_Free ps) (@{fold 2} (fn p => fn def => + val (name, (args, rec_args)) = dest_Type (fst (dest_funT (fastype_of ctor))) + |> apsnd (chop (nvars * 2 + length pfrees + length plives + length pbounds)); + val rec_args' = map (fn T => HOLogic.mk_prodT (T, P_T --> T)) rec_args; + val args = args @ rec_args'; + + val free_ids = map HOLogic.id_const (vars @ pfrees); + val bound_ids = map HOLogic.id_const (pbounds @ vars); + + val deads = MRBNF_Def.deads_of_mrbnf mrbnf; + val map_id_fst = ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads + (map HOLogic.id_const plives @ map fst_const rec_args') + bound_ids free_ids mrbnf $ Bound (length (flat P_Tss))); + val mk_def_t = MRBNF_Util.mk_def_t false (#binding model) qualify; + + in mk_def_t "Uctor" 0 (Term.abs ("F", Type (name, args)) ( + mk_case_tuple (map dest_Free (flat pss)) (@{fold 2} (fn p => fn def => BNF_FP_Util.mk_If (fst (#isVVr def) $ map_id_fst) (p $ (fst (#asVVr def) $ map_id_fst)) ) ps (map_filter I defs) (ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads (map HOLogic.id_const plives @ map (fn T => HOLogic.mk_comp ( - Term.abs ("R", snd (HOLogic.dest_prodT T)) (Bound 0 $ HOLogic.mk_tuple ps), + Term.abs ("R", snd (HOLogic.dest_prodT T)) (Bound 0 $ HOLogic.mk_tuple (flat pss)), snd_const T - )) rec_args') bound_ids free_ids mrbnf $ Bound (length P_Ts))) - ))) lthy; - - val card = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); - val some_defs = map_filter I defs; - val (Pmap, lthy) = mk_def_t "Pmap" nvars (fold_rev Term.absfree (map dest_Free fs) ( - mk_case_tuple (map dest_Free ps) (HOLogic.mk_tuple (map2 (fn p => fn def => - Term.list_comb (fst (#compSS def), fs @ [p])) ps some_defs - )) - )) lthy; - val (valid_P, lthy) = mk_def_t "valid_P" 1 (mk_case_tuple (map dest_Free ps) ( - foldr1 HOLogic.mk_conj (map2 (fn def => fn t => - mk_ordLess (mk_card_of (fst (#SSupp def) $ t)) card - ) some_defs ps) - )) lthy; + )) rec_args') bound_ids free_ids mrbnf $ Bound (length (flat P_Tss)))) + ))) lthy end + ) pss defss (#pre_mrbnfs fp_res) (#quotient_fps fp_res) models lthy; - in ({ - defs = defs, - Uctor = Uctor, - Pmap = Pmap, - valid_P = valid_P - }, lthy) end - ) (#pre_mrbnfs fp_res) (#quotient_fps fp_res) models suffixes lthy; + val ps = flat pss; + val card = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); + val some_defs = maps (map_filter I) defss; + val (Pmap, lthy) = mk_def_t "Pmap" (nvars + 1) (fold_rev Term.absfree (map dest_Free fs) ( + mk_case_tuple (map dest_Free ps) (HOLogic.mk_tuple (map2 (fn p => fn def => + Term.list_comb (fst (#compSS def), fs @ [p])) ps some_defs + )) + )) lthy; + val (valid_P, lthy) = mk_def_t "valid_P" 1 (mk_case_tuple (map dest_Free ps) ( + foldr1 HOLogic.mk_conj (map2 (fn def => fn t => + mk_ordLess (mk_card_of (fst (#SSupp def) $ t)) card + ) some_defs ps) + )) lthy; val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; val morph = let - val uctor = fst (#Uctor (hd consts)); + val uctor = fst (hd Uctors); val uctor' = Morphism.term phi uctor; val tyenv = Sign.typ_match (Proof_Context.theory_of lthy) (fastype_of uctor', fastype_of uctor) Vartab.empty; val subst = Envir.subst_term (tyenv, Vartab.empty); @@ -355,44 +348,38 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models Morphism.thm phi thm ) end; - val consts = map (fn { defs, Uctor, Pmap, valid_P } => { - defs = map (Option.map (fn { aT, SSfun, VVr, SSupp, IImsupps, isVVr, asVVr, compSS } => { - aT = aT, - SSfun = SSfun, - VVr = morph VVr, - SSupp = morph SSupp, - IImsupps = map morph IImsupps, - isVVr = morph isVVr, - asVVr = morph asVVr, - compSS = morph compSS - })) defs, - Uctor = morph Uctor, - Pmap = morph Pmap, - valid_P = morph valid_P - }) consts; - - in (consts, lthy) end; + val defss = map (map (Option.map (fn { aT, SSfun, VVr, SSupp, IImsupps, isVVr, asVVr, compSS } => { + aT = aT, + SSfun = SSfun, + VVr = morph VVr, + SSupp = morph SSupp, + IImsupps = map morph IImsupps, + isVVr = morph isVVr, + asVVr = morph asVVr, + compSS = morph compSS + }))) defss; + + in (defss, map morph Uctors, morph Pmap, morph valid_P, lthy) end; + +fun option_map2 f (SOME x) (SOME y) = SOME (f x y) + | option_map2 _ _ _ = NONE +fun traverse_pair (SOME (x, y)) = (SOME x, SOME y) + | traverse_pair NONE = (NONE, NONE) fun create_tvsubst_of_mrbnf qualify fp_res models lthy = let val (fp_res, eta_defs, vars, models, lthy) = prove_model_axioms qualify fp_res models lthy; val (((vars, pfrees), plives), pbounds) = vars; - - val (tvsubst_consts, lthy) = define_tvsubst_consts qualify fp_res - (vars, pfrees, plives, pbounds) models lthy; - - val _ = @{print} tvsubst_consts - (*val nvars = length vars; - val mrbnf = hd (#pre_mrbnfs (#fp_result model)); - val quotient = hd (#quotient_fps (#fp_result model)); - val live = MRBNF_Def.live_of_mrbnf mrbnf; + val (defss, Uctors, Pmap, valid_P, lthy) = define_tvsubst_consts qualify fp_res + (vars, pfrees, plives, pbounds) models lthy; + val nvars = length vars; val card = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); - val defs = map2 (fn (SOME axiom) => (fn SOME def => SOME { - eta = fst axiom, - axioms = snd axiom, + val defss = map2 (fn model => map2 (option_map2 (fn eta => fn def => { + eta = fst eta, + axioms = snd eta, aT = #aT def, VVr = #VVr def, SSupp = #SSupp def, @@ -402,22 +389,22 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = SSfun = #SSfun def, compSS = #compSS def, mk_SSupp_bound = fn t => mk_ordLess (mk_card_of (fst (#SSupp def) $ t)) card - } | NONE => NONE) | NONE => fn _ => NONE) (#etas model) defs; + })) (#etas model)) models defss; - val SSupp_VVr_empties = map (Option.map (fn def => - Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (fst (#SSupp def) $ fst (#VVr def), mk_bot (#aT def))) (fn {context=ctxt, ...} => EVERY1 [ - K (unfold_thms_tac ctxt (@{thms HOL.simp_thms(6) not_True_eq_False empty_def[symmetric]} @ [snd (#SSupp def)])), - rtac ctxt TrueI - ]) - )) defs; - val SSupp_VVr_bounds = map (Option.map (fn def => - Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (#mk_SSupp_bound def (fst (#VVr def)))) (fn {context=ctxt, ...} => EVERY1 [ - K (unfold_thms_tac ctxt (map_filter I SSupp_VVr_empties)), - REPEAT_DETERM o resolve_tac ctxt @{thms emp_bound cmin_greater card_of_Card_order} - ]) - )) defs; + val (SSupp_VVr_emptiess, SSupp_VVr_boundss) = split_list (map (split_list o map (traverse_pair o Option.map (fn def => + let + val empty = Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (fst (#SSupp def) $ fst (#VVr def), mk_bot (#aT def))) (fn {context=ctxt, ...} => EVERY1 [ + K (unfold_thms_tac ctxt (@{thms HOL.simp_thms(6) not_True_eq_False empty_def[symmetric]} @ [snd (#SSupp def)])), + rtac ctxt TrueI + ]); + val bound = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (#mk_SSupp_bound def (fst (#VVr def)))) (fn {context=ctxt, ...} => EVERY1 [ + K (unfold_thms_tac ctxt [empty]), + REPEAT_DETERM o resolve_tac ctxt @{thms emp_bound cmin_greater card_of_Card_order} + ]); + in (empty, bound) end + ))) defss); - val VVr_injs = map (Option.map (fn def => + val VVr_injss = map2 (fn quot => map (Option.map (fn def => let val (a, b) = (Free ("a", #aT def), Free ("b", #aT def)); val ax = #axioms def; @@ -427,7 +414,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = )) (fn {context=ctxt, ...} => EVERY1 [ K (unfold_thms_tac ctxt (@{thms comp_def} @ [snd (#VVr def)])), rtac ctxt (#eta_inj ax), - dtac ctxt (iffD1 OF [#inject quotient]), + dtac ctxt (iffD1 OF [#inject quot]), REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], dtac ctxt @{thm trans[rotated]}, rtac ctxt sym, @@ -437,51 +424,52 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = rtac ctxt @{thm arg_cong[OF id_apply]}, assume_tac ctxt ]) end - )) defs; + ))) (#quotient_fps fp_res) defss; - val (((fs, gs), some_hs), _) = lthy + val (((fs, gs), some_hss), _) = lthy |> mk_Frees "f" (map (fn a => a --> a) vars) ||>> mk_Frees "g" (map (fn a => a --> a) vars) - ||>> mk_Frees "h" (map_filter (Option.map #SSfun) defs); - val hs = fst (fold_map (fn def => fn hs => case def of + ||>> mk_Freess "h" (map (map_filter (Option.map #SSfun)) defss); + val hss = map2 (fn defs => fn some_hs => fst (fold_map (fn def => fn hs => case def of SOME _ => (SOME (hd hs), tl hs) | _ => (NONE, hs) - ) defs some_hs); + ) defs some_hs)) defss some_hss; fun mk_supp_bound' f = mk_ordLess (mk_card_of (mk_supp f)) card; - val f_premss = map (fn f => map HOLogic.mk_Trueprop [mk_bij f, mk_supp_bound f]) fs; - val f_premss' = map (fn f => map HOLogic.mk_Trueprop [mk_bij f, mk_supp_bound' f]) fs; + val f_prems = maps (fn f => map HOLogic.mk_Trueprop [mk_bij f, mk_supp_bound f]) fs; + val f_prems' = maps (fn f => map HOLogic.mk_Trueprop [mk_bij f, mk_supp_bound' f]) fs; - val rrename_VVrs = map_index (fn (i, opt) => Option.map (fn def => + val rrename_VVrss = map2 (fn quot => map_index (fn (i, opt) => Option.map (fn def => let val a = Free ("a", #aT def); val VVr = fst (#VVr def) val goal = mk_Trueprop_eq ( - Term.list_comb (#rename quotient, fs) $ (VVr $ a), + Term.list_comb (#rename quot, fs) $ (VVr $ a), VVr $ (nth fs i $ a) ); - in Goal.prove_sorry lthy (names (fs @ [a])) (flat f_premss) goal (fn {context=ctxt, prems} => EVERY1 [ + in Goal.prove_sorry lthy (names (fs @ [a])) f_prems goal (fn {context=ctxt, prems} => EVERY1 [ K (unfold_thms_tac ctxt [snd (#VVr def), @{thm comp_def}]), rtac ctxt trans, - rtac ctxt (#rename_ctor (#inner quotient)), + rtac ctxt (#rename_ctor (#inner quot)), REPEAT_DETERM o resolve_tac ctxt (prems @ @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order}), - rtac ctxt (infer_instantiate' ctxt [NONE, NONE, SOME (Thm.cterm_of ctxt (#ctor quotient))] arg_cong), + rtac ctxt (infer_instantiate' ctxt [NONE, NONE, SOME (Thm.cterm_of ctxt (#ctor quot))] arg_cong), rtac ctxt (Local_Defs.unfold0 ctxt @{thms comp_def} (fun_cong OF [#eta_natural (#axioms def)])), REPEAT_DETERM o resolve_tac ctxt (prems @ @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order}) ]) end - ) opt) defs; + ) opt)) (#quotient_fps fp_res) defss; + val mrbnfs = #pre_mrbnfs fp_res; val cmin_UNIV = foldl1 mk_cmin (map (mk_card_of o HOLogic.mk_UNIV) vars); val Cinfinite_card = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_conj ( mk_cinfinite cmin_UNIV, mk_Card_order cmin_UNIV ))) (fn {context=ctxt, ...} => EVERY1 [ - REPEAT_DETERM o resolve_tac ctxt (MRBNF_Def.UNIV_cinfinite_of_mrbnf mrbnf :: @{thms cmin_Cinfinite conjI card_of_Card_order}) + REPEAT_DETERM o resolve_tac ctxt (MRBNF_Def.UNIV_cinfinite_of_mrbnf (hd mrbnfs) :: @{thms cmin_Cinfinite conjI card_of_Card_order}) ]); val regularCard_card = Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_regularCard cmin_UNIV)) (fn {context=ctxt, ...} => EVERY1 [ - REPEAT_DETERM o resolve_tac ctxt (#var_regular (MRBNF_Def.class_thms_of_mrbnf mrbnf) :: MRBNF_Def.UNIV_cinfinite_of_mrbnf mrbnf :: @{thms cmin_regularCard cmin_Cinfinite conjI card_of_Card_order}) + REPEAT_DETERM o resolve_tac ctxt (#var_regular (MRBNF_Def.class_thms_of_mrbnf (hd mrbnfs)) :: MRBNF_Def.UNIV_cinfinite_of_mrbnf (hd mrbnfs) :: @{thms cmin_regularCard cmin_Cinfinite conjI card_of_Card_order}) ]); val Un_bound = @{thm Un_Cinfinite_ordLess} OF [@{thm _}, @{thm _}, Cinfinite_card]; val UNION_bound = @{thm regularCard_UNION_bound} OF [Cinfinite_card, regularCard_card]; - val SSupp_comps = @{map 3} (fn f => fn rrename_VVr => Option.map (fn def => + val SSupp_compss = @{map 3} (fn quotient => @{map 3} (fn f => fn rrename_VVr => Option.map (fn def => let val g = Free ("g", #aT def --> #T quotient); val goal = HOLogic.mk_Trueprop (mk_leq @@ -514,7 +502,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = REPEAT_DETERM o resolve_tac ctxt prems ]); - val SSupp_comp_rename_subset = Goal.prove_sorry lthy (names (fs @ [g])) (flat f_premss) + val SSupp_comp_rename_subset = Goal.prove_sorry lthy (names (fs @ [g])) f_prems (HOLogic.mk_Trueprop (mk_leq (fst (#SSupp def) $ HOLogic.mk_comp (Term.list_comb (#rename quotient, fs), g)) (mk_Un (fst (#SSupp def) $ g, mk_supp f)) @@ -538,7 +526,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ]); val SSupp_comp_rename_bound = Goal.prove_sorry lthy (names (fs @ [g])) ( - [HOLogic.mk_Trueprop (#mk_SSupp_bound def g)] @ flat f_premss' + [HOLogic.mk_Trueprop (#mk_SSupp_bound def g)] @ f_prems' ) (HOLogic.mk_Trueprop (#mk_SSupp_bound def (HOLogic.mk_comp ( Term.list_comb (#rename quotient, fs), g )))) (fn {context=ctxt, prems} => EVERY1 [ @@ -552,13 +540,11 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = SSupp_comp_rename_subset = SSupp_comp_rename_subset, SSupp_comp_rename_bound = SSupp_comp_rename_bound } end - )) fs rrename_VVrs defs; + )) fs) (#quotient_fps fp_res) rrename_VVrss defss; val g_prems' = maps (fn g => map HOLogic.mk_Trueprop [mk_bij g, mk_supp_bound' g]) gs; - val f_prems = flat f_premss; - val f_prems' = flat f_premss'; - val compSS_comp0s = map (Option.map (fn def => + val compSS_comp0ss = map2 (fn quotient => map (Option.map (fn def => let val goal = mk_Trueprop_eq ( HOLogic.mk_comp (Term.list_comb (fst (#compSS def), fs), Term.list_comb (fst (#compSS def), gs)), @@ -576,9 +562,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = K (unfold_thms_tac ctxt @{thms comp_assoc}), rtac ctxt refl ]) end - )) defs; + ))) (#quotient_fps fp_res) defss; - val compSS_id0s = map (Option.map (fn def => + val compSS_id0ss = map2 (fn quotient => map (Option.map (fn def => let val goal = mk_Trueprop_eq ( Term.list_comb (fst (#compSS def), map HOLogic.id_const vars), @@ -589,9 +575,42 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = @ [snd (#compSS def), #rename_id0 quotient] ) THEN rtac ctxt refl 1 ) end - )) defs; + ))) (#quotient_fps fp_res) defss; + val some_defss = map (map_filter I) defss; + val P_Ts = map #SSfun (flat some_defss); + val ((ps, p), _) = lthy + |> mk_Frees "p" P_Ts + ||>> apfst hd o mk_Frees "p" [HOLogic.mk_tupleT P_Ts]; + val Pmap_id0 = + let val goal = mk_Trueprop_eq ( + Term.list_comb (fst Pmap, map HOLogic.id_const vars), + HOLogic.id_const (fastype_of p) + ) in Goal.prove_sorry lthy [] [] goal (fn {context=ctxt, ...} => EVERY1 [ + rtac ctxt ext, + K (unfold_thms_tac ctxt (@{thm case_prod_beta} :: snd Pmap :: maps (map_filter I) compSS_id0ss)), + K (unfold_thms_tac ctxt @{thms id_def prod.collapse}), + rtac ctxt refl + ]) end + + val Pmap_comp0 = + let val goal = mk_Trueprop_eq ( + HOLogic.mk_comp (Term.list_comb (fst Pmap, fs), Term.list_comb (fst Pmap, gs)), + Term.list_comb (fst Pmap, map2 (curry HOLogic.mk_comp) fs gs) + ) in Goal.prove_sorry lthy (names (fs @ gs)) (g_prems' @ f_prems') goal (fn {context=ctxt, prems} => EVERY1 [ + rtac ctxt ext, + rtac ctxt @{thm trans[OF comp_apply]}, + K (unfold_thms_tac ctxt (snd Pmap :: @{thms case_prod_beta})), + K (unfold_thms_tac ctxt @{thms prod.inject fst_conv snd_conv}), + REPEAT_DETERM o resolve_tac ctxt (conjI :: prems @ map (fn thm => + @{thm trans[OF comp_apply[symmetric]]} OF [@{thm fun_cong} OF [thm]] + ) (maps (map_filter I) compSS_comp0ss)) + ]) end; + + val _ = @{print} Pmap_comp0 + + (* val IImsupp_VVrs = @{map 3} (fn f => fn i => Option.map (fn def => let val a = Free ("a", #aT def); @@ -874,35 +893,6 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ]) end )) fs defs; - val some_defs = map_filter I defs; - val P_Ts = map #SSfun some_defs; - val ((ps, p), _) = lthy - |> mk_Frees "p" P_Ts - ||>> apfst hd o mk_Frees "p" [HOLogic.mk_tupleT P_Ts]; - - val Pmap_comp0 = - let val goal = mk_Trueprop_eq ( - HOLogic.mk_comp (Term.list_comb (fst Pmap, fs), Term.list_comb (fst Pmap, gs)), - Term.list_comb (fst Pmap, map2 (curry HOLogic.mk_comp) fs gs) - ) in Goal.prove_sorry lthy (names (fs @ gs)) (g_prems' @ f_prems') goal (fn {context=ctxt, prems} => EVERY1 [ - rtac ctxt ext, - K (unfold_thms_tac ctxt (snd Pmap :: @{thms case_prod_beta})), - rtac ctxt @{thm trans[OF comp_apply]}, - K (unfold_thms_tac ctxt @{thms prod.inject fst_conv snd_conv}), - REPEAT_DETERM o resolve_tac ctxt (conjI :: prems @ map (fn thm => - @{thm trans[OF comp_apply[symmetric]]} OF [@{thm fun_cong} OF [thm]] - ) (map_filter I compSS_comp0s)) - ]) end; - val Pmap_id0 = - let val goal = mk_Trueprop_eq ( - Term.list_comb (fst Pmap, map HOLogic.id_const vars), - HOLogic.id_const (fastype_of p) - ) in Goal.prove_sorry lthy [] [] goal (fn {context=ctxt, ...} => EVERY1 [ - K (unfold_thms_tac ctxt (@{thm case_prod_beta} :: snd Pmap :: map_filter I compSS_id0s)), - K (unfold_thms_tac ctxt @{thms id_def prod.collapse}), - rtac ctxt refl - ]) end - val valid_Pmap = let val goal = Logic.mk_implies (apply2 HOLogic.mk_Trueprop ( diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy index dfada38e..b30cde69 100644 --- a/thys/POPLmark/SystemFSub.thy +++ b/thys/POPLmark/SystemFSub.thy @@ -250,7 +250,7 @@ fun Vfvars :: "V \ var set" where interpretation Components where dummy = "undefined :: var" and Tmap = Tmap and Tfvars = Tfvars -apply standard unfolding ssbij_def Tmap_def +apply standard unfolding ssbij_def Tmap_def using small_Un small_def typ.card_of_FFVars_bounds apply (auto simp: typ.FFVars_rrenames map_prod.comp typ.rrename_comp0s inf_A) apply (rule var_typ_pre_class.Un_bound var_typ_pre_class.UN_bound context_set_bd_UNIV set_bd_UNIV @@ -265,13 +265,13 @@ definition G :: "var set \ (T \ bool) \ T \< "G \ \B R t. (B = {} \ snd (snd t) = Top \ \ fst t ok \ fst (snd t) closed_in fst t) \ (\x. B = {} \ fst (snd t) = TyVar x \ fst (snd t) = snd (snd t) \ \ fst t ok \ fst (snd t) closed_in fst t) - \ (\x U \ T. B = {} \ fst t = \ \ fst (snd t) = TyVar x \ snd (snd t) = T \ x <: U \ \ \ R (\, U, T) + \ (\x U \ T. B = {} \ fst t = \ \ fst (snd t) = TyVar x \ snd (snd t) = T \ x <: U \ \ \ R (\, U, T) \ \\ \ \ U <: T\) - \ (\\ T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2. B = {} \ fst t = \ \ fst (snd t) = (S\<^sub>1 \ S\<^sub>2) \ snd (snd t) = (T\<^sub>1 \ T\<^sub>2) \ - R (\, T\<^sub>1, S\<^sub>1) \ \ \ \ \ T1 <: S1 \ \ + \ (\\ T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2. B = {} \ fst t = \ \ fst (snd t) = (S\<^sub>1 \ S\<^sub>2) \ snd (snd t) = (T\<^sub>1 \ T\<^sub>2) \ + R (\, T\<^sub>1, S\<^sub>1) \ \ \ \ \ T1 <: S1 \ \ R (\, S\<^sub>2, T\<^sub>2) \ \ \ \ \ S2 <: T2 \ ) - \ (\\ T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2. B = {x} \ fst t = \ \ fst (snd t) = (\x<:S\<^sub>1. S\<^sub>2) \ snd (snd t) = (\x<:T\<^sub>1. T\<^sub>2) \ - R (\, T\<^sub>1, S\<^sub>1) \ \\ \ \ T1 <: S1 \ \ + \ (\\ T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2. B = {x} \ fst t = \ \ fst (snd t) = (\x<:S\<^sub>1. S\<^sub>2) \ snd (snd t) = (\x<:T\<^sub>1. T\<^sub>2) \ + R (\, T\<^sub>1, S\<^sub>1) \ \\ \ \ T1 <: S1 \ \ R (\,x<:T\<^sub>1, S\<^sub>2, T\<^sub>2) \ \\ \,x<:T1 \ S2 <: T2 \) " @@ -298,7 +298,7 @@ lemma wf_eqvt: shows "\ \ ok \ \ map_context f \ ok" unfolding map_context_def proof (induction \) case (Cons a \) - then show ?case using assms apply auto + then show ?case using assms apply auto apply (metis fst_conv image_iff) using closed_in_eqvt map_context_def by fastforce qed simp @@ -329,63 +329,18 @@ lemma G_equiv: "ssbij \ \ small B \ G B R typ.rrename_comps typ.FFVars_rrenames wf_eqvt extend_eqvt | ((rule exI[of _ "\ _"] exI)+, (rule conjI)?, rule refl) | ((rule exI[of _ "rrename_typ \ _"])+, (rule conjI)?, rule in_context_eqvt))+ -(* - unfolding G_def - apply (elim disjE) - subgoal - apply (rule disjI1) - apply (cases t) - unfolding ssbij_def Tmap_def using closed_in_eqvt wf_eqvt by simp - subgoal - apply (rule disjI2, rule disjI1) - apply (erule exE) - apply (elim conjE) - subgoal for x - apply (cases t) - unfolding ssbij_def Tmap_def using wf_eqvt by auto - done - subgoal - apply (rule disjI2, rule disjI2, rule disjI1) - apply (elim exE conjE) - subgoal for x U \ T - apply (rule exI) - apply (rule exI[of _ "rrename_typ \ U"]) - apply (rule exI[of _ "map_context \ \"]) - apply (rule exI[of _ "rrename_typ \ T"]) - apply (cases t) - unfolding ssbij_def Tmap_def - apply (auto simp: in_context_eqvt supp_inv_bound typ.rrename_comps typ.rrename_comp0s ty_eqvt) - done - done - subgoal - apply (rule disjI2, rule disjI2, rule disjI2, rule disjI1) - apply (elim exE conjE) - subgoal for \ T1 S1 S2 T2 - apply (rule exI[of _ "map_context \ \"]) - apply (rule exI[of _ "rrename_typ \ T1"]) - apply (rule exI[of _ "rrename_typ \ S1"]) - apply (rule exI[of _ "rrename_typ \ S2"]) - apply (rule exI[of _ "rrename_typ \ T2"]) - apply (cases t) unfolding ssbij_def Tmap_def - by (auto simp: in_context_eqvt supp_inv_bound - typ.rrename_comps typ.rrename_comp0s ty_eqvt) - done - apply (rule disjI2)+ - apply (elim exE conjE) - subgoal for \ T1 S1 x S2 T2 - apply (rule exI[of _ "map_context \ \"]) - apply (rule exI[of _ "rrename_typ \ T1"]) - apply (rule exI[of _ "rrename_typ \ S1"]) - apply (rule exI) - apply (rule exI[of _ "rrename_typ \ S2"]) - apply (rule exI[of _ "rrename_typ \ T2"]) - apply (cases t) unfolding ssbij_def Tmap_def - apply (auto simp: in_context_eqvt supp_inv_bound typ.FFVars_rrenames - typ.rrename_comps typ.rrename_comp0s extend_eqvt[symmetric] wf_eqvt ty_eqvt - ) - done + apply (metis (no_types, lifting) UN_subset_iff image_eqI snd_conv subsetD) + using image_iff apply fastforce + apply (auto simp: case_prod_map_prod) + subgoal for \ xs ys b l + apply (drule bspec) + apply assumption + apply (erule case_prodE) + apply (erule bexE) + apply (unfold case_prod_beta) + apply (erule conjE) + by (metis (no_types, opaque_lifting) fst_eqD inv_simp1 snd_eqD typ.rrename_bijs typ.rrename_inv_simps) done -*) lemma fresh: "\xx. xx \ Tfvars t" by (metis emp_bound equals0D imageI inf.commute inf_absorb2 small_Tfvars small_def small_ssbij subsetI) @@ -405,23 +360,23 @@ using finite_iff_le_card_var by blast lemma exists_fresh: "\ z. z \ set xs \ (\t \ set ts. z \ Tfvars t)" proof- - have 0: "|set xs \ \ (Tfvars ` (set ts))| \ (Tfvars ` (set ts))| set xs \ \ (Tfvars ` (set ts))" - by (meson exists_fresh) + by (meson exists_fresh) thus ?thesis by auto qed abbreviation Ii where "Ii \ \(\,S,T). \ \ S <: T" -lemma rrename_swap_FFvars[simp]: "x \ FFVars_typ T \ xx \ FFVars_typ T \ +lemma rrename_swap_FFvars[simp]: "x \ FFVars_typ T \ xx \ FFVars_typ T \ rrename_typ (id(x := xx, xx := x)) T = T" apply(rule typ.rrename_cong_ids) by auto -lemma map_context_swap_FFVars[simp]: -"\k\set \. x \ fst k \ x \ FFVars_typ (snd k) \ - xx \ fst k \ xx \ FFVars_typ (snd k) \ +lemma map_context_swap_FFVars[simp]: +"\k\set \. x \ fst k \ x \ FFVars_typ (snd k) \ + xx \ fst k \ xx \ FFVars_typ (snd k) \ map_context (id(x := xx, xx := x)) \ = \" unfolding map_context_def apply(rule map_idI) by auto @@ -476,10 +431,10 @@ unfolding G_def Tmap_def apply safe using exists_fresh[of "[x]" "[t]"] apply(elim exE conjE) subgoal for xx apply (rule exI[of _ "{xx}"]) apply (intro conjI) - subgoal by simp - subgoal by simp + subgoal by simp + subgoal by simp subgoal apply(rule disjI5_5) - apply(rule exI[of _ "fst t"]) + apply(rule exI[of _ "fst t"]) apply (rule exI[of _ "T\<^sub>1"]) apply (rule exI[of _ "S\<^sub>1"]) apply (rule exI[of _ "xx"]) @@ -494,15 +449,15 @@ unfolding G_def Tmap_def apply safe subgoal premises P using P(2-) using wf_FFVars[OF wf_context[OF P(1)[OF P(5)]]] wf_context[OF P(1)[OF P(6)]] - apply(subgoal_tac "(\k\set \. x \ fst k \ x \ FFVars_typ (snd k)) \ + apply(subgoal_tac "(\k\set \. x \ fst k \ x \ FFVars_typ (snd k)) \ x \ FFVars_typ T\<^sub>1") apply(subst (asm) extend_eqvt, simp, simp) - subgoal apply (auto simp add: ssbij_def) - by (metis image_eqI map_context_swap_FFVars) + subgoal apply (auto simp add: ssbij_def) + by (metis image_eqI map_context_swap_FFVars) subgoal by (auto simp add: ssbij_def) . . . . . . *) -(* +(* using fresh[of t] unfolding G_def Tmap_def apply safe subgoal by (rule exI[of _ "{}"]) auto subgoal by (rule exI[of _ "{}"]) auto @@ -512,7 +467,7 @@ unfolding G_def Tmap_def apply safe apply (rule exI[of _ "{xx}"]) apply (rule conjI) subgoal by auto - apply(rule conjI, simp) + apply(rule conjI, simp) apply (rule disjI2)+ apply (rule exI[of _ "fst t"]) apply (rule exI[of _ "T\<^sub>1"]) @@ -526,7 +481,7 @@ unfolding G_def Tmap_def apply safe subgoal apply (elim conjE) apply (subst Forall_rrename[of "id(x:=xx,xx:=x)"]) - by auto + by auto subgoal for a b c subgoal premises P using P(2-) apply - apply (rule iffD2[OF arg_cong[of _ _ R]]) @@ -534,7 +489,7 @@ unfolding G_def Tmap_def apply safe defer apply (elim allE) apply (erule impE) - prefer 2 + prefer 2 apply assumption apply (rule conjI) apply (simp add: ssbij_def) @@ -551,15 +506,15 @@ unfolding G_def Tmap_def apply safe apply (rule supp_swap_bound) apply (rule infinite_var) apply (erule UnE) - apply auto[1] + apply auto[1] apply (metis P(1) fst_conv image_eqI wf_ConsE wf_context) - apply (drule wf_FFVars[rotated]) - apply (meson P(1) wf_context) + apply (drule wf_FFVars[rotated]) + apply (meson P(1) wf_context) apply (metis P(1) fst_conv fun_upd_apply id_apply wf_ConsE wf_context) apply simp - apply (smt (verit) P(1) Prelim.bij_swap fst_conv fun_upd_apply - id_apply infinite_var list.discI list.inject subset_eq - supp_swap_bound typ.rrename_cong_ids well_scoped(1) + apply (smt (verit) P(1) Prelim.bij_swap fst_conv fun_upd_apply + id_apply infinite_var list.discI list.inject subset_eq + supp_swap_bound typ.rrename_cong_ids well_scoped(1) wf_ty.cases wf_context) . . . . *) @@ -567,9 +522,9 @@ unfolding G_def Tmap_def apply safe interpretation Ty: Induct1 where dummy = "undefined :: var" and Tmap = Tmap and Tfvars = Tfvars and G = G apply standard - using G_mono G_equiv by auto + using G_mono G_equiv by auto -(* Now the proof of this is completely standard, +(* Now the proof of this is completely standard, bacause we use the original operator G: *) lemma ty_I: "ty \ T1 T2 = Ty.I (\, T1, T2)" unfolding ty_def Ty.I_def lfp_curry3 apply(rule arg_cong2[of _ _ _ _ lfp], simp_all) @@ -583,9 +538,9 @@ subgoal for R \\ TT1 TT2 apply(rule iffI) \<^cancel>\SA_Trans_TVar: \ subgoal apply(rule exI[of _ "{}"], rule conjI, simp) apply(rule disjI5_3) by auto \<^cancel>\SA_Arrow: \ - subgoal apply(rule exI[of _ "{}"], rule conjI, simp) apply(rule disjI5_4) by auto + subgoal apply(rule exI[of _ "{}"], rule conjI, simp) apply(rule disjI5_4) by auto \<^cancel>\SA_All: \ - subgoal for T\<^sub>1 S\<^sub>1 x S\<^sub>2 + subgoal for T\<^sub>1 S\<^sub>1 x S\<^sub>2 apply(rule exI[of _ "{x}"], rule conjI, simp) apply(rule disjI5_5) by auto . subgoal apply(elim conjE disjE exE) \<^cancel>\SA_Top: \ @@ -595,7 +550,7 @@ subgoal for R \\ TT1 TT2 apply(rule iffI) \<^cancel>\SA_Trans_TVar: \ subgoal apply(rule disjI5_3) by auto \<^cancel>\SA_Arrow: \ - subgoal apply(rule disjI5_4) by auto + subgoal apply(rule disjI5_4) by auto \<^cancel>\SA_All: \ subgoal for v \ T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2 apply(rule disjI5_5) by fastforce . . . @@ -606,25 +561,25 @@ interpretation ty: Induct where dummy = "undefined :: var" using G_refresh[of R B t] unfolding ty_I by auto . print_theorems -corollary strong_induct_ty[consumes 2, case_names ty SA_Top SA_Refl_TVar SA_Trans_TVar SA_Arrow SA_All]: -assumes par: "\p. small (Pfvars p)" -and ty: "\ \ S <: T" -and SA_Top: "\\ S p. - \ \ ok \ S closed_in \ \ +corollary strong_induct_ty[consumes 2, case_names ty SA_Top SA_Refl_TVar SA_Trans_TVar SA_Arrow SA_All]: +assumes par: "\p. small (Pfvars p)" +and ty: "\ \ S <: T" +and SA_Top: "\\ S p. + \ \ ok \ S closed_in \ \ \ p \ S Top" -and SA_Refl_TVar: "\\ x p. - \ \ ok \ TyVar x closed_in \ \ +and SA_Refl_TVar: "\\ x p. + \ \ ok \ TyVar x closed_in \ \ \ p \ (TyVar x) (TyVar x)" -and SA_Trans_TVar: "\x U \ T p. - x <: U \ \ \ \ \ U <: T \ \p. \ p \ U T \ +and SA_Trans_TVar: "\x U \ T p. + x <: U \ \ \ \ \ U <: T \ \p. \ p \ U T \ \ p \ (TyVar x) T" -and SA_Arrow: "\\ T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2 p. - \ \ T\<^sub>1 <: S\<^sub>1 \ \p. \ p \ T\<^sub>1 S\<^sub>1 \ \ \ S\<^sub>2 <: T\<^sub>2 \ \p. \ p \ S\<^sub>2 T\<^sub>2 \ - \ p \ (S\<^sub>1 \ S\<^sub>2) (T\<^sub>1 \ T\<^sub>2)" -and SA_All: "\\ T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2 p. - x \ Pfvars p \ x \ dom \ \ x \ FFVars_typ S\<^sub>1 \ x \ FFVars_typ T\<^sub>1 \ - \ \ T\<^sub>1 <: S\<^sub>1 \ \p. \ p \ T\<^sub>1 S\<^sub>1 \ \ , x <: T\<^sub>1 \ S\<^sub>2 <: T\<^sub>2 \ - \p. \ p (\ , x <: T\<^sub>1) S\<^sub>2 T\<^sub>2 \ +and SA_Arrow: "\\ T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2 p. + \ \ T\<^sub>1 <: S\<^sub>1 \ \p. \ p \ T\<^sub>1 S\<^sub>1 \ \ \ S\<^sub>2 <: T\<^sub>2 \ \p. \ p \ S\<^sub>2 T\<^sub>2 \ + \ p \ (S\<^sub>1 \ S\<^sub>2) (T\<^sub>1 \ T\<^sub>2)" +and SA_All: "\\ T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2 p. + x \ Pfvars p \ x \ dom \ \ x \ FFVars_typ S\<^sub>1 \ x \ FFVars_typ T\<^sub>1 \ + \ \ T\<^sub>1 <: S\<^sub>1 \ \p. \ p \ T\<^sub>1 S\<^sub>1 \ \ , x <: T\<^sub>1 \ S\<^sub>2 <: T\<^sub>2 \ + \p. \ p (\ , x <: T\<^sub>1) S\<^sub>2 T\<^sub>2 \ \ p \ (\ x <: S\<^sub>1 . S\<^sub>2) (\ x <: T\<^sub>1 . T\<^sub>2)" shows "\ p \ S T" apply(subgoal_tac "case (\, S, T) of (\, S, T) \ \ p \ S T") @@ -632,7 +587,7 @@ apply(subgoal_tac "case (\, S, T) of (\, S, T) \ \, S, T) of (\, S, T) \ \ \ U <: T" +assumes f: "bij f" "|supp f| \ U <: T" shows "(map_context f \) \ (rrename_typ f U) <: (rrename_typ f T)" using assms unfolding ty_I using Ty.I_equiv[of "(\,U,T)" f] unfolding Tmap_def ssbij_def by auto From 659bd049f6ac4ca2e7a21c678a319aa468ff52c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Tue, 26 Mar 2024 13:32:25 +0000 Subject: [PATCH 4/7] Obtain mutual tvsubst function from recursor --- Tools/mrbnf_tvsubst.ML | 433 ++++++++++++++++++++--------------------- operations/TVSubst.thy | 425 ++++++++++++++++++++-------------------- 2 files changed, 423 insertions(+), 435 deletions(-) diff --git a/Tools/mrbnf_tvsubst.ML b/Tools/mrbnf_tvsubst.ML index 895bdbc4..846bbde5 100644 --- a/Tools/mrbnf_tvsubst.ML +++ b/Tools/mrbnf_tvsubst.ML @@ -312,7 +312,7 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models mk_case_tuple (map dest_Free (flat pss)) (@{fold 2} (fn p => fn def => BNF_FP_Util.mk_If (fst (#isVVr def) $ map_id_fst) (p $ (fst (#asVVr def) $ map_id_fst)) - ) ps (map_filter I defs) (ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads + ) (rev ps) (rev (map_filter I defs)) (ctor $ (MRBNF_Def.mk_map_comb_of_mrbnf deads (map HOLogic.id_const plives @ map (fn T => HOLogic.mk_comp ( Term.abs ("R", snd (HOLogic.dest_prodT T)) (Bound 0 $ HOLogic.mk_tuple (flat pss)), snd_const T @@ -334,6 +334,13 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models ) some_defs ps) )) lthy; + val (PFVarss, lthy) = mk_defs_t false (Binding.conglomerate (map #binding models)) qualify "PFVars" 1 + (map (fn i => mk_case_tuple (map dest_Free ps) ( + foldl1 mk_Un (flat (map2 (fn defs => map2 (fn def => fn p => + fst (nth (#IImsupps def) i) $ p + ) (map_filter I defs)) defss pss)) + )) (0 upto length models - 1)) lthy; + val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; @@ -359,7 +366,7 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models compSS = morph compSS }))) defss; - in (defss, map morph Uctors, morph Pmap, morph valid_P, lthy) end; + in (defss, map morph Uctors, morph Pmap, map morph PFVarss, morph valid_P, lthy) end; fun option_map2 f (SOME x) (SOME y) = SOME (f x y) | option_map2 _ _ _ = NONE @@ -371,7 +378,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = val (fp_res, eta_defs, vars, models, lthy) = prove_model_axioms qualify fp_res models lthy; val (((vars, pfrees), plives), pbounds) = vars; - val (defss, Uctors, Pmap, valid_P, lthy) = define_tvsubst_consts qualify fp_res + val (defss, Uctors, Pmap, PFVarss, valid_P, lthy) = define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) models lthy; val nvars = length vars; @@ -608,10 +615,73 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ) (maps (map_filter I) compSS_comp0ss)) ]) end; - val _ = @{print} Pmap_comp0 + val SSupp_naturalss = @{map 3} (fn model => fn quotient => map2 (fn f => Option.map (fn def => + let + val h = Free ("h", #SSfun def); + val goal = mk_Trueprop_eq ( + fst (#SSupp def) $ (HOLogic.mk_comp ( + HOLogic.mk_comp (Term.list_comb (#rename quotient, fs), h), + mk_inv f + )), + mk_image f $ (fst (#SSupp def) $ h) + ); + val inv_simp = infer_instantiate' lthy [SOME (Thm.cterm_of lthy f)] @{thm inv_simp2}; + val eta_naturals = map (fn thm => Local_Defs.unfold0 lthy @{thms comp_def} ( + fun_cong OF [thm] + )) (map_filter (Option.map (#eta_natural o snd)) (#etas model)); + in Goal.prove_sorry lthy (names (fs @ [h])) f_prems goal (fn {context=ctxt, prems} => EVERY1 [ + K (unfold_thms_tac ctxt [snd (#SSupp def)]), + rtac ctxt @{thm iffD2[OF set_eq_iff]}, + rtac ctxt allI, + rtac ctxt iffI, + K (unfold_thms_tac ctxt (snd (#VVr def) :: @{thms mem_Collect_eq comp_def image_Collect})), + etac ctxt @{thm contrapos_np}, + dtac ctxt @{thm Meson.not_exD}, + etac ctxt allE, + dtac ctxt @{thm iffD1[OF de_Morgan_conj]}, + etac ctxt disjE, + EqSubst.eqsubst_asm_tac ctxt [0] [inv_simp], + resolve_tac ctxt prems, + etac ctxt notE, + rtac ctxt refl, + dtac ctxt @{thm notnotD}, + dtac ctxt sym, + etac ctxt @{thm subst}, + rtac ctxt trans, + rtac ctxt (#rename_ctor (#inner quotient)), + REPEAT_DETERM o resolve_tac ctxt prems, + EqSubst.eqsubst_tac ctxt [0] eta_naturals, + REPEAT_DETERM o resolve_tac ctxt prems, + EqSubst.eqsubst_tac ctxt [0] [inv_simp], + resolve_tac ctxt prems, + rtac ctxt refl, + etac ctxt exE, + etac ctxt conjE, + hyp_subst_tac ctxt, + EqSubst.eqsubst_tac ctxt [0] @{thms inv_simp1}, + resolve_tac ctxt prems, + etac ctxt @{thm contrapos_nn}, + dtac ctxt (mk_arg_cong lthy 1 (Term.list_comb (#rename quotient, map mk_inv fs))), + EqSubst.eqsubst_asm_tac ctxt [0] [#rename_comp quotient], + REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems), + REPEAT_DETERM o EVERY' [ + EqSubst.eqsubst_asm_tac ctxt [0] @{thms inv_o_simp1}, + resolve_tac ctxt prems + ], + K (unfold_thms_tac ctxt [#rename_id quotient]), + etac ctxt trans, + rtac ctxt trans, + rtac ctxt (#rename_ctor (#inner quotient)), + REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems), + EqSubst.eqsubst_tac ctxt [0] eta_naturals, + REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems), + EqSubst.eqsubst_tac ctxt [0] @{thms inv_simp1}, + resolve_tac ctxt prems, + rtac ctxt refl + ]) end + )) fs) models (#quotient_fps fp_res) defss; - (* - val IImsupp_VVrs = @{map 3} (fn f => fn i => Option.map (fn def => + val IImsupp_VVrss = map2 (fn quotient => @{map 3} (fn f => fn i => Option.map (fn def => let val a = Free ("a", #aT def); val g = Free ("g", #aT def --> #T quotient); @@ -635,9 +705,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = etac ctxt conjE, assume_tac ctxt ]) end - )) fs (0 upto nvars - 1) defs; + )) fs (0 upto nvars - 1)) (#quotient_fps fp_res) defss; - val IImsupp_imsupp_rrename_commutes = @{map 4} (fn rrename_VVr => fn IImsupp_VVr => fn i => Option.map (fn def => + val IImsupp_imsupp_rrename_commutess = @{map 4} (fn quotient => @{map 4} (fn i => fn rrename_VVr => fn IImsupp_VVr => Option.map (fn def => let val g = Free ("g", #aT def --> #T quotient); val int_empties = map2 (fn f => fn IImsupp => @@ -710,9 +780,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = assume_tac ctxt, resolve_tac ctxt prems ]) end - )) rrename_VVrs IImsupp_VVrs (0 upto nvars - 1) defs; + )) (0 upto nvars - 1)) (#quotient_fps fp_res) rrename_VVrss IImsupp_VVrss defss; - val compSS_cong_ids = map2 (fn rrename_commute => Option.map (fn def => + val compSS_cong_idss = map2 (map2 (fn rrename_commute => Option.map (fn def => let val h = Free ("h", #SSfun def); val IImsupp_prems = map2 (fn IImsupp => fn f => @@ -750,148 +820,52 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = K (unfold_thms_tac ctxt @{thms id_o o_id}), rtac ctxt refl ]) end - )) IImsupp_imsupp_rrename_commutes defs; - - val VVr_thms = @{map 4} (fn rrename_VVr => fn VVr_inj => fn f => Option.map (fn def => - let - val x = Free ("x", #T quotient); - val goal = mk_Trueprop_eq ( - fst (#isVVr def) $ (Term.list_comb (#rename quotient, fs) $ x), - fst (#isVVr def) $ x - ); - val isVVr_rename = Goal.prove_sorry lthy (names (fs @ [x])) (flat f_premss) goal (fn {context=ctxt, prems} => EVERY1 [ - K (unfold_thms_tac ctxt [snd (#isVVr def)]), - rtac ctxt iffI, - etac ctxt exE, - dtac ctxt (mk_arg_cong lthy 1 (Term.list_comb (#rename quotient, map mk_inv fs))), - REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_asm_tac ctxt [0] [@{thm inv_o_simp1}, #rename_comp quotient, the rrename_VVr], - REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems @ @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order}) - ], - K (unfold_thms_tac ctxt [#rename_id quotient]), - rtac ctxt exI, - assume_tac ctxt, - etac ctxt exE, - hyp_subst_tac ctxt, - EqSubst.eqsubst_tac ctxt [0] [the rrename_VVr], - REPEAT_DETERM o resolve_tac ctxt prems, - rtac ctxt exI, - rtac ctxt refl - ]); - - val goal = Logic.mk_implies ( - HOLogic.mk_Trueprop (fst (#isVVr def) $ x), - mk_Trueprop_eq ( - fst (#asVVr def) $ (Term.list_comb (#rename quotient, fs) $ x), - f $ (fst (#asVVr def) $ x) - ) - ); - val asVVr_rename = Goal.prove_sorry lthy (names (fs @ [x])) (flat f_premss) goal (fn {context=ctxt, prems} => EVERY1 [ - K (unfold_thms_tac ctxt (@{thms if_P} @ [snd (#asVVr def), isVVr_rename OF prems])), - K (unfold_thms_tac ctxt [snd (#isVVr def)]), - etac ctxt exE, - hyp_subst_tac ctxt, - EqSubst.eqsubst_tac ctxt [0] [the rrename_VVr], - REPEAT_DETERM o resolve_tac ctxt prems, + ))) IImsupp_imsupp_rrename_commutess defss; + + val asVVr_VVrss = map2 (map2 (fn VVr_inj => Option.map (fn def => + let val a = Free ("a", #aT def) + in Goal.prove_sorry lthy (names [a]) [] + (mk_Trueprop_eq (fst (#asVVr def) $ (fst (#VVr def) $ a), a)) + (fn {context=ctxt, ...} => EVERY1 [ + K (unfold_thms_tac ctxt [snd (#asVVr def), snd (#isVVr def)]), rtac ctxt trans, - rtac ctxt @{thm some_equality}, + rtac ctxt @{thm if_P}, + rtac ctxt exI, rtac ctxt refl, - rtac ctxt (the VVr_inj), - assume_tac ctxt, - rtac ctxt (mk_arg_cong lthy 1 f), - rtac ctxt sym, rtac ctxt @{thm some_equality}, rtac ctxt refl, rtac ctxt (the VVr_inj), assume_tac ctxt - ]); - - val a = Free ("a", #aT def) - val asVVr_VVr = Goal.prove_sorry lthy (names [a]) [] - (mk_Trueprop_eq (fst (#asVVr def) $ (fst (#VVr def) $ a), a)) - (fn {context=ctxt, ...} => EVERY1 [ - K (unfold_thms_tac ctxt [snd (#asVVr def), snd (#isVVr def)]), - rtac ctxt trans, - rtac ctxt @{thm if_P}, - rtac ctxt exI, - rtac ctxt refl, - rtac ctxt @{thm some_equality}, - rtac ctxt refl, - rtac ctxt (the VVr_inj), - assume_tac ctxt - ]); - in { - isVVr_rename = isVVr_rename, - asVVr_rename = asVVr_rename, - asVVr_VVr = asVVr_VVr - } end - )) rrename_VVrs VVr_injs fs defs; + ]) end + ))) VVr_injss defss; - val SSupp_naturals = map2 (fn f => Option.map (fn def => + val isVVr_renamess = @{map 3} (fn quotient => map2 (fn rrename_VVr => Option.map (fn def => let - val h = Free ("h", #SSfun def); + val x = Free ("x", #T quotient); val goal = mk_Trueprop_eq ( - fst (#SSupp def) $ (HOLogic.mk_comp ( - HOLogic.mk_comp (Term.list_comb (#rename quotient, fs), h), - mk_inv f - )), - mk_image f $ (fst (#SSupp def) $ h) + fst (#isVVr def) $ (Term.list_comb (#rename quotient, fs) $ x), + fst (#isVVr def) $ x ); - val inv_simp = infer_instantiate' lthy [SOME (Thm.cterm_of lthy f)] @{thm inv_simp2}; - val eta_naturals = map (fn thm => Local_Defs.unfold0 lthy @{thms comp_def} ( - fun_cong OF [thm] - )) (map_filter (Option.map (#eta_natural o snd)) (#etas model)); - in Goal.prove_sorry lthy (names (fs @ [h])) f_prems goal (fn {context=ctxt, prems} => EVERY1 [ - K (unfold_thms_tac ctxt [snd (#SSupp def)]), - rtac ctxt @{thm iffD2[OF set_eq_iff]}, - rtac ctxt allI, + in Goal.prove_sorry lthy (names (fs @ [x])) f_prems goal (fn {context=ctxt, prems} => EVERY1 [ + K (unfold_thms_tac ctxt [snd (#isVVr def)]), rtac ctxt iffI, - K (unfold_thms_tac ctxt (snd (#VVr def) :: @{thms mem_Collect_eq comp_def image_Collect})), - etac ctxt @{thm contrapos_np}, - dtac ctxt @{thm Meson.not_exD}, - etac ctxt allE, - dtac ctxt @{thm iffD1[OF de_Morgan_conj]}, - etac ctxt disjE, - EqSubst.eqsubst_asm_tac ctxt [0] [inv_simp], - resolve_tac ctxt prems, - etac ctxt notE, - rtac ctxt refl, - dtac ctxt @{thm notnotD}, - dtac ctxt sym, - etac ctxt @{thm subst}, - rtac ctxt trans, - rtac ctxt (#rename_ctor (#inner quotient)), - REPEAT_DETERM o resolve_tac ctxt prems, - EqSubst.eqsubst_tac ctxt [0] eta_naturals, - REPEAT_DETERM o resolve_tac ctxt prems, - EqSubst.eqsubst_tac ctxt [0] [inv_simp], - resolve_tac ctxt prems, - rtac ctxt refl, etac ctxt exE, - etac ctxt conjE, - hyp_subst_tac ctxt, - EqSubst.eqsubst_tac ctxt [0] @{thms inv_simp1}, - resolve_tac ctxt prems, - etac ctxt @{thm contrapos_nn}, dtac ctxt (mk_arg_cong lthy 1 (Term.list_comb (#rename quotient, map mk_inv fs))), - EqSubst.eqsubst_asm_tac ctxt [0] [#rename_comp quotient], - REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems), REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_asm_tac ctxt [0] @{thms inv_o_simp1}, - resolve_tac ctxt prems + EqSubst.eqsubst_asm_tac ctxt [0] [@{thm inv_o_simp1}, #rename_comp quotient, the rrename_VVr], + REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems @ @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order}) ], K (unfold_thms_tac ctxt [#rename_id quotient]), - etac ctxt trans, - rtac ctxt trans, - rtac ctxt (#rename_ctor (#inner quotient)), - REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems), - EqSubst.eqsubst_tac ctxt [0] eta_naturals, - REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems), - EqSubst.eqsubst_tac ctxt [0] @{thms inv_simp1}, - resolve_tac ctxt prems, + rtac ctxt exI, + assume_tac ctxt, + etac ctxt exE, + hyp_subst_tac ctxt, + EqSubst.eqsubst_tac ctxt [0] [the rrename_VVr], + REPEAT_DETERM o resolve_tac ctxt prems, + rtac ctxt exI, rtac ctxt refl ]) end - )) fs defs; + ))) (#quotient_fps fp_res) rrename_VVrss defss; val valid_Pmap = let @@ -901,7 +875,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = )); in Goal.prove_sorry lthy (names (fs @ [p])) f_prems' goal (fn {context=ctxt, prems} => EVERY1 [ K (unfold_thms_tac ctxt (@{thms case_prod_beta fst_conv snd_conv} - @ map (snd o #compSS) some_defs + @ map (snd o #compSS) (flat some_defss) @ [snd Pmap, snd valid_P] )), REPEAT_DETERM o etac ctxt conjE, @@ -909,10 +883,11 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = assume_tac ctxt, resolve_tac ctxt (@{thms conjI supp_inv_bound} @ prems @ maps (fn thms => [#SSupp_comp_bound thms, #SSupp_comp_rename_bound thms] - ) (map_filter I SSupp_comps)) + ) (maps (map_filter I) SSupp_compss)) ] ]) end; + val some_defs = flat some_defss; fun Pmap_id0_tac ctxt = EVERY1 [ rtac ctxt trans, rtac ctxt (fun_cong OF [Pmap_id0]), @@ -923,9 +898,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = REPEAT_DETERM o assume_tac ctxt ]; fun Pmap_cong_id_tac ctxt = EVERY1 [ - K (unfold_thms_tac ctxt (snd Pmap :: @{thms case_prod_beta})), + K (unfold_thms_tac ctxt (snd Pmap :: map snd PFVarss @ @{thms case_prod_beta})), Subgoal.FOCUS_PREMS (fn {context=ctxt, prems, ...} => REPEAT_DETERM (EVERY1 [ - EqSubst.eqsubst_tac ctxt [0] (map_filter I compSS_cong_ids), + EqSubst.eqsubst_tac ctxt [0] (maps (map_filter I) compSS_cong_idss), REPEAT_DETERM o FIRST' [ assume_tac ctxt, resolve_tac ctxt (prems @ @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order}), @@ -937,21 +912,21 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = rtac ctxt refl ]; fun PFVars_Pmap_tac ctxt = EVERY1 [ - K (unfold_thms_tac ctxt (snd Pmap :: @{thms case_prod_beta fst_conv snd_conv})), + K (unfold_thms_tac ctxt (snd Pmap :: map snd PFVarss @ @{thms case_prod_beta fst_conv snd_conv})), K (unfold_thms_tac ctxt (@{thm image_Un} :: map (snd o #compSS) some_defs)), REPEAT_DETERM o rtac ctxt @{thm arg_cong2[of _ _ _ _ "(\)"]}, REPEAT_DETERM o EVERY' [ SELECT_GOAL (unfold_thms_tac ctxt (maps (map snd o #IImsupps) some_defs)), K (unfold_thms_tac ctxt @{thms image_comp[symmetric]}), EqSubst.eqsubst_tac ctxt [0] @{thms image_comp[unfolded comp_def]}, - EqSubst.eqsubst_tac ctxt [0] (#FVars_renames quotient), + EqSubst.eqsubst_tac ctxt [0] (maps #FVars_renames (#quotient_fps fp_res)), REPEAT_DETERM o FIRST' [ assume_tac ctxt, resolve_tac ctxt @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order} ], K (unfold_thms_tac ctxt @{thms image_UN[symmetric]}), REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_tac ctxt [0] (map_filter I SSupp_naturals), + EqSubst.eqsubst_tac ctxt [0] (maps (map_filter I) SSupp_naturalss), REPEAT_DETERM o FIRST' [ assume_tac ctxt, resolve_tac ctxt @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order} @@ -966,13 +941,17 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ]; fun small_PFVars_tac ctxt = EVERY1 [ K (unfold_thms_tac ctxt (@{thms case_prod_beta comp_def} + @ map snd PFVarss @ maps (map snd o #IImsupps) some_defs @ [snd Pmap, snd valid_P] )), REPEAT_DETERM o etac ctxt conjE, REPEAT_DETERM o FIRST' [ assume_tac ctxt, - resolve_tac ctxt ([Un_bound, UNION_bound] @ #card_of_FVars_bound_UNIVs quotient @ @{thms cmin_greater card_of_Card_order}) + resolve_tac ctxt ([Un_bound, UNION_bound] + @ maps #card_of_FVars_bound_UNIVs (#quotient_fps fp_res) + @ @{thms cmin_greater card_of_Card_order} + ) ] ]; fun valid_Pmap_tac ctxt = EVERY1 [ @@ -980,8 +959,8 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = REPEAT_DETERM o assume_tac ctxt ]; - fun rrename_Uctor_tac ctxt = EVERY1 [ - K (unfold_thms_tac ctxt [snd Uctor]), + fun mk_rrename_Uctor_tac mrbnf quotient ctxt = EVERY1 [ + K (unfold_thms_tac ctxt (map snd Uctors)), REPEAT_DETERM o EVERY' [ EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], REPEAT_DETERM o FIRST' [ @@ -1003,9 +982,7 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ] ], REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_tac ctxt [0] ((#rename_ctor (#inner quotient) RS sym) :: map_filter (Option.map (fn thms => - #isVVr_rename thms - )) VVr_thms), + EqSubst.eqsubst_tac ctxt [0] ((#rename_ctor (#inner quotient) RS sym) :: maps (map_filter I) isVVr_renamess), REPEAT_DETERM o FIRST' [ assume_tac ctxt, resolve_tac ctxt @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order} @@ -1021,16 +998,16 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = dtac ctxt sym, etac ctxt @{thm subst}, SELECT_GOAL (unfold_thms_tac ctxt (@{thms case_prod_beta fst_conv snd_conv} - @ map_filter (Option.map #asVVr_VVr) VVr_thms + @ maps (map_filter I) asVVr_VVrss @ [snd Pmap] )), - EqSubst.eqsubst_tac ctxt [0] (map_filter I rrename_VVrs), + EqSubst.eqsubst_tac ctxt [0] (maps (map_filter I) rrename_VVrss), REPEAT_DETERM o FIRST' [ assume_tac ctxt, resolve_tac ctxt @{thms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order} ], SELECT_GOAL (unfold_thms_tac ctxt (@{thms comp_def} @ map (snd o #compSS) some_defs - @ map_filter (Option.map #asVVr_VVr) VVr_thms + @ maps (map_filter I) asVVr_VVrss )), EqSubst.eqsubst_tac ctxt [0] @{thms inv_simp1}, assume_tac ctxt, @@ -1071,67 +1048,69 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = K (unfold_thms_tac ctxt @{thms if_True}), rtac ctxt refl ]; - fun mk_FVars_subset_tac FVars i ctxt = EVERY1 [ - K (unfold_thms_tac ctxt @{thms Un_empty_right case_prod_beta}), - Subgoal.FOCUS_PREMS (fn {context=ctxt, prems, ...} => EVERY1 [ - K (unfold_thms_tac ctxt [snd Uctor, @{thm case_prod_beta}]), - EVERY' (map_index (fn (j, def) => EVERY' [ - rtac ctxt @{thm case_split}, - EqSubst.eqsubst_tac ctxt [0] @{thms if_P}, - assume_tac ctxt, - SELECT_GOAL (unfold_thms_tac ctxt (map_filter (Option.map (snd o #isVVr)) defs)), - etac ctxt exE, - dtac ctxt sym, - etac ctxt @{thm subst}, - K (unfold_thms_tac ctxt (map_filter (Option.map #asVVr_VVr) VVr_thms)), - rtac ctxt @{thm case_split[of "_ = _"]}, - rtac ctxt @{thm iffD2[OF arg_cong2[OF _ refl, of _ _ "(\)"]]}, - rtac ctxt (mk_arg_cong lthy 1 FVars), - assume_tac ctxt, + + fun mk_FVars_subset_tac mrbnf quotient defs n FVars i ctxt = + let val some_defs = map_filter I defs; + in EVERY1 [ + K (unfold_thms_tac ctxt @{thms Un_empty_right case_prod_beta}), + Subgoal.FOCUS_PREMS (fn {context=ctxt, prems, ...} => EVERY1 [ + K (unfold_thms_tac ctxt (map snd Uctors @ @{thms case_prod_beta})), + EVERY' (map_index (fn (j, def) => EVERY' [ + rtac ctxt @{thm case_split}, + EqSubst.eqsubst_tac ctxt [0] @{thms if_P}, + assume_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt [snd (#isVVr def)]), + etac ctxt exE, + dtac ctxt sym, + etac ctxt @{thm subst}, + K (unfold_thms_tac ctxt (maps (map_filter I) asVVr_VVrss)), + rtac ctxt @{thm case_split[of "_ = _"]}, + rtac ctxt @{thm iffD2[OF arg_cong2[OF _ refl, of _ _ "(\)"]]}, + rtac ctxt (mk_arg_cong lthy 1 FVars), + assume_tac ctxt, + rtac ctxt @{thm Un_upper1}, + rtac ctxt subsetI, + rtac ctxt UnI2, + SELECT_GOAL (unfold_thms_tac ctxt (map snd PFVarss + @ [snd (#SSupp def), snd (nth (#IImsupps def) i)] + @ @{thms case_prod_beta} + )), + rtac ctxt (BNF_Util.mk_UnIN (length (flat some_defss)) (n + j + 1)), + TRY o rtac ctxt UnI2, + rtac ctxt @{thm UN_I}, + rtac ctxt @{thm CollectI}, + assume_tac ctxt, + rtac ctxt @{thm iffD2[OF arg_cong2[OF refl comp_apply, of "(\)"]]}, + assume_tac ctxt, + K (unfold_thms_tac ctxt @{thms if_not_P}) + ]) some_defs), + K (unfold_thms_tac ctxt (#FVars_ctors quotient)), + REPEAT_DETERM o EVERY' [ + EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf), + REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id} + ], + K (unfold_thms_tac ctxt @{thms image_id image_comp comp_def}), + REPEAT_DETERM o rtac ctxt @{thm Un_mono'}, rtac ctxt @{thm Un_upper1}, - rtac ctxt subsetI, - rtac ctxt UnI2, - SELECT_GOAL (unfold_thms_tac ctxt [snd (#SSupp def), snd (nth (#IImsupps def) i)]), - rtac ctxt (BNF_Util.mk_UnIN (length some_defs) (j + 1)), - TRY o rtac ctxt UnI2, - rtac ctxt @{thm UN_I}, - rtac ctxt @{thm CollectI}, - assume_tac ctxt, - rtac ctxt @{thm iffD2[OF arg_cong2[OF refl comp_apply, of "(\)"]]}, - assume_tac ctxt, - K (unfold_thms_tac ctxt @{thms if_not_P}) - ]) some_defs), - K (unfold_thms_tac ctxt (#FVars_ctors quotient)), - REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf), - REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id} - ], - K (unfold_thms_tac ctxt @{thms image_id image_comp comp_def}), - REPEAT_DETERM o rtac ctxt @{thm Un_mono'}, - rtac ctxt @{thm Un_upper1}, - REPEAT_DETERM o EVERY' [ - TRY o EVERY' [ - rtac ctxt @{thm iffD2[OF arg_cong2[OF refl, of _ _ "(\)"]]}, - rtac ctxt @{thm Diff_Un_disjunct}, + REPEAT_DETERM o EVERY' [ + TRY o EVERY' [ + rtac ctxt @{thm iffD2[OF arg_cong2[OF refl, of _ _ "(\)"]]}, + rtac ctxt @{thm Diff_Un_disjunct}, + resolve_tac ctxt prems, + rtac ctxt @{thm Diff_mono[OF _ subset_refl]} + ], + SELECT_GOAL (unfold_thms_tac ctxt @{thms UN_extend_simps(2)}), + rtac ctxt @{thm subset_If}, + SELECT_GOAL (unfold_thms_tac ctxt @{thms UN_empty'}), + rtac ctxt @{thm empty_subsetI}, + rtac ctxt @{thm UN_mono[OF subset_refl]}, resolve_tac ctxt prems, - rtac ctxt @{thm Diff_mono[OF _ subset_refl]} - ], - SELECT_GOAL (unfold_thms_tac ctxt @{thms UN_extend_simps(2)}), - rtac ctxt @{thm subset_If}, - SELECT_GOAL (unfold_thms_tac ctxt @{thms UN_empty'}), - rtac ctxt @{thm empty_subsetI}, - rtac ctxt @{thm UN_mono[OF subset_refl]}, - resolve_tac ctxt prems, - K (unfold_thms_tac ctxt @{thms prod.collapse}), - resolve_tac ctxt prems, - eresolve_tac ctxt @{thms UnI1 UnI2} - ] - ]) ctxt - ]; - - val PFVarss = map (fn i => mk_case_tuple (map dest_Free ps) ( - foldl1 mk_Un (map2 (fn p => fn def => fst (nth (#IImsupps def) i) $ p) ps some_defs) - )) (0 upto nvars - 1); + K (unfold_thms_tac ctxt @{thms prod.collapse}), + resolve_tac ctxt prems, + eresolve_tac ctxt @{thms UnI1 UnI2} + ] + ]) ctxt + ] end; val parameter_axioms = { Pmap_id0 = Pmap_id0_tac, @@ -1141,14 +1120,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = small_PFVarss = replicate nvars small_PFVars_tac, small_avoiding_sets = replicate nvars (fn ctxt => rtac ctxt (@{thm Cinfinite_gt_empty} OF [Cinfinite_card]) 1) }; - val model_axioms = { - rrename_Uctor = rrename_Uctor_tac, - FVars_subsets = map2 mk_FVars_subset_tac (#FVars quotient) (0 upto nvars - 1) - }; - val parameters = { P = HOLogic.mk_tupleT P_Ts, - PFVarss = PFVarss, + PFVarss = map fst PFVarss, Pmap = fst Pmap, avoiding_sets = map mk_bot vars, validity = SOME { @@ -1158,15 +1132,26 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = axioms = parameter_axioms, min_bound = true } : (Proof.context -> tactic) MRBNF_Recursor.parameter; - val rec_model = MRBNF_Recursor.mk_quotient_model quotient [] { - binding = b, - Uctor = fst Uctor, - validity = NONE, - axioms = model_axioms - } : (Proof.context -> tactic) MRBNF_Recursor.model; - - val (rec_ress, lthy) = MRBNF_Recursor.create_binding_recursor qualify (#fp_result model) parameters [rec_model] lthy; - val rec_res = hd rec_ress; + + val rec_models = fst (@{fold_map 5} (fn quotient => fn mrbnf => fn model => fn Uctor => fn defs => fn n => + (MRBNF_Recursor.mk_quotient_model quotient [] { + binding = #binding model, + Uctor = fst Uctor, + validity = NONE, + axioms = { + rrename_Uctor = mk_rrename_Uctor_tac mrbnf quotient, + FVars_subsets = map2 (mk_FVars_subset_tac mrbnf quotient defs n) (#FVars quotient) (0 upto nvars - 1) + } + } : (Proof.context -> tactic) MRBNF_Recursor.model, n + length (map_filter I defs)) + ) (#quotient_fps fp_res) (#pre_mrbnfs fp_res) models Uctors defss 0); + + val (rec_ress, lthy) = MRBNF_Recursor.create_binding_recursor qualify fp_res parameters rec_models lthy; + val _ = @{print} rec_ress + + (* + fun mk_FVars_subset_tac FVars i ctxt = EVERY1 [ + + ]; val (_, lthy) = Local_Theory.begin_nested lthy; diff --git a/operations/TVSubst.thy b/operations/TVSubst.thy index 83d099a3..b26d5049 100644 --- a/operations/TVSubst.thy +++ b/operations/TVSubst.thy @@ -585,103 +585,6 @@ lemma SSupp_natural: done done -lemma PFVars_Pmaps: - fixes f1::"'var::{var_T1_pre, var_T2_pre} \ 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" - assumes f_prems: "bij f1" "|supp f1| )"])+ - (* REPEAT_DETERM *) - apply (unfold IImsupp11_1_def) - apply (unfold image_comp[symmetric]) - apply (subst image_comp[unfolded comp_def]) - apply (subst T1.FFVars_rrenames) - apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ - apply (unfold image_UN[symmetric]) - apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ - apply (unfold image_comp) - apply (subst inv_o_simp1) - apply (rule assms) - apply (unfold o_id image_Un) - apply (rule refl) - (* copied from above *) - apply (unfold IImsupp12_1_def) - apply (unfold image_comp[symmetric]) - apply (subst image_comp[unfolded comp_def]) - apply (subst T1.FFVars_rrenames) - apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ - apply (unfold image_UN[symmetric]) - apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ - apply (unfold image_comp) - apply (subst inv_o_simp1) - apply (rule assms) - apply (unfold o_id image_Un) - apply (rule refl) - (* copied from above *) - apply (unfold IImsupp21_1_def) - apply (unfold image_comp[symmetric]) - apply (subst image_comp[unfolded comp_def]) - apply (subst T1.FFVars_rrenames) - apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ - apply (unfold image_UN[symmetric]) - apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ - apply (unfold image_comp) - apply (subst inv_o_simp1) - apply (rule assms) - apply (unfold o_id image_Un) - apply (rule refl) - (* END REPEAT_DETERM *) - done - subgoal - apply (unfold Pmap_def PFVars_2_def case_prod_beta fst_conv snd_conv) - apply (unfold compSS_defs image_Un) - apply (rule arg_cong2[of _ _ _ _ "(\)"])+ - (* REPEAT_DETERM *) - apply (unfold IImsupp11_2_def) - apply (unfold image_comp[symmetric]) - apply (subst image_comp[unfolded comp_def]) - apply (subst T1.FFVars_rrenames) - apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ - apply (unfold image_UN[symmetric]) - apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ - apply (unfold image_comp) - apply (subst inv_o_simp1) - apply (rule assms) - apply (unfold o_id image_Un) - apply (rule refl) - (* copied from above *) - apply (unfold IImsupp12_2_def) - apply (unfold image_comp[symmetric]) - apply (subst image_comp[unfolded comp_def]) - apply (subst T1.FFVars_rrenames) - apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ - apply (unfold image_UN[symmetric]) - apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ - apply (unfold image_comp) - apply (subst inv_o_simp1) - apply (rule assms) - apply (unfold o_id image_Un) - apply (rule refl) - (* copied from above *) - apply (unfold IImsupp21_2_def) - apply (unfold image_comp[symmetric]) - apply (subst image_comp[unfolded comp_def]) - apply (subst T1.FFVars_rrenames) - apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ - apply (unfold image_UN[symmetric]) - apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ - apply (unfold image_comp) - apply (subst inv_o_simp1) - apply (rule assms) - apply (unfold o_id image_Un) - apply (rule refl) - (* END REPEAT_DETERM *) - done - done - lemma IImsupp_VVrs: "f a \ a \ imsupp f \ IImsupp11_1 y = {} \ y a = VVr11 a" "f2 b \ b \ imsupp f2 \ IImsupp12_2 y2 = {} \ y2 b = VVr12 b" @@ -949,7 +852,6 @@ lemma IImsupp_rrename_commute: done done - lemma compSS_cong_ids: fixes f1::"'var::{var_T1_pre, var_T2_pre} \ 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" assumes f_prems: "bij f1" "|supp f1| 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" - assumes f_prems: "bij f1" "|supp f1| a. a \ PFVars_1 p \ f1 a = a) \ (\a. a \ PFVars_2 p \ f2 a = a) \ Pmap f1 f2 p = p" - apply (unfold PFVars_1_def PFVars_2_def Pmap_def case_prod_beta) - subgoal premises prems - apply (subst compSS_cong_ids, (rule f_prems prems ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order | erule UnI2 UnI1 | rule UnI1)+)+ - apply (unfold prod.collapse) - apply (rule refl) - done - done - -lemma small_PFVarss: - "valid_P p \ |PFVars_1 (p::('var::{var_T1_pre,var_T2_pre}, 'tyvar::{var_T1_pre,var_T2_pre}, 'a::{var_T1_pre,var_T2_pre}, 'b) P)| |PFVars_2 p| 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" + assumes f_prems: "bij f1" "|supp f1| + bij f1 \ |supp (f1::'var::{var_T1_pre,var_T2_pre} \ 'var)| + bij f2 \ |supp (f2::'tyvar::{var_T1_pre,var_T2_pre} \ 'tyvar)| + valid_P (Pmap f1 f2 p)" + apply (unfold valid_P_def Pmap_def case_prod_beta compSS_defs fst_conv snd_conv) + apply (erule conjE)+ + apply (assumption | rule conjI SSupp_comp_bounds SSupp_rename_bounds supp_inv_bound)+ + done + +(**************************************) +(***** Needed as tactics only *********) +(**************************************) + +lemma PFVars_Pmaps: + fixes f1::"'var::{var_T1_pre, var_T2_pre} \ 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" + assumes f_prems: "bij f1" "|supp f1| )"])+ + (* REPEAT_DETERM *) + apply (unfold IImsupp11_1_def) + apply (unfold image_comp[symmetric]) + apply (subst image_comp[unfolded comp_def]) + apply (subst T1.FFVars_rrenames) + apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ + apply (unfold image_UN[symmetric]) + apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ + apply (unfold image_comp) + apply (subst inv_o_simp1) + apply (rule assms) + apply (unfold o_id image_Un) + apply (rule refl) + (* copied from above *) + apply (unfold IImsupp12_1_def) + apply (unfold image_comp[symmetric]) + apply (subst image_comp[unfolded comp_def]) + apply (subst T1.FFVars_rrenames) + apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ + apply (unfold image_UN[symmetric]) + apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ + apply (unfold image_comp) + apply (subst inv_o_simp1) + apply (rule assms) + apply (unfold o_id image_Un) + apply (rule refl) + (* copied from above *) + apply (unfold IImsupp21_1_def) + apply (unfold image_comp[symmetric]) + apply (subst image_comp[unfolded comp_def]) + apply (subst T1.FFVars_rrenames) + apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ + apply (unfold image_UN[symmetric]) + apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ + apply (unfold image_comp) + apply (subst inv_o_simp1) + apply (rule assms) + apply (unfold o_id image_Un) + apply (rule refl) + (* END REPEAT_DETERM *) + done + subgoal + apply (unfold Pmap_def PFVars_2_def case_prod_beta fst_conv snd_conv) + apply (unfold compSS_defs image_Un) + apply (rule arg_cong2[of _ _ _ _ "(\)"])+ + (* REPEAT_DETERM *) + apply (unfold IImsupp11_2_def) + apply (unfold image_comp[symmetric]) + apply (subst image_comp[unfolded comp_def]) + apply (subst T1.FFVars_rrenames) + apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ + apply (unfold image_UN[symmetric]) + apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ + apply (unfold image_comp) + apply (subst inv_o_simp1) + apply (rule assms) + apply (unfold o_id image_Un) + apply (rule refl) + (* copied from above *) + apply (unfold IImsupp12_2_def) + apply (unfold image_comp[symmetric]) + apply (subst image_comp[unfolded comp_def]) + apply (subst T1.FFVars_rrenames) + apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ + apply (unfold image_UN[symmetric]) + apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ + apply (unfold image_comp) + apply (subst inv_o_simp1) + apply (rule assms) + apply (unfold o_id image_Un) + apply (rule refl) + (* copied from above *) + apply (unfold IImsupp21_2_def) + apply (unfold image_comp[symmetric]) + apply (subst image_comp[unfolded comp_def]) + apply (subst T1.FFVars_rrenames) + apply (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+ + apply (unfold image_UN[symmetric]) + apply (subst SSupp_natural, (rule assms ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order)+)+ + apply (unfold image_comp) + apply (subst inv_o_simp1) + apply (rule assms) + apply (unfold o_id image_Un) + apply (rule refl) + (* END REPEAT_DETERM *) + done + done + +lemma Pmap_cong_id: + fixes f1::"'var::{var_T1_pre, var_T2_pre} \ 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" + assumes f_prems: "bij f1" "|supp f1| a. a \ PFVars_1 p \ f1 a = a) \ (\a. a \ PFVars_2 p \ f2 a = a) \ Pmap f1 f2 p = p" + apply (unfold PFVars_1_def PFVars_2_def Pmap_def case_prod_beta) + subgoal premises prems + apply (subst compSS_cong_ids, (rule f_prems prems ordLess_ordLeq_trans cmin1 cmin2 card_of_Card_order | erule UnI2 UnI1 | rule UnI1)+)+ + apply (unfold prod.collapse) + apply (rule refl) + done + done + +lemma small_PFVarss: + "valid_P p \ |PFVars_1 (p::('var::{var_T1_pre,var_T2_pre}, 'tyvar::{var_T1_pre,var_T2_pre}, 'a::{var_T1_pre,var_T2_pre}, 'b) P)| |PFVars_2 p| set5_T1_pre (y::(_, _, 'a::{var_T1_pre,var_T2_pre}, 'b, _, _, _, _, _, _) T1_pre) \ (PFVars_1 p \ avoiding_set1) = {} \ (\t pu p. valid_P p \ (t, pu) \ set7_T1_pre y \ set8_T1_pre y \ U1FVars_1 t (pu p) \ FFVars_T11 t \ PFVars_1 p \ avoiding_set1) \ (\t pu p. valid_P p \ (t, pu) \ set9_T1_pre y \ set10_T1_pre y \ U2FVars_1 t (pu p) \ FFVars_T21 t \ PFVars_1 p \ avoiding_set1) \ @@ -1203,7 +1283,7 @@ lemma U1FVars_subset_1: "valid_P p \ set5_T1_pre (y::(_, _, 'a:: apply (tactic \resolve_tac @{context} [BNF_Util.mk_UnIN 3 1] 1\) apply (rule UnI2)? apply (rule UN_I) - apply (rule iffD2[OF mem_Collect_eq]) + apply (rule CollectI) apply assumption apply (rule iffD2[OF arg_cong2[OF refl comp_apply, of "(\)"]]) apply assumption @@ -1552,83 +1632,6 @@ lemma U2FVars_subset_2: "valid_P p \ set6_T2_pre (y::('var::{var done done -lemma isVVr_renames: -fixes f1::"'var::{var_T1_pre, var_T2_pre} \ 'var" and f2::"'tyvar::{var_T1_pre, var_T2_pre} \ 'tyvar" - assumes f_prems: "bij f1" "|supp f1| - bij f1 \ |supp (f1::'var::{var_T1_pre,var_T2_pre} \ 'var)| - bij f2 \ |supp (f2::'tyvar::{var_T1_pre,var_T2_pre} \ 'tyvar)| - valid_P (Pmap f1 f2 p)" - apply (unfold valid_P_def Pmap_def case_prod_beta compSS_defs fst_conv snd_conv) - apply (erule conjE)+ - apply (assumption | rule conjI SSupp_comp_bounds SSupp_rename_bounds supp_inv_bound)+ - done - lemma U1map_Uctor: "valid_P p \ bij f1 \ |supp (f1::'var::{var_T1_pre,var_T2_pre} \ 'var)| bij f2 \ |supp (f2::'tyvar::{var_T1_pre,var_T2_pre} \ 'tyvar)| U1map f1 f2 (T1_ctor (map_T1_pre id id id id id id fst fst fst fst y)) (U1ctor y p) = U1ctor (map_T1_pre f1 f2 id id f1 f2 From d8c025772b0a85a59321244bf79e537daa95a2a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Wed, 27 Mar 2024 15:47:47 +0000 Subject: [PATCH 5/7] Adjust mrbnf_sugar to work with mutual tvsubst --- Tools/mrbnf_sugar.ML | 5 +- Tools/mrbnf_tvsubst.ML | 386 ++++++++++++++++++++++------------------- operations/Sugar.thy | 8 +- 3 files changed, 211 insertions(+), 188 deletions(-) diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML index 6733df4d..b861d4b2 100644 --- a/Tools/mrbnf_sugar.ML +++ b/Tools/mrbnf_sugar.ML @@ -429,7 +429,7 @@ fun create_binder_datatype (spec : spec) lthy = eta_natural = eta_natural_tac }; val tvsubst_model = { - fp_result = res, + binding = #tvsubst_b spec, etas = map (fn a => Option.map (rpair tvsubst_axioms) ( List.find (fn t => domain_type (fastype_of t) = a) etas )) vars @@ -586,7 +586,8 @@ fun create_binder_datatype (spec : spec) lthy = val (lthy, tvsubst_opt) = if not (null (map_filter I (#etas tvsubst_model))) then let - val (tvsubst_res, lthy) = MRBNF_TVSubst.create_tvsubst_of_mrbnf (#tvsubst_b spec) (Binding.prefix_name "tv") tvsubst_model lthy; + val (tvsubst_ress, lthy) = MRBNF_TVSubst.create_tvsubst_of_mrbnf (Binding.prefix_name "tv") res [tvsubst_model] lthy; + val tvsubst_res = hd tvsubst_ress; val tvsubst_simps = let val (fs, _) = lthy diff --git a/Tools/mrbnf_tvsubst.ML b/Tools/mrbnf_tvsubst.ML index 846bbde5..ddd319a6 100644 --- a/Tools/mrbnf_tvsubst.ML +++ b/Tools/mrbnf_tvsubst.ML @@ -24,7 +24,7 @@ sig val create_tvsubst_of_mrbnf: (binding -> binding) -> MRBNF_FP_Def_Sugar.fp_result -> (Proof.context -> tactic) tvsubst_model list -> local_theory - -> tvsubst_result * local_theory + -> tvsubst_result list * local_theory end structure MRBNF_TVSubst : MRBNF_TVSUBST = @@ -177,8 +177,8 @@ fun prove_model_axioms qualify res (models : (Proof.context -> tactic) tvsubst_m replicate (nvars + pfree) sort @ replicate plive @{sort type} @ replicate pbound sort ) lthy; val ctor = #ctor (hd (#quotient_fps res)); - val vars = rev (Term.add_tvars ctor []); - val res = MRBNF_FP_Def_Sugar.substitute_vars (map TVar vars ~~ Ts) res + val vars = map TVar (rev (Term.add_tvars ctor [])) @ map TFree (rev (Term.add_tfrees ctor [])); + val res = MRBNF_FP_Def_Sugar.substitute_vars (vars ~~ Ts) res val ctor = #ctor (hd (#quotient_fps res)); val args = snd (dest_Type (domain_type (fastype_of ctor))); @@ -222,7 +222,7 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models val (_, lthy) = Local_Theory.begin_nested lthy; - val (defss, lthy) = @{fold_map 4} (fn mrbnf => fn quot => fn model => fn suffix => + val (defss, lthy) = @{fold_map 3} (fn quot => fn model => fn suffix => @{fold_map 3} (fn eta_opt => fn suffix => fn i => fn lthy => let val opt = Option.map (fn (eta, _) => let val qT = #T quot; @@ -284,7 +284,7 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models ) eta_opt in ( Option.map fst opt, the_default lthy (Option.map snd opt)) end) (#etas model) suffix (0 upto nvars - 1) - ) (#pre_mrbnfs fp_res) (#quotient_fps fp_res) models suffixes lthy; + ) (#quotient_fps fp_res) models suffixes lthy; val P_Tss = map (map_filter (Option.map #SSfun)) defss; val P_T = HOLogic.mk_tupleT (flat P_Tss); @@ -339,7 +339,7 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models foldl1 mk_Un (flat (map2 (fn defs => map2 (fn def => fn p => fst (nth (#IImsupps def) i) $ p ) (map_filter I defs)) defss pss)) - )) (0 upto length models - 1)) lthy; + )) (0 upto nvars - 1)) lthy; val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; @@ -1146,40 +1146,44 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ) (#quotient_fps fp_res) (#pre_mrbnfs fp_res) models Uctors defss 0); val (rec_ress, lthy) = MRBNF_Recursor.create_binding_recursor qualify fp_res parameters rec_models lthy; - val _ = @{print} rec_ress - - (* - fun mk_FVars_subset_tac FVars i ctxt = EVERY1 [ - - ]; val (_, lthy) = Local_Theory.begin_nested lthy; - val (tvsubst, lthy) = mk_def_t false Binding.empty I (Binding.name_of b) (length ps) + val (tvsubsts, lthy) = @{fold_map 3} (fn res => fn model => fn quotient => + mk_def_t false Binding.empty I (Binding.name_of (#binding model)) (length ps) (fold_rev Term.absfree (map dest_Free ps) (Term.abs ("t", #T quotient) ( - #rec_fun rec_res $ Bound 0 $ HOLogic.mk_tuple ps) - )) lthy; + #rec_fun res $ Bound 0 $ HOLogic.mk_tuple ps) + )) + ) rec_ress models (#quotient_fps fp_res) lthy; val (lthy, old_lthy) = `Local_Theory.end_nested lthy; val phi = Proof_Context.export_morphism old_lthy lthy; - val tvsubst = + val tvsubsts = let - val tvsubst_new = Morphism.term phi (fst tvsubst); + val tvsubst_new = Morphism.term phi (fst (hd tvsubsts)); val tyenv = Sign.typ_match (Proof_Context.theory_of lthy) - (fastype_of tvsubst_new, fastype_of (fst tvsubst)) Vartab.empty - in (Envir.subst_term (tyenv, Vartab.empty) tvsubst_new, Morphism.thm phi (snd tvsubst)) end - - val eta_naturals' = map (Option.map (fn eta => Local_Defs.unfold0 lthy @{thms comp_def} ( - fun_cong OF [#eta_natural (snd eta)] - ))) (#etas model); - - val var_types = MRBNF_Def.var_types_of_mrbnf mrbnf; - - val free = MRBNF_Def.free_of_mrbnf mrbnf; - val bound = MRBNF_Def.bound_of_mrbnf mrbnf; - val n = live + free + bound; - val eta_set_empties = map (Option.map (fn def => + (fastype_of tvsubst_new, fastype_of (fst (hd tvsubsts))) Vartab.empty + fun morph t = ( + Envir.subst_term (tyenv, Vartab.empty) (Morphism.term phi (fst t)), + Morphism.thm phi (snd t) + ) + in map morph tvsubsts end; + + val eta_naturalss' = map (fn model => + map (Option.map (fn eta => Local_Defs.unfold0 lthy @{thms comp_def} ( + fun_cong OF [#eta_natural (snd eta)] + ))) (#etas model) + ) models; + + val npassive = length plives + length pfrees + length pbounds; + val var_types = MRBNF_Def.var_types_of_mrbnf (hd mrbnfs); + val free = MRBNF_Def.free_of_mrbnf (hd mrbnfs); + val bound = MRBNF_Def.bound_of_mrbnf (hd mrbnfs); + val live = MRBNF_Def.live_of_mrbnf (hd mrbnfs); + val n = free + bound + live; + + val eta_set_emptiess = map2 (fn mrbnf => map (Option.map (fn def => let val args = (snd o dest_Type o snd o dest_funT o fastype_of o #eta) def; val (live_args, bound_args, free_args) = fold_rev ( @@ -1189,6 +1193,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ) (var_types ~~ args) ([], [], []); val sets = MRBNF_Def.mk_sets_of_mrbnf (replicate n (MRBNF_Def.deads_of_mrbnf mrbnf)) (replicate n live_args) (replicate n bound_args) (replicate n free_args) mrbnf; + val sets = take nvars sets @ drop (nvars + npassive) sets; + val var_types = replicate nvars MRBNF_Def.Free_Var @ replicate nvars MRBNF_Def.Bound_Var + @ replicate (foldr1 (op+) (#rec_vars fp_res)) MRBNF_Def.Live_Var; val sets' = filter (fn (var, set) => var <> MRBNF_Def.Free_Var orelse #aT def <> HOLogic.dest_setT (range_type (fastype_of set))) (var_types ~~ sets); val a = Free ("a", #aT def); @@ -1245,101 +1252,111 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = etac ctxt FalseE ]) end ) sets' end - )) defs; + ))) (#pre_mrbnfs fp_res) defss; - val FVars_VVrs = map2 (fn FVars => Option.map (fn _ => map_filter (Option.map (fn def => + val FVars_VVrss = map2 (fn quotient => map (Option.map (fn def => map (fn FVars => let val a = Free ("a", #aT def); val T = HOLogic.dest_setT (range_type (fastype_of FVars)); val set = if #aT def = T then mk_singleton a else Const (@{const_name bot}, HOLogic.mk_setT T) in Goal.prove_sorry lthy (names [a]) [] (mk_Trueprop_eq (FVars $ (fst (#VVr def) $ a), set)) (fn {context=ctxt,...} => unfold_thms_tac ctxt (@{thms comp_def UN_empty Diff_empty Un_empty_right Un_empty_left empty_Diff} - @ #FVars_ctors quotient @ map_filter (Option.map (snd o #VVr)) defs @ flat (map_filter I eta_set_empties) + @ #FVars_ctors quotient @ [snd (#VVr def)] @ flat (maps (map_filter I) eta_set_emptiess) ) THEN resolve_tac ctxt [refl, #eta_free (#axioms def)] 1 ) end - )) defs)) (#FVars quotient) defs; - - val free_sets = map_filter (fn (MRBNF_Def.Free_Var, s) => SOME s | _ => NONE) ( - var_types ~~ MRBNF_Def.mk_sets_of_mrbnf (replicate n (MRBNF_Def.deads_of_mrbnf mrbnf)) - (replicate n (replicate live (#T quotient))) (replicate n vars) (replicate n vars) mrbnf - ); - val f'_prems = map_filter I (map2 (fn h => Option.map (fn def => HOLogic.mk_Trueprop (#mk_SSupp_bound def (the h)))) hs defs); - val tvsubst_VVrs = @{map 7} (fn i => fn set => fn eta => fn f => fn set_empties => fn VVr_thms => Option.map (fn def => - let val a = Free ("a", #aT def); - in Goal.prove_sorry lthy (names (some_hs @ [a])) f'_prems ( - mk_Trueprop_eq (Term.list_comb (fst tvsubst, some_hs @ [fst (#VVr def) $ a]), the f $ a) - ) (fn {context=ctxt, prems} => EVERY1 [ - K (unfold_thms_tac ctxt [snd tvsubst, snd (#VVr def), @{thm comp_def}]), - rtac ctxt trans, - rtac ctxt (#rec_Uctor rec_res), - SELECT_GOAL (unfold_thms_tac ctxt (@{thms prod.case} @ [snd valid_P] @ map_filter I SSupp_VVr_empties)), - REPEAT_DETERM o resolve_tac ctxt (prems @ @{thms conjI cmin_greater card_of_Card_order emp_bound}), - K (unfold_thms_tac ctxt (@{thms prod.case Un_empty} @ the set_empties @ [snd (#noclash quotient), snd Uctor])), - REPEAT_DETERM o resolve_tac ctxt @{thms Int_empty_left conjI}, - REPEAT_DETERM o EVERY' [ - EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], - REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id} - ], - K (unfold_thms_tac ctxt (@{thms id_o o_id comp_def[of fst] fst_conv id_def[symmetric]} - @ [MRBNF_Def.map_id_of_mrbnf mrbnf] - )), - REPEAT_DETERM_N i o EVERY' [ + ) (#FVars quotient)))) (#quotient_fps fp_res) defss; + + val some_hs = flat some_hss; + val f'_prems = map2 (fn h => fn def => HOLogic.mk_Trueprop (#mk_SSupp_bound def h)) some_hs some_defs; + val setss = map (fn mrbnf => + MRBNF_Def.mk_sets_of_mrbnf (replicate n (MRBNF_Def.deads_of_mrbnf mrbnf)) + (replicate n (plives @ flat (map2 replicate (#rec_vars fp_res) (map #T (#quotient_fps fp_res))))) + (replicate n (pbounds @ vars)) (replicate n (vars @ pfrees)) mrbnf + ) mrbnfs; + val preTs = map (fn mrbnf => + MRBNF_Def.mk_T_of_mrbnf (MRBNF_Def.deads_of_mrbnf mrbnf) + (plives @ flat (map2 replicate (#rec_vars fp_res) (map #T (#quotient_fps fp_res)))) + (pbounds @ vars) (vars @ pfrees) mrbnf + ) mrbnfs; + + val tvsubst_VVrss = @{map 10} (fn mrbnf => fn model => fn rec_res => fn tvsubst => fn quotient => fn defs => fn hs => fn eta_set_empties => fn asVVr_VVrs => fn sets => + @{map 7} (fn i => fn set => fn eta => fn f => fn set_empties => fn asVVr_VVr => Option.map (fn def => + let val a = Free ("a", #aT def); + in Goal.prove_sorry lthy (names (some_hs @ [a])) f'_prems ( + mk_Trueprop_eq (Term.list_comb (fst tvsubst, some_hs @ [fst (#VVr def) $ a]), the f $ a) + ) (fn {context=ctxt, prems} => EVERY1 [ + K (unfold_thms_tac ctxt [snd tvsubst, snd (#VVr def), @{thm comp_def}]), rtac ctxt trans, - rtac ctxt @{thm if_not_P}, - SELECT_GOAL (unfold_thms_tac ctxt (@{thms comp_def} @ map (snd o #isVVr) some_defs @ map (snd o #VVr) some_defs @ [#inject quotient])), - rtac ctxt @{thm iffD2[OF not_ex]}, - rtac ctxt allI, - rtac ctxt @{thm notI}, - REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], - EqSubst.eqsubst_asm_tac ctxt [0] (map_filter I eta_naturals'), - REPEAT_DETERM o (resolve_tac ctxt @{thms supp_id_bound bij_id} ORELSE' assume_tac ctxt), - SELECT_GOAL (unfold_thms_tac ctxt @{thms id_def}), - dtac ctxt (mk_arg_cong lthy 1 set), - K (unfold_thms_tac ctxt (#eta_free (snd (the eta)) :: flat (map_filter I eta_set_empties))), - rotate_tac ~1, - etac ctxt @{thm contrapos_pp}, - rtac ctxt @{thm insert_not_empty} - ], - rtac ctxt trans, - rtac ctxt @{thm if_P}, - K (unfold_thms_tac ctxt [snd (#isVVr def), Local_Defs.unfold0 ctxt @{thms comp_def} ( - @{thm meta_eq_to_obj_eq} OF [snd (#VVr def)] RS fun_cong RS sym - ), #asVVr_VVr (the VVr_thms)]), - rtac ctxt exI, - rtac ctxt refl, - rtac ctxt refl - ]) end - )) (nvars - 1 downto 0) free_sets (#etas model) hs eta_set_empties VVr_thms defs; - - val preT = MRBNF_Def.mk_T_of_mrbnf (MRBNF_Def.deads_of_mrbnf mrbnf) - (replicate live (#T quotient)) vars vars mrbnf; - val x = Free ("x", preT); - val sets = MRBNF_Def.mk_sets_of_mrbnf (replicate n (MRBNF_Def.deads_of_mrbnf mrbnf)) - (replicate n (replicate live (#T quotient))) - (replicate n vars) (replicate n vars) mrbnf; - val tvsubst_not_isVVr = + rtac ctxt (#rec_Uctor rec_res), + SELECT_GOAL (unfold_thms_tac ctxt (@{thms prod.case} @ [snd valid_P] @ maps (map_filter I) SSupp_VVr_emptiess)), + REPEAT_DETERM o resolve_tac ctxt (prems @ @{thms conjI cmin_greater card_of_Card_order emp_bound}), + K (unfold_thms_tac ctxt (@{thms prod.case Un_empty} @ the set_empties @ map snd Uctors @ [snd (#noclash quotient)])), + REPEAT_DETERM o resolve_tac ctxt @{thms Int_empty_left conjI}, + REPEAT_DETERM o EVERY' [ + EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], + REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id} + ], + K (unfold_thms_tac ctxt (@{thms id_o o_id comp_def[of fst] fst_conv id_def[symmetric]} + @ [MRBNF_Def.map_id_of_mrbnf mrbnf] + )), + REPEAT_DETERM_N i o EVERY' [ + rtac ctxt trans, + rtac ctxt @{thm if_not_P}, + SELECT_GOAL (unfold_thms_tac ctxt (@{thms comp_def} @ map (snd o #isVVr) some_defs @ map (snd o #VVr) some_defs @ [#inject quotient])), + rtac ctxt @{thm iffD2[OF not_ex]}, + rtac ctxt allI, + rtac ctxt @{thm notI}, + REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], + EqSubst.eqsubst_asm_tac ctxt [0] (maps (map_filter I) eta_naturalss'), + REPEAT_DETERM o (resolve_tac ctxt @{thms supp_id_bound bij_id} ORELSE' assume_tac ctxt), + SELECT_GOAL (unfold_thms_tac ctxt @{thms id_def}), + dtac ctxt (mk_arg_cong lthy 1 set), + K (unfold_thms_tac ctxt (#eta_free (snd (the eta)) :: flat (maps (map_filter I) eta_set_emptiess))), + rotate_tac ~1, + etac ctxt @{thm contrapos_pp}, + rtac ctxt @{thm insert_not_empty} + ], + rtac ctxt trans, + rtac ctxt @{thm if_P}, + K (unfold_thms_tac ctxt [snd (#isVVr def), Local_Defs.unfold0 ctxt @{thms comp_def} ( + @{thm meta_eq_to_obj_eq} OF [snd (#VVr def)] RS fun_cong RS sym + ), the asVVr_VVr]), + rtac ctxt exI, + rtac ctxt refl, + rtac ctxt refl + ]) end + )) (0 upto nvars - 1) (take nvars sets) (#etas model) hs eta_set_empties asVVr_VVrs defs + ) mrbnfs models rec_ress tvsubsts (#quotient_fps fp_res) defss hss eta_set_emptiess asVVr_VVrss setss; + + val tvsubst_not_isVVrs = @{map 6} (fn i => fn mrbnf => fn quotient => fn rec_res => fn sets => fn preT => let - val bound_sets = map_filter (fn (MRBNF_Def.Bound_Var, x) => SOME x | _ => NONE) (var_types ~~ sets); + val x = Free ("x", preT); + val bound_sets = drop (length pbounds) ( + map_filter (fn (MRBNF_Def.Bound_Var, x) => SOME x | _ => NONE) (var_types ~~ sets) + ); val int_empty_prems = map2 (fn bset => fn i => HOLogic.mk_Trueprop ( - mk_int_empty (bset $ x, foldl1 mk_Un (map_filter I (map2 (fn f => Option.map (fn def => - fst (nth (#IImsupps def) i) $ the f - )) hs defs))) + mk_int_empty (bset $ x, foldl1 mk_Un (map2 (fn f => fn def => + fst (nth (#IImsupps def) i) $ f + ) some_hs some_defs)) )) bound_sets (0 upto nvars - 1); - val VVr_prems = map (fn def => HOLogic.mk_Trueprop (HOLogic.mk_not (fst (#isVVr def) $ (#ctor quotient $ x)))) some_defs; + val VVr_prems = map (fn def => + HOLogic.mk_Trueprop (HOLogic.mk_not (fst (#isVVr def) $ (#ctor quotient $ x))) + ) (nth some_defss i); val prems = f'_prems @ int_empty_prems @ [HOLogic.mk_Trueprop (fst (#noclash quotient) $ x)] @ VVr_prems; - val tvsubst_t = Term.list_comb (fst tvsubst, some_hs); - val ids = map HOLogic.id_const vars; + val tvsubst_ts = map (fn tvsubst => Term.list_comb (fst tvsubst, some_hs)) tvsubsts; + val ids = map HOLogic.id_const; val map_t = MRBNF_Def.mk_map_comb_of_mrbnf (MRBNF_Def.deads_of_mrbnf mrbnf) - (replicate live tvsubst_t) ids ids mrbnf; - val goal = mk_Trueprop_eq (tvsubst_t $ (#ctor quotient $ x), #ctor quotient $ (map_t $ x)); + (ids plives @ flat (map2 replicate (#rec_vars fp_res) tvsubst_ts)) + (ids (pbounds @ vars)) (ids (vars @ pfrees)) mrbnf; + val goal = mk_Trueprop_eq (nth tvsubst_ts i $ (#ctor quotient $ x), #ctor quotient $ (map_t $ x)); in Goal.prove_sorry lthy (names (some_hs @ [x])) prems goal (fn {context=ctxt, prems} => EVERY1 [ - K (unfold_thms_tac ctxt [snd tvsubst]), + K (unfold_thms_tac ctxt (map snd tvsubsts)), rtac ctxt trans, rtac ctxt (#rec_Uctor rec_res), SELECT_GOAL (unfold_thms_tac ctxt (@{thms prod.case} @ [snd valid_P])), - K (unfold_thms_tac ctxt @{thms Un_empty_right}), REPEAT_DETERM o resolve_tac ctxt (conjI :: prems), - K (unfold_thms_tac ctxt (@{thms prod.case} @ [snd Uctor])), + K (unfold_thms_tac ctxt (@{thms prod.case Un_empty_right} @ map snd Uctors @ map snd PFVarss)), + REPEAT_DETERM o resolve_tac ctxt prems, REPEAT_DETERM o EVERY' [ EqSubst.eqsubst_tac ctxt [0] [MRBNF_Def.map_comp_of_mrbnf mrbnf], REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id} @@ -1358,13 +1375,17 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = REPEAT_DETERM o resolve_tac ctxt (conjI :: prems) ], rtac ctxt refl - ]) end; + ]) end + ) (0 upto length models - 1) (#pre_mrbnfs fp_res) (#quotient_fps fp_res) rec_ress setss preTs; - val not_isVVr_frees = map2 (fn fset => Option.map (fn def => - let val goal = Logic.mk_implies ( - HOLogic.mk_Trueprop (HOLogic.mk_not (fst (#isVVr def) $ (#ctor quotient $ x))), - mk_Trueprop_eq (fset $ x, mk_bot (#aT def)) - ) in Goal.prove_sorry lthy (names [x]) [] goal (fn {context=ctxt, ...} => EVERY1 [ + val not_isVVr_freess = @{map 4} (fn sets => fn quotient => fn preT => map2 (fn fset => Option.map (fn def => + let + val x = Free ("x", preT); + val goal = Logic.mk_implies ( + HOLogic.mk_Trueprop (HOLogic.mk_not (fst (#isVVr def) $ (#ctor quotient $ x))), + mk_Trueprop_eq (fset $ x, mk_bot (#aT def)) + ) + in Goal.prove_sorry lthy (names [x]) [] goal (fn {context=ctxt, ...} => EVERY1 [ rtac ctxt (#eta_compl_free (#axioms def)), K (unfold_thms_tac ctxt (@{thms image_iff Set.bex_simps not_ex comp_def} @ [snd (#isVVr def), snd (#VVr def)])), rtac ctxt allI, @@ -1373,9 +1394,9 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = hyp_subst_tac ctxt, rtac ctxt refl ]) end - )) (map_filter (fn (MRBNF_Def.Free_Var, x) => SOME x | _ => NONE) (var_types ~~ sets)) defs; + )) (take nvars sets)) setss (#quotient_fps fp_res) preTs defss; - val in_IImsuppss = map (Option.map (fn def => map2 (fn FVars => fn IImsupp => + val in_IImsuppsss = map2 (fn quotient => map (Option.map (fn def => map2 (fn FVars => fn IImsupp => let val a = Free ("a", #aT def); val z = Free ("z", HOLogic.dest_setT (range_type (fastype_of FVars))); @@ -1398,61 +1419,63 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = rtac ctxt CollectI, assume_tac ctxt ]) end - ) (#FVars quotient) (#IImsupps def))) defs; + ) (#FVars quotient) (#IImsupps def)))) (#quotient_fps fp_res) defss; - val IImsupp_Diffs = @{map 5} (fn FVars => fn f => fn i => fn in_IImsupps => Option.map (fn def => - let - val a = Free ("a", #aT def); - val A = Free ("A", HOLogic.mk_setT (#aT def)); - val B = Free ("B", HOLogic.mk_setT (#aT def)); - val inner = Term.absfree (dest_Free a) (FVars $ (the f $ a)) - val goal = Logic.mk_implies ( - HOLogic.mk_Trueprop (mk_int_empty (B, fst (nth (#IImsupps def) i) $ the f)), - mk_Trueprop_eq ( - mk_UNION (HOLogic.mk_binop @{const_name minus} (A, B)) inner, - HOLogic.mk_binop @{const_name minus} (mk_UNION A inner, B) - ) - ); - in Goal.prove_sorry lthy (names [the f, A, B]) [] goal (fn {context=ctxt, ...} => EVERY1 [ - rtac ctxt @{thm iffD2[OF set_eq_iff]}, - rtac ctxt allI, - rtac ctxt iffI, - let fun helper_tac inv = EVERY' [ - REPEAT_DETERM o eresolve_tac ctxt @{thms UN_E DiffE}, - REPEAT_DETERM o resolve_tac ctxt @{thms DiffI UN_I}, - assume_tac ctxt, - if not inv then assume_tac ctxt else K all_tac, - rtac ctxt @{thm case_split[of "_ = _"]}, - if inv then rotate_tac ~2 else K all_tac, - dtac ctxt @{thm iffD1[OF arg_cong2[OF refl, of _ _ "(\)"], rotated]}, - rtac ctxt trans, - rtac ctxt (mk_arg_cong lthy 1 FVars), - assume_tac ctxt, - resolve_tac ctxt (flat (map_filter I FVars_VVrs)), - dtac ctxt @{thm singletonD}, - rtac ctxt @{thm iffD2[OF arg_cong2[OF _ refl, of _ _ "(\)"]]}, - if inv then rtac ctxt sym else K all_tac, - assume_tac ctxt, - assume_tac ctxt, - forward_tac ctxt (the in_IImsupps), + val IImsupp_Diffss = @{map 4} (fn quotient => fn in_IImsuppss => fn hs => + @{map 5} (fn FVars => fn f => fn i => fn in_IImsupps => Option.map (fn def => + let + val a = Free ("a", #aT def); + val A = Free ("A", HOLogic.mk_setT (#aT def)); + val B = Free ("B", HOLogic.mk_setT (#aT def)); + val inner = Term.absfree (dest_Free a) (FVars $ (the f $ a)) + val goal = Logic.mk_implies ( + HOLogic.mk_Trueprop (mk_int_empty (B, fst (nth (#IImsupps def) i) $ the f)), + mk_Trueprop_eq ( + mk_UNION (HOLogic.mk_binop @{const_name minus} (A, B)) inner, + HOLogic.mk_binop @{const_name minus} (mk_UNION A inner, B) + ) + ); + in Goal.prove_sorry lthy (names [the f, A, B]) [] goal (fn {context=ctxt, ...} => EVERY1 [ + rtac ctxt @{thm iffD2[OF set_eq_iff]}, + rtac ctxt allI, + rtac ctxt iffI, + let fun helper_tac inv = EVERY' [ + REPEAT_DETERM o eresolve_tac ctxt @{thms UN_E DiffE}, + REPEAT_DETERM o resolve_tac ctxt @{thms DiffI UN_I}, + assume_tac ctxt, + if not inv then assume_tac ctxt else K all_tac, + rtac ctxt @{thm case_split[of "_ = _"]}, + if inv then rotate_tac ~2 else K all_tac, + dtac ctxt @{thm iffD1[OF arg_cong2[OF refl, of _ _ "(\)"], rotated]}, + rtac ctxt trans, + rtac ctxt (mk_arg_cong lthy 1 FVars), + assume_tac ctxt, + resolve_tac ctxt (flat (maps (map_filter I) FVars_VVrss)), + dtac ctxt @{thm singletonD}, + rtac ctxt @{thm iffD2[OF arg_cong2[OF _ refl, of _ _ "(\)"]]}, + if inv then rtac ctxt sym else K all_tac, + assume_tac ctxt, + assume_tac ctxt, + forward_tac ctxt (the in_IImsupps), + assume_tac ctxt, + dtac ctxt @{thm trans[OF Int_commute]}, + dtac ctxt @{thm iffD1[OF disjoint_iff]}, + etac ctxt allE, + etac ctxt impE, + if inv then K (prefer_tac 2) else assume_tac ctxt, + assume_tac ctxt + ] in EVERY' [ + helper_tac false, + helper_tac true + ] end, + REPEAT_DETERM o EqSubst.eqsubst_tac ctxt [0] (snd (#SSupp def) :: map snd (#IImsupps def)), + rtac ctxt UnI1, + rtac ctxt @{thm iffD2[OF mem_Collect_eq]}, assume_tac ctxt, - dtac ctxt @{thm trans[OF Int_commute]}, - dtac ctxt @{thm iffD1[OF disjoint_iff]}, - etac ctxt allE, - etac ctxt impE, - if inv then K (prefer_tac 2) else assume_tac ctxt, assume_tac ctxt - ] in EVERY' [ - helper_tac false, - helper_tac true - ] end, - REPEAT_DETERM o EqSubst.eqsubst_tac ctxt [0] (snd (#SSupp def) :: map snd (#IImsupps def)), - rtac ctxt UnI1, - rtac ctxt @{thm iffD2[OF mem_Collect_eq]}, - assume_tac ctxt, - assume_tac ctxt - ]) end - )) (#FVars quotient) hs (0 upto nvars - 1) in_IImsuppss defs; + ]) end + )) (#FVars quotient) hs (0 upto nvars - 1) in_IImsuppss + ) (#quotient_fps fp_res) in_IImsuppsss hss defss; (*val FFVars_tvsubsts = @{map 8} (fn FVars => fn i => fn f => fn tvsubst_VVr => fn FVars_VVr => fn not_isVVr_free => fn IImsupp_Diff => Option.map (fn def => let @@ -1541,10 +1564,11 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = ]) end )) (#FVars quotient) (0 upto nvars - 1) fs' tvsubst_VVrs FVars_VVrs not_isVVr_frees IImsupp_Diffs defs;*) - val VVrs' = map_filter (Option.map ((fn (VVr, VVr_def) => (VVr, @{thm eq_reflection} OF [mk_unabs_def 1 ( + val VVrss' = map (map_filter (Option.map ((fn (VVr, VVr_def) => (VVr, @{thm eq_reflection} OF [mk_unabs_def 1 ( @{thm meta_eq_to_obj_eq} OF [Local_Defs.unfold0 lthy (@{thms comp_def} @ eta_defs) VVr_def] - )])) o #VVr)) defs; - val result = { + )])) o #VVr))) defss; + + val results = @{map 5} (fn tvsubst => fn defs => fn tvsubst_VVrs => fn tvsubst_not_isVVr => fn VVrs' => { tvsubst = fst tvsubst, SSupps = map_filter (Option.map (fst o #SSupp)) defs, IImsuppss = map_filter (Option.map (map fst o #IImsupps)) defs, @@ -1552,26 +1576,26 @@ fun create_tvsubst_of_mrbnf qualify fp_res models lthy = isVVrs = map_filter (Option.map (snd o #isVVr)) defs, tvsubst_VVrs = map_filter I tvsubst_VVrs, tvsubst_cctor_not_isVVr = tvsubst_not_isVVr - }: tvsubst_result; + }: tvsubst_result) tvsubsts defss tvsubst_VVrss tvsubst_not_isVVrs VVrss'; (* TODO: Remove *) val notes = - [("SSupp_VVr_empty", map_filter I SSupp_VVr_empties), - ("SSupp_VVr_bound", map_filter I SSupp_VVr_bounds), - ("in_IImsupp", flat (map_filter I in_IImsuppss)), - ("eta_set_empties", flat (map_filter I eta_set_empties)), - ("FVars_VVr", flat (map_filter I FVars_VVrs)), - ("tvsubst_VVr", map_filter I tvsubst_VVrs), - ("tvsubst_cctor_not_isVVr", [tvsubst_not_isVVr]), - ("not_isVVr_free", map_filter I not_isVVr_frees), - ("IImsupp_Diff", map_filter I IImsupp_Diffs) + [("SSupp_VVr_empty", maps (map_filter I) SSupp_VVr_emptiess), + ("SSupp_VVr_bound", maps (map_filter I) SSupp_VVr_boundss), + ("in_IImsupp", flat (maps (map_filter I) in_IImsuppsss)), + ("eta_set_empties", flat (maps (map_filter I) eta_set_emptiess)), + ("FVars_VVr", flat (maps (map_filter I) FVars_VVrss)), + ("tvsubst_VVr", maps (map_filter I) tvsubst_VVrss), + ("tvsubst_cctor_not_isVVr", tvsubst_not_isVVrs), + ("not_isVVr_free", maps (map_filter I) not_isVVr_freess), + ("IImsupp_Diff", maps (map_filter I) IImsupp_Diffss) (*("FFVars_tvsubst", map_filter I FFVars_tvsubsts)*) ] |> (map (fn (thmN, thms) => - ((Binding.qualify true (short_type_name (fst (dest_Type (#T quotient)))) (Binding.name thmN), []), [(thms, [])]) + ((Binding.qualify true (short_type_name (fst (dest_Type (#T (hd (#quotient_fps fp_res)))))) + (Binding.name thmN), []), [(thms, [])]) )); val (_, lthy) = Local_Theory.notes notes lthy - in (result, lthy) end;*) - in error "end" end + in (results, lthy) end; end \ No newline at end of file diff --git a/operations/Sugar.thy b/operations/Sugar.thy index fb9068eb..8138568c 100644 --- a/operations/Sugar.thy +++ b/operations/Sugar.thy @@ -637,14 +637,12 @@ val T2_model = { \ ML_file \../Tools/mrbnf_tvsubst.ML\ - -ML \ -Multithreading.parallel_proofs := 0 -\ -declare [[ML_print_depth=100000]] + local_setup \fn lthy => let val (res', lthy) = MRBNF_TVSubst.create_tvsubst_of_mrbnf I res [T1_model, T2_model] lthy + val _ = @{print} res' in lthy end\ +print_theorems end \ No newline at end of file From d990448a2dce638e72fad09f27b1faa9e7bb5187 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Wed, 27 Mar 2024 16:03:25 +0000 Subject: [PATCH 6/7] Fix POPLmark theory --- thys/POPLmark/SystemFSub.thy | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy index b30cde69..dc749487 100644 --- a/thys/POPLmark/SystemFSub.thy +++ b/thys/POPLmark/SystemFSub.thy @@ -329,18 +329,6 @@ lemma G_equiv: "ssbij \ \ small B \ G B R typ.rrename_comps typ.FFVars_rrenames wf_eqvt extend_eqvt | ((rule exI[of _ "\ _"] exI)+, (rule conjI)?, rule refl) | ((rule exI[of _ "rrename_typ \ _"])+, (rule conjI)?, rule in_context_eqvt))+ - apply (metis (no_types, lifting) UN_subset_iff image_eqI snd_conv subsetD) - using image_iff apply fastforce - apply (auto simp: case_prod_map_prod) - subgoal for \ xs ys b l - apply (drule bspec) - apply assumption - apply (erule case_prodE) - apply (erule bexE) - apply (unfold case_prod_beta) - apply (erule conjE) - by (metis (no_types, opaque_lifting) fst_eqD inv_simp1 snd_eqD typ.rrename_bijs typ.rrename_inv_simps) - done lemma fresh: "\xx. xx \ Tfvars t" by (metis emp_bound equals0D imageI inf.commute inf_absorb2 small_Tfvars small_def small_ssbij subsetI) From 38628ff384382ba66eab75f9acc8245dd3381551 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Wed, 27 Mar 2024 16:22:33 +0000 Subject: [PATCH 7/7] Add tvsubst suffix to IImsupp again --- Tools/mrbnf_tvsubst.ML | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Tools/mrbnf_tvsubst.ML b/Tools/mrbnf_tvsubst.ML index ddd319a6..56772c44 100644 --- a/Tools/mrbnf_tvsubst.ML +++ b/Tools/mrbnf_tvsubst.ML @@ -239,13 +239,13 @@ fun define_tvsubst_consts qualify fp_res (vars, pfrees, plives, pbounds) (models ))) )) lthy; - val (IImsupps, lthy) = @{fold_map 2} (fn FVars => fn s => mk_def_public ("IImsupp" ^ the suffix ^ "_" ^ s) 1 ( - Term.absfree (dest_Free h) ( + val (IImsupps, lthy) = @{fold_map 2} (fn FVars => fn s => + mk_def_public ("IImsupp" ^ the suffix ^ s ^ "_" ^ Binding.name_of (#binding model)) 1 (Term.absfree (dest_Free h) ( let val UN = mk_UNION (fst SSupp $ h) (HOLogic.mk_comp (FVars, h)); in if fastype_of (fst SSupp $ h) = range_type (fastype_of FVars) then mk_Un (fst SSupp $ h, UN) else UN end - ))) (#FVars quot) (if nvars = 1 then [""] else map string_of_int (1 upto nvars)) lthy; + ))) (#FVars quot) (if nvars = 1 then [""] else map (fn i => "_" ^ string_of_int i) (1 upto nvars)) lthy; val (isVVr, lthy) = mk_def_t ("isVVr" ^ the suffix) 1 (Term.absfree (dest_Free t) ( HOLogic.mk_exists ("a", aT, HOLogic.mk_eq (t, fst VVr $ Bound 0))