Do not seperate between own/other injections, use types instead

jvanbruegge · Dec 12, 2024 · 9310ad4 · 9310ad4
1 parent e4cccb3
commit 9310ad4
Show file tree

Hide file tree

Showing 4 changed files with 135 additions and 31 deletions.
diff --git a/Tools/bmv_monad_def.ML b/Tools/bmv_monad_def.ML
@@ -1,13 +1,16 @@
 signature BMV_MONAD_DEF = sig
   type bmv_monad
+  type supported_functor (* TODO *)
 
   type 'a bmv_monad_axioms = {
     Sb_Inj: 'a,
     Sb_comp_Injs: 'a list,
-    Sb_comp: 'a,
+    Sb_comp: 'a,  (* require typeclass on free vars to bound *)
     Sb_cong: 'a,
-    Vrs_Injs: 'a list,
+    (* TODO: Add Vrs_bd axiom *)
+    Vrs_Injs: 'a list, (* TODO: One per Inj AND var kind *)
     Vrs_Sbs: 'a list
+    (* Add optional Map_Sb axiom (dependent on iff Map exists) *)
   };
 
   type bmv_monad_model = {
@@ -16,7 +19,7 @@ signature BMV_MONAD_DEF = sig
     frees: typ list,
     lives: typ list,
     leader: int,
-    Injs: (term list * (term * int) list) list,
+    Injs: term list list,
     Sbs: term list,
     Maps: term option list,
     Vrs: term list list,
@@ -36,6 +39,8 @@ signature BMV_MONAD_DEF = sig
 
   val bmv_monad_def: BNF_Def.inline_policy -> (Proof.context -> BNF_Def.fact_policy)
     -> (binding -> binding) -> bmv_monad_model -> local_theory -> bmv_monad
+
+  val compose_bmv_monad: (binding -> binding) -> bmv_monad -> bmv_monad list -> local_theory -> bmv_monad
 end
 
 structure BMV_Monad_Def : BMV_MONAD_DEF = struct
@@ -62,6 +67,7 @@ fun morph_bmv_axioms phi {
   Vrs_Sbs = map (Morphism.thm phi) Vrs_Sbs
 } : thm bmv_monad_axioms
 
+(* TODO: Add bound *)
 datatype bmv_monad = BMV of {
   ops: typ list,
   leader: int,
@@ -70,10 +76,12 @@ datatype bmv_monad = BMV of {
   Injs: term list list,
   Sbs: term list,
   Maps: term option list,
-  Vrs: term list list,
+  Vrs: term list list (*list*), (* TODO: Need Vr operator per Injection *)
   axioms: thm bmv_monad_axioms list
 }
 
+datatype supported_functor = Supported_Functor (* TODO *)
+
 fun Rep_bmv (BMV x) = x
 
 val ops_of_bmv_monad = #ops o Rep_bmv
@@ -91,7 +99,7 @@ type bmv_monad_model = {
   lives: typ list,
   bmv_ops: bmv_monad list,
   leader: int,
-  Injs: (term list * (term * int) list) list,
+  Injs: term list list,
   Sbs: term list,
   Maps: term option list,
   Vrs: term list list,
@@ -116,13 +124,13 @@ fun prove_axioms (model: bmv_monad_model) lthy =
   let
     val Ts = #ops model @ maps ops_of_bmv_monad (#bmv_ops model);
     val Sbs = #Sbs model @ maps Sbs_of_bmv_monad (#bmv_ops model);
-    val Injss = #Injs model @ map (rpair []) (maps Injs_of_bmv_monad (#bmv_ops model));
+    val Injss = #Injs model @ maps Injs_of_bmv_monad (#bmv_ops model);
     val Vrss = #Vrs model @ maps Vrs_of_bmv_monad (#bmv_ops model);
 
-    val axioms = @{map 5} (fn T => fn (own_Injs, other_Injs) => fn Sb => fn Vrs => fn tacs =>
+    val axioms = @{map 5} (fn T => fn Injs => fn Sb => fn Vrs => fn tacs =>
       let
-        val (other_Injs, other_idxs) = split_list other_Injs;
-        val Injs = own_Injs @ other_Injs;
+        val (own_Injs, other_Injs) = partition (fn Inj => body_type (fastype_of Inj) = T) Injs;
+        val other_idxs = map (fn Inj => find_index (fn T => body_type (fastype_of Inj) = T) Ts) other_Injs;
         val ((((rhos, rhos'), aa), x), _) = lthy
           |> mk_Frees "\<rho>" (map fastype_of Injs)
           ||>> mk_Frees "\<rho>'" (map fastype_of Injs)
@@ -160,7 +168,7 @@ fun prove_axioms (model: bmv_monad_model) lthy =
               HOLogic.mk_comp (Term.list_comb (Sb, map (fn Inj =>
                 case List.find (fn rho' => fastype_of rho' = fastype_of Inj) rhos' of
                   NONE => Inj | SOME t => t
-              ) (fst Injs @ map fst (snd Injs))), rho)
+              ) Injs), rho)
             ) other_rhos (map (nth Sbs) other_idxs) (map (nth Injss) other_idxs))
           ))
         )) (fn {context=ctxt, ...} => #Sb_comp tacs ctxt);
@@ -214,12 +222,29 @@ fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lth
       leader = #leader model,
       frees = #frees model,
       lives = #lives model,
-      Injs = map (fn (xs, ys) => xs @ map fst ys) (#Injs model) @ maps (#Injs o Rep_bmv) (#bmv_ops model),
+      Injs = #Injs model @ maps (#Injs o Rep_bmv) (#bmv_ops model),
       Sbs = #Sbs model @ maps (#Sbs o Rep_bmv) (#bmv_ops model),
       Vrs = #Vrs model @ maps (#Vrs o Rep_bmv) (#bmv_ops model),
       Maps = #Maps model @ maps (#Maps o Rep_bmv) (#bmv_ops model),
       axioms = axioms @ maps (#axioms o Rep_bmv) (#bmv_ops model)
     } : bmv_monad;
   in bmv end
 
+(* Cleanup: Throw away op iff any:
+- not the leader
+- does not appear in the codomain of any (=of any **other** SOp) Injection,
+*)
+
+fun compose_bmv_monad qualify outer inners lthy =
+  let
+    val _ = if length (lives_of_bmv_monad outer) <> length inners then
+      error "Outer needs exactly as many lives as there are inners" else ()
+
+    val ops' = map (Term.typ_subst_atomic (lives_of_bmv_monad outer ~~ map (fn bmv =>
+      nth (ops_of_bmv_monad bmv) (leader_of_bmv_monad bmv)
+    ) inners)) (ops_of_bmv_monad outer);
+
+    val _ = @{print} ops'
+  in error "unfinished" end;
+
 end
diff --git a/Tools/mrbnf_util.ML b/Tools/mrbnf_util.ML
@@ -10,6 +10,7 @@ sig
   val cond_automap: ('a -> 'a) -> 'a list -> bool list -> 'a list
   val short_type_name: string -> string
   val swap: 'a * 'b -> 'b * 'a
+  val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
 
   val subst_typ_morphism: (typ * typ) list -> morphism
 
@@ -82,6 +83,8 @@ fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = apfst (cons (x, T))
   | strip_ex t = ([], t)
 
 fun swap (a, b) = (b, a)
+fun partition _ [] = ([], [])
+  | partition f (x::xs) = (if f x then apfst else apsnd) (cons x) (partition f xs)
 
 val mk_minus = HOLogic.mk_binop @{const_name minus};
 fun mk_all (x, T) t = HOLogic.mk_all (x, T, t);

diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy
@@ -103,7 +103,7 @@ val model_FType = {
   frees = [@{typ "'a::var"}],
   lives = [],
   bmv_ops = [],
-  Injs = [([@{term "TyVar :: 'a::var \<Rightarrow> _"}], [])],
+  Injs = [[@{term "TyVar :: 'a::var \<Rightarrow> _"}]],
   Sbs = [@{term "tvsubst_FType :: _ => 'a::var FType => _"}],
   Maps = [NONE],
   Vrs = [[@{term "FVars_FType :: _ => 'a::var set"}]],
@@ -213,20 +213,23 @@ definition Vrs_L2_M2_2 :: "('a1, 'a2::var) L2_M2 \<Rightarrow> 'a2 set" where
 definition Sb_L2 :: "('a1 \<Rightarrow> 'a1) \<Rightarrow> ('a2::var \<Rightarrow> 'a2 FType) \<Rightarrow> ('a1, 'a2) L2 \<Rightarrow> ('a1, 'a2) L2" where
   "Sb_L2 \<equiv> \<lambda>f1 f2. map_prod (id f1) (tvsubst_FType f2)"
 definition Vrs_L2_1 :: "('a1, 'a2) L2 \<Rightarrow> 'a1 set" where
-  "Vrs_L2_1 \<equiv> Vrs_L1_M1_1 \<circ> fst" (* corresponds to L2_M1 and Inj_L2_M1_1 *)
+  "Vrs_L2_1 \<equiv> \<lambda>(x,x2). {x}" (* corresponds to L2_M1 and Inj_L2_M1_1 *)
 definition Vrs_L2_2 :: "('a1, 'a2::var) L2 \<Rightarrow> 'a2 set" where
-  "Vrs_L2_2 \<equiv> Vrs_L2_M2_2 \<circ> snd" (* corresponds to L2_M2 and Inj_L2_M2_2 *)
+  "Vrs_L2_2 \<equiv> \<lambda>(x,x2). FVars_FType x2" (* corresponds to L2_M2 and Inj_L2_M2_2 *)
 
 (* Composition *)
 type_synonym ('a1, 'a2) LC = "('a1, 'a2, ('a1, 'a2) L1, ('a1, 'a2) L2) L"
+typ "('a1, 'a2, 'c1, 'c2) L"
+typ "('a1, 'a2) L1"
+typ "('a1, 'a2) LC"
 type_synonym ('a1, 'a2) L_MC = "('a1, 'a2, ('a1, 'a2) L1, ('a1, 'a2) L2) L_M1"
 typ "('a1, 'a2) L_MC" (* is the same as LC_M1, so do not add *)
 
-type_synonym ('a1, 'a2) LC_M1 = "('a1, 'a2) L1_M1"
-type_synonym ('a1, 'a2) LC_M2 = "('a1, 'a2) L1_M2"
-type_synonym ('a1, 'a2) LC_M3 = "('a1, 'a2) L2_M2"
-
+typ "('a1, 'a2) L1_M1"
+typ "('a1, 'a2) L1_M2"
+typ "('a1, 'a2) L2_M2"
 
+declare [[ML_print_depth=10000]]
 
 ML \<open>
 val model_ID = {
@@ -236,7 +239,7 @@ val model_ID = {
   lives = [],
   bmv_ops = [],
   Maps = [NONE],
-  Injs = [([@{term "id :: 'a \<Rightarrow> _"}], [])],
+  Injs = [[@{term "id :: 'a \<Rightarrow> _"}]],
   Sbs = [@{term "id :: _ => 'a => 'a"}],
   Vrs = [[@{term "\<lambda>(x::'a). {x}"}]],
   tacs = [{
@@ -282,7 +285,7 @@ val model_L = {
       BMV_Monad_Def.frees_of_bmv_monad id_bmv ~~ [@{typ "'a1"}]
   )) id_bmv],
   Maps = [SOME @{term "\<lambda>(f1::'c1 => 'c1') (f2::'c2 => 'c2') (a1::'a1, a2::'a1, p). (a1, a2, map_sum f1 f2 p)"}],
-  Injs = [([], [(@{term "id :: 'a1 \<Rightarrow> 'a1"}, 1)])],
+  Injs = [[@{term "id :: 'a1 \<Rightarrow> 'a1"}]],
   Sbs = [@{term "Sb_L :: _ \<Rightarrow> _ \<Rightarrow> ('a1, 'a2, 'c1, 'c2) L"}],
   Vrs = [[
     @{term "\<lambda>(x1::'a1, x2::'a1, p::'c1 + 'c2). {x1, x2}"}
@@ -352,7 +355,7 @@ val model_L1 = {
     )) id_bmv
   ],
   Maps = [NONE],
-  Injs = [([], [(@{term "id :: 'a1 \<Rightarrow> 'a1"}, 1), (@{term "id :: 'a2 \<Rightarrow> 'a2"}, 2)])],
+  Injs = [[@{term "id :: 'a1 \<Rightarrow> 'a1"}, @{term "id :: 'a2 \<Rightarrow> 'a2"}]],
   Sbs = [@{term "Sb_L1 :: _ \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> ('a1, 'a2) L1"}],
   Vrs = [[@{term "\<lambda>(x::'a1, x2::'a2). {x}"}, @{term "\<lambda>(x::'a1, x2::'a2). {x2}"}]],
   tacs = [{
@@ -405,11 +408,84 @@ ML \<open>
 val L1_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L1 @{context}
 \<close>
 
+(* ML \<open>
+val model_L2 = {
+  ops = [@{typ "'a2 * 'a2::var FType"}],
+  leader = 0,
+  frees = [@{typ "'a2::var"}],
+  lives = [],
+  bmv_ops = [
+    BMV_Monad_Def.morph_bmv_monad (
+      MRBNF_Util.subst_typ_morphism (
+        BMV_Monad_Def.frees_of_bmv_monad id_bmv ~~ [@{typ "'a2::var"}]
+    )) id_bmv,
+    BMV_Monad_Def.morph_bmv_monad (
+      MRBNF_Util.subst_typ_morphism (
+        BMV_Monad_Def.frees_of_bmv_monad FType_bmv ~~ [@{typ "'a2::var"}]
+    )) FType_bmv
+  ],
+  Maps = [NONE],
+  Injs = [([], [(@{term "id :: 'a2::var \<Rightarrow> 'a2"}, 1), (@{term "TyVar :: 'a2::var \<Rightarrow> 'a2 FType"}, 2)])],
+  Sbs = [@{term "Sb_L2 :: _ \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> ('a2, 'a2::var) L2"}],
+  Vrs = [[@{term "Vrs_L2_1 :: ('a2, 'a2::var) L2 \<Rightarrow> _"}, @{term "Vrs_L2_2 :: ('a2, 'a2::var) L2 \<Rightarrow> _"}]],
+  tacs = [{
+    Sb_Inj = fn ctxt => EVERY1 [
+      K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Sb_Inj_FType id_apply prod.map_id0}),
+      resolve_tac ctxt [refl]
+    ],
+    Sb_comp_Injs = [],
+    Sb_comp = fn ctxt => EVERY1 [
+      K (Local_Defs.unfold0_tac ctxt (
+        (BNF_Def.map_comp0_of_bnf (the (BNF_Def.bnf_of @{context} "Product_Type.prod")) RS sym)
+        :: @{thms Sb_L2_def id_apply Sb_comp_FType[unfolded SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]]}
+      )),
+      resolve_tac ctxt [refl]
+    ],
+    Vrs_Injs = [],
+    Vrs_Sbs = [
+      fn ctxt => EVERY1 [
+        K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_1_def case_prod_map_prod}),
+        K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta UN_single id_apply}),
+        resolve_tac ctxt [refl]
+      ],
+      fn ctxt => EVERY1 [
+        K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_2_def case_prod_map_prod}),
+        K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta UN_single id_apply}),
+        resolve_tac ctxt @{thms Vrs_Sb_FType},
+        K (Local_Defs.unfold0_tac ctxt @{thms SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]}),
+        assume_tac ctxt
+      ]
+    ],
+    Sb_cong = fn ctxt => EVERY1 [
+      K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_1_def Vrs_L2_2_def case_prod_beta id_apply}),
+      resolve_tac ctxt @{thms prod.map_cong0},
+      eresolve_tac ctxt @{thms Basic_BNFs.fsts.cases},
+      dresolve_tac ctxt @{thms meta_spec},
+      dresolve_tac ctxt @{thms meta_mp},
+      resolve_tac ctxt @{thms singletonI},
+      hyp_subst_tac ctxt,
+      assume_tac ctxt,
+      eresolve_tac ctxt @{thms Basic_BNFs.snds.cases},
+      resolve_tac ctxt @{thms Sb_cong_FType[unfolded SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]]},
+      REPEAT_DETERM o assume_tac ctxt,
+      rotate_tac ~3,
+      dresolve_tac ctxt @{thms meta_spec},
+      dresolve_tac ctxt @{thms meta_mp},
+      hyp_subst_tac ctxt,
+      assume_tac ctxt,
+      assume_tac ctxt
+    ]
+  } : (Proof.context -> tactic) BMV_Monad_Def.bmv_monad_axioms]
+} : BMV_Monad_Def.bmv_monad_model;
+\<close>
+ML \<open>
+val L2_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L2 @{context}
+\<close> *)
 ML \<open>
 val model_L2 = {
   ops = [@{typ "'a1 * 'a2::var FType"}],
   leader = 0,
-  frees = [@{typ "'a1"}, @{typ "'a2::var"}],
+  frees = [@{typ 'a1}, @{typ "'a2::var"}],
   lives = [],
   bmv_ops = [
     BMV_Monad_Def.morph_bmv_monad (
@@ -422,9 +498,9 @@ val model_L2 = {
     )) FType_bmv
   ],
   Maps = [NONE],
-  Injs = [([], [(@{term "id :: 'a1 \<Rightarrow> 'a1"}, 1), (@{term "TyVar :: 'a2::var \<Rightarrow> 'a2 FType"}, 2)])],
+  Injs = [[@{term "id :: 'a1 \<Rightarrow> 'a1"}, @{term "TyVar :: 'a2::var \<Rightarrow> 'a2 FType"}]],
   Sbs = [@{term "Sb_L2 :: _ \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> ('a1, 'a2::var) L2"}],
-  Vrs = [[@{term "\<lambda>(x::'a1, x2::'a2::var FType). {x}"}, @{term "\<lambda>(x::'a1, x2::'a2::var FType). FVars_FType x2"}]],
+  Vrs = [[@{term "Vrs_L2_1 :: ('a1, 'a2::var) L2 \<Rightarrow> _"}, @{term "Vrs_L2_2 :: ('a1, 'a2::var) L2 \<Rightarrow> _"}]],
   tacs = [{
     Sb_Inj = fn ctxt => EVERY1 [
       K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Sb_Inj_FType id_apply prod.map_id0}),
@@ -441,20 +517,20 @@ val model_L2 = {
     Vrs_Injs = [],
     Vrs_Sbs = [
       fn ctxt => EVERY1 [
-        K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def case_prod_map_prod}),
+        K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_1_def case_prod_map_prod}),
         K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta UN_single id_apply}),
         resolve_tac ctxt [refl]
       ],
       fn ctxt => EVERY1 [
-        K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def case_prod_map_prod}),
+        K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_2_def case_prod_map_prod}),
         K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta UN_single id_apply}),
         resolve_tac ctxt @{thms Vrs_Sb_FType},
         K (Local_Defs.unfold0_tac ctxt @{thms SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\<eta>_FType_tvsubst_FType_def TyVar_def[symmetric]}),
         assume_tac ctxt
       ]
     ],
     Sb_cong = fn ctxt => EVERY1 [
-      K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def case_prod_beta id_apply}),
+      K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_1_def Vrs_L2_2_def case_prod_beta id_apply}),
       resolve_tac ctxt @{thms prod.map_cong0},
       eresolve_tac ctxt @{thms Basic_BNFs.fsts.cases},
       dresolve_tac ctxt @{thms meta_spec},
@@ -479,4 +555,8 @@ ML \<open>
 val L2_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L2 @{context}
 \<close>
 
+ML \<open>
+val x = BMV_Monad_Def.compose_bmv_monad I L_bmv [L1_bmv, L2_bmv] @{context}
+\<close>
+
 end
diff --git a/operations/VVSubst.thy b/operations/VVSubst.thy
@@ -767,10 +767,6 @@ val fp_res = the (MRBNF_FP_Def_Sugar.fp_result_of @{context} "Least_Fixpoint.T1"
 ML_file \<open>../Tools/mrbnf_recursor_tactics.ML\<close>
 ML_file \<open>../Tools/mrbnf_recursor.ML\<close>
 
-ML \<open>
-Multithreading.parallel_proofs := 0
-\<close>
-
 local_setup \<open>fn lthy =>
 let
   val qualify = I