Revamp fixpoint code (#49)

jvanbruegge · Nov 26, 2024 · 1ebcefd · 1ebcefd
2 parents 2840f79 + 3c5ee89
commit 1ebcefd
Show file tree

Hide file tree

Showing 55 changed files with 19,255 additions and 9,489 deletions.
diff --git a/ROOT b/ROOT
@@ -41,7 +41,9 @@ session Binders in "thys" = Prelim +
 session Operations in "operations" = Untyped_Lambda_Calculus +
   theories
     Binder_Inductive
-    Fixpoint
+    Least_Fixpoint
+    Least_Fixpoint2
+    Greatest_Fixpoint
     Recursor
     VVSubst
     TVSubst

diff --git a/Tools/binder_induction.ML b/Tools/binder_induction.ML
@@ -78,7 +78,7 @@ fun extract_vars ctxt var t =
             | NONE => (case BNF_Def.bnf_of ctxt name of
               SOME bnf => BNF_Def.sets_of_bnf bnf
               | NONE => (case MRBNF_FP_Def_Sugar.fp_result_of ctxt name of
-                SOME sugar => #FVars (hd (filter (
+                SOME sugar => #FVarss (hd (filter (
                   fn quot => fst (dest_Type (#T quot)) = name
                 ) (#quotient_fps sugar)))
                 | NONE => []

diff --git a/Tools/binder_inductive.ML b/Tools/binder_inductive.ML
@@ -13,14 +13,9 @@ fun long_name ctxt name =
     Const (s, _) => s
   | _ => error ("Undeclared constant: " ^ quote name)
 
-datatype ('a, 'b) either = Inl of 'a | Inr of 'b
-
 fun collapse (Inl x) = x
   | collapse (Inr x) = x
 
-fun mk_insert x S =
-  Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S;
-
 fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
   let
     val binds = the_default [] binds_opt;
@@ -154,7 +149,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
         val mapx = case mr_bnf of
           Inl mrbnf => MRBNF_Def.map_of_mrbnf mrbnf
           | Inr (Inl bnf) => BNF_Def.map_of_bnf bnf
-          | Inr (Inr sugar) => #rename (hd (filter (fn quot =>
+          | Inr (Inr sugar) => #permute (hd (filter (fn quot =>
             fst (dest_Type (#T quot)) = name
           ) (#quotient_fps sugar)))
         val Ts = fst (split_last (Term.binder_types (fastype_of mapx)));
@@ -434,7 +429,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
 
         fun map_id0_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_id0_of_mrbnf mrbnf]
           | map_id0_of_mr_bnf (Inr (Inl bnf)) = [BNF_Def.map_id0_of_bnf bnf]
-          | map_id0_of_mr_bnf (Inr (Inr sugar)) = map #rename_id0 (#quotient_fps sugar)
+          | map_id0_of_mr_bnf (Inr (Inr sugar)) = map #permute_id0 (#quotient_fps sugar)
 
         fun prove_missing goals specified thms tac = fst (@{fold_map 4} (
           fn true => (fn _ => fn _ => fn _ => fn acc => (hd acc, tl acc))
@@ -446,7 +441,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
         fun map_comp_of_mr_bnf (Inl mrbnf) = [MRBNF_Def.map_comp_of_mrbnf mrbnf, MRBNF_Def.map_comp0_of_mrbnf mrbnf RS sym]
           | map_comp_of_mr_bnf (Inr (Inl bnf)) = [BNF_Def.map_comp_of_bnf bnf, BNF_Def.map_comp0_of_bnf bnf RS sym]
           | map_comp_of_mr_bnf (Inr (Inr sugar)) = maps (fn quot =>
-              [#rename_comp quot, #rename_comp0 quot]
+              [#permute_comp quot, #permute_comp0 quot]
             ) (#quotient_fps sugar)
 
         val perm_id0s = prove_missing perm_id0_goals perms_specified perm_id0s (fn ctxt => fn mr_bnfs => K (EVERY1 [
@@ -460,7 +455,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
 
         fun set_map_of_mr_bnf (Inl mrbnf) = MRBNF_Def.set_map_of_mrbnf mrbnf
           | set_map_of_mr_bnf (Inr (Inl bnf)) = BNF_Def.set_map_of_bnf bnf
-          | set_map_of_mr_bnf (Inr (Inr sugar)) = maps #FVars_renames (#quotient_fps sugar)
+          | set_map_of_mr_bnf (Inr (Inr sugar)) = maps #FVars_permutes (#quotient_fps sugar)
 
         val supp_seminats = prove_missing supp_seminat_goals one_specified supp_seminats (fn ctxt => fn mr_bnfs => K (EVERY1 [
           K (Local_Defs.unfold0_tac ctxt (
@@ -470,7 +465,7 @@ fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy =
           rtac ctxt @{thm subset_refl}
         ]));
 
-        fun map_cong_id_of_mr_bnf (Inr (Inr sugar)) = map (#rename_cong_id o #inner) (#quotient_fps sugar)
+        fun map_cong_id_of_mr_bnf (Inr (Inr sugar)) = map (#permute_cong_id o #inner) (#quotient_fps sugar)
           | map_cong_id_of_mr_bnf x =
             let
               val thm1 = case x of

diff --git a/Tools/mrbnf_def.ML b/Tools/mrbnf_def.ML
@@ -1307,9 +1307,12 @@ datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
 datatype fact_policy = Dont_Note | Note_Some | Note_All;
 
 val mrbnf_internals = Attrib.setup_config_bool @{binding mrbnf_internals} (K false);
+val mrbnf_notes = Attrib.setup_config_bool @{binding mrbnf_notes} (K true);
 val mrbnf_timing = Attrib.setup_config_bool @{binding mrbnf_timing} (K false);
 
-fun user_policy policy ctxt = if Config.get ctxt mrbnf_internals then Note_All else policy;
+fun user_policy policy ctxt = if Config.get ctxt mrbnf_notes then
+  (if Config.get ctxt mrbnf_internals then Note_All else policy)
+  else Dont_Note;
 
 val smart_max_inline_term_size = 25; (*FUDGE*)
 
@@ -2269,6 +2272,14 @@ fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term
             |> Thm.close_derivation \<^here>
           end;
 
+        val lthy = Local_Theory.background_theory (fn thy =>
+          let
+            val lthy = Named_Target.init [] (hd coclass) thy;
+            val lthy = snd (Local_Theory.notes (map (fn (thmN, thm) => ((Binding.name thmN, []), [([thm], [])])) [
+              ("large", covar_large)
+            ]) lthy) handle ERROR _ => lthy;
+          in Local_Theory.exit_global lthy end
+        ) lthy;
         val lthy = Local_Theory.background_theory (fn thy =>
           let
             val lthy = Named_Target.init [] (hd class) thy;