Add operations theory for least fixpoint

jvanbruegge · Aug 8, 2024 · eb2ab48 · eb2ab48
1 parent b2b3b5b
commit eb2ab48
Show file tree

Hide file tree

Showing 5 changed files with 5,700 additions and 35 deletions.
diff --git a/Tools/mrbnf_fp.ML b/Tools/mrbnf_fp.ML
@@ -517,18 +517,6 @@ fun construct_binder_fp fp mrbnf_ks binding_relation lthy =
     );
     val rename_comp0s = mk_rename_comp0s lthy rename_comps renamesAs;
 
-    fun mk_rename_bij lthy rename_t rename_comp0 rename_id0 =
-      let val goal = HOLogic.mk_Trueprop (mk_bij (Term.list_comb (rename_t, ffs)));
-      in prove lthy ffs prem_terms_ffs goal (mk_rename_bij_tac rename_comp0 rename_id0) end;
-    val rename_bijs = @{map 3} (mk_rename_bij lthy) renamesAs rename_comp0s rename_id0s;
-
-    fun mk_rename_inv_simp lthy rename_t rename_comp0 rename_id0 =
-      let val goal = mk_Trueprop_eq (
-        mk_inv (Term.list_comb (rename_t, ffs)),
-        Term.list_comb (rename_t, map mk_inv ffs)
-      ) in prove lthy ffs prem_terms_ffs goal (mk_rename_inv_simp_tac rename_comp0 rename_id0) end;
-    val rename_inv_simps = @{map 3} (mk_rename_inv_simp lthy) renamesAs rename_comp0s rename_id0s;
-
     (* Define inductive predicate free *)
     fun mk_inductive i A z b_vec free_sets bound_sets lthy =
       let
@@ -2336,6 +2324,16 @@ fun construct_binder_fp fp mrbnf_ks binding_relation lthy =
       (transpose FFVars_defss) rrename_defs Quotient_abs_reps Quotient_total_abs_eq_iffs alpha_bijs
       rename_ids alpha_refls;
 
+    fun mk_rename_bij lthy rename_t rename_comp0 rename_id0 =
+      let val goal = HOLogic.mk_Trueprop (mk_bij (Term.list_comb (rename_t, ffs)));
+      in prove lthy ffs prem_terms_ffs goal (mk_rename_bij_tac rename_comp0 rename_id0) end;
+
+    fun mk_rename_inv_simp lthy rename_t rename_comp0 rename_id0 =
+      let val goal = mk_Trueprop_eq (
+        mk_inv (Term.list_comb (rename_t, ffs)),
+        Term.list_comb (rename_t, map mk_inv ffs)
+      ) in prove lthy ffs prem_terms_ffs goal (mk_rename_inv_simp_tac rename_comp0 rename_id0) end;
+
     val rrename_bijs = @{map 3} (mk_rename_bij lthy) rrenamesAs rrename_comp0s rrename_id0s;
     val rrename_inv_simps = @{map 3} (mk_rename_inv_simp lthy) rrenamesAs rrename_comp0s rrename_id0s;
 
@@ -2379,8 +2377,6 @@ fun construct_binder_fp fp mrbnf_ks binding_relation lthy =
           rename_id = nth rename_ids i,
           rename_comp0 = nth rename_comp0s i,
           rename_comp = nth rename_comps i,
-          rename_bij = nth rename_bijs i,
-          rename_inv_simp = nth rename_inv_simps i,
           FVars_ctors = nth (transpose FVars_ctorss) i,
           FVars_renames = nth (transpose FVars_renamess) i,
           FVars_intross = FVars_intross,
@@ -2421,8 +2417,6 @@ fun construct_binder_fp fp mrbnf_ks binding_relation lthy =
           rename_id = nth rrename_ids i,
           rename_comp0 = nth rrename_comp0s i,
           rename_comp = nth rrename_comps i,
-          rename_bij = nth rrename_bijs i,
-          rename_inv_simp = nth rrename_inv_simps i,
           FVars_ctors = nth (transpose FFVars_cctorss) i,
           FVars_renames = nth (transpose FFVars_rrenamess) i,
           FVars_intross = FFVars_intross,
@@ -2445,6 +2439,8 @@ fun construct_binder_fp fp mrbnf_ks binding_relation lthy =
 
             rename_ctor = nth rrename_cctors i,
             rename_cong_id = nth rrename_cong_ids i,
+            rename_bij = nth rrename_bijs i,
+            rename_inv_simp = nth rrename_inv_simps i,
             fresh_co_induct_param = TT_fresh_co_induct_param,
             fresh_co_induct = TT_fresh_co_induct,
             fresh_induct_param_no_clash = TT_fresh_induct_param_no_clash_opt
@@ -2470,8 +2466,6 @@ fun construct_binder_fp fp mrbnf_ks binding_relation lthy =
        ("rename_ids", rename_ids),
        ("rename_comp0s", rename_comp0s),
        ("rename_comps", rename_comps),
-       ("rename_bijs", rename_bijs),
-       ("rename_inv_simps", rename_inv_simps),
        ("FVars_ctors", flat FVars_ctorss),
        ("FVars_rename_less", flat FVars_rename_less),
        ("FVars_renames", flat FVars_renamess),

diff --git a/Tools/mrbnf_fp_def_sugar.ML b/Tools/mrbnf_fp_def_sugar.ML
@@ -13,8 +13,6 @@ sig
     rename_id: thm,
     rename_comp0: thm,
     rename_comp: thm,
-    rename_bij: thm,
-    rename_inv_simp: thm,
     FVars_ctors: thm list,
     FVars_renames: thm list,
     FVars_intross: thm list list,
@@ -62,6 +60,8 @@ sig
 
     rename_ctor: thm,
     rename_cong_id: thm,
+    rename_bij: thm,
+    rename_inv_simp: thm,
     fresh_co_induct_param: thm,
     fresh_co_induct: thm,
     fresh_induct_param_no_clash: thm option
@@ -104,8 +104,6 @@ type 'a fp_result_T = {
   rename_id: thm,
   rename_comp0: thm,
   rename_comp: thm,
-  rename_bij: thm,
-  rename_inv_simp: thm,
   FVars_ctors: thm list,
   FVars_renames: thm list,
   FVars_intross: thm list list,
@@ -114,7 +112,7 @@ type 'a fp_result_T = {
 };
 
 fun morph_fp_result_T morph phi { T, ctor, rename, FVars, inner, inject, rename_id0, rename_id,
-  rename_comp0, rename_comp, rename_bij, rename_inv_simp, FVars_ctors, FVars_renames, card_of_FVars_bounds,
+  rename_comp0, rename_comp, FVars_ctors, FVars_renames, card_of_FVars_bounds,
   card_of_FVars_bound_UNIVs, FVars_intross, noclash } = {
   T = Morphism.typ phi T,
   ctor = Morphism.term phi ctor,
@@ -127,8 +125,6 @@ fun morph_fp_result_T morph phi { T, ctor, rename, FVars, inner, inject, rename_
   rename_id = Morphism.thm phi rename_id,
   rename_comp0 = Morphism.thm phi rename_comp0,
   rename_comp = Morphism.thm phi rename_comp,
-  rename_bij = Morphism.thm phi rename_bij,
-  rename_inv_simp = Morphism.thm phi rename_inv_simp,
   FVars_ctors = map (Morphism.thm phi) FVars_ctors,
   FVars_renames = map (Morphism.thm phi) FVars_renames,
   FVars_intross = map (map (Morphism.thm phi)) FVars_intross,
@@ -198,13 +194,15 @@ type quotient_result = {
 
   rename_ctor: thm,
   rename_cong_id: thm,
+  rename_bij: thm,
+  rename_inv_simp: thm,
   fresh_co_induct_param: thm,
   fresh_co_induct: thm,
   fresh_induct_param_no_clash: thm option
 };
 
 fun morph_quotient_result phi { abs, rep, alpha_quotient_sym, total_abs_eq_iff, abs_rep, rep_abs,
-abs_ctor, rename_def, FVars_defs, ctor_def, rename_ctor, fresh_co_induct, rename_cong_id,
+abs_ctor, rename_def, FVars_defs, ctor_def, rename_ctor, fresh_co_induct, rename_cong_id, rename_bij, rename_inv_simp,
 fresh_co_induct_param, nnoclash_noclash, fresh_induct_param_no_clash } = {
   abs = Morphism.term phi abs,
   rep = Morphism.term phi rep,
@@ -219,6 +217,8 @@ fresh_co_induct_param, nnoclash_noclash, fresh_induct_param_no_clash } = {
   abs_ctor = Morphism.thm phi abs_ctor,
   rename_ctor = Morphism.thm phi rename_ctor,
   rename_cong_id = Morphism.thm phi rename_cong_id,
+  rename_bij = Morphism.thm phi rename_bij,
+  rename_inv_simp = Morphism.thm phi rename_inv_simp,
   fresh_co_induct_param = Morphism.thm phi fresh_co_induct_param,
   fresh_co_induct = Morphism.thm phi fresh_co_induct,
   fresh_induct_param_no_clash = Option.map (Morphism.thm phi) fresh_induct_param_no_clash

diff --git a/operations/Fixpoint.thy → operations/Composition.thy b/operations/Fixpoint.thy → operations/Composition.thy
@@ -1,7 +1,9 @@
-theory Fixpoint
-  imports "Binders.MRBNF_FP"
+theory Composition
+  imports "Binders.MRBNF_Composition"
 begin
 
+declare [[mrbnf_internals]]
+
 (* TODO: Show proofs as apply script *)
 ML \<open>
 val ctor_T1_Ts = [
@@ -78,19 +80,13 @@ let
   val (bnf1, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf1 lthy
   val (bnf2, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf2 lthy
   val _ = @{print} "register"
-
-  (* Step 4: Create fixpoint of pre-MRBNF *)
-  val (res, lthy) = MRBNF_FP.construct_binder_fp MRBNF_Util.Least_FP [
-    ((name1, mrbnf1), 2), ((name2, mrbnf2), 2)
-  ] rel lthy;
-  val _ = @{print} "fixpoint"
 in lthy end
 \<close>
 print_theorems
+print_bnfs
 
 declare [[quick_and_dirty=false]]
 
-thm noclash_T1_def
 lemmas infinite_UNIV = cinfinite_imp_infinite[OF T1_pre.UNIV_cinfinite]
 
 end