Add vars_bd theorems to BMV Monad

jvanbruegge · Dec 12, 2024 · f7fc766 · f7fc766
1 parent 637e16f
commit f7fc766
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 3 deletions.
diff --git a/Tools/bmv_monad_def.ML b/Tools/bmv_monad_def.ML
@@ -7,7 +7,7 @@ signature BMV_MONAD_DEF = sig
     Sb_comp_Injs: 'a list,
     Sb_comp: 'a,
     Sb_cong: 'a,
-    (* TODO: Add Vrs_bd axiom *)
+    Vrs_bds: 'a option list list,
     Vrs_Injs: 'a option list list,
     Vrs_Sbs: 'a option list list
     (* Add optional Map_Sb axiom (dependent on iff Map exists) *)
@@ -56,17 +56,19 @@ type 'a bmv_monad_axioms = {
   Sb_comp_Injs: 'a list,
   Sb_comp: 'a,
   Sb_cong: 'a,
+  Vrs_bds: 'a option list list,
   Vrs_Injs: 'a option list list,
   Vrs_Sbs: 'a option list list
 };
 
 fun morph_bmv_axioms phi {
-  Sb_Inj, Sb_comp_Injs, Sb_comp, Sb_cong, Vrs_Injs, Vrs_Sbs
+  Sb_Inj, Sb_comp_Injs, Sb_comp, Sb_cong, Vrs_bds, Vrs_Injs, Vrs_Sbs
 } = {
   Sb_Inj = Morphism.thm phi Sb_Inj,
   Sb_comp_Injs = map (Morphism.thm phi) Sb_comp_Injs,
   Sb_comp = Morphism.thm phi Sb_comp,
   Sb_cong = Morphism.thm phi Sb_cong,
+  Vrs_bds = map (map (Option.map (Morphism.thm phi))) Vrs_bds,
   Vrs_Injs = map (map (Option.map (Morphism.thm phi))) Vrs_Injs,
   Vrs_Sbs = map (map (Option.map (Morphism.thm phi))) Vrs_Sbs
 } : thm bmv_monad_axioms
@@ -200,6 +202,12 @@ fun prove_axioms (model: bmv_monad_model) lthy =
           ))
         )) (fn {context=ctxt, ...} => #Sb_comp tacs ctxt);
 
+        val Vrs_bds = map2 (map2 (@{map_option 2} (fn Vrs => fn tac =>
+          Goal.prove_sorry lthy [] [] (Logic.all x (HOLogic.mk_Trueprop (
+            mk_ordLess (mk_card_of (Vrs $ x)) (#bd model)
+          ))) (fn {context=ctxt, ...} => tac ctxt)
+        ))) Vrs (#Vrs_bds tacs);
+
         val Vrs_Injs = @{map 3} (fn Inj => map2 (@{map_option 2} (fn tac => fn Vrs =>
           let
             val a = the (List.find (fn a => fastype_of a = hd (binder_types (fastype_of Inj))) aa);
@@ -246,9 +254,10 @@ fun prove_axioms (model: bmv_monad_model) lthy =
         Sb_comp_Injs = Sb_comp_Injs,
         Sb_comp = Sb_comp,
         Vrs_Injs = Vrs_Injs,
+        Vrs_bds = Vrs_bds,
         Vrs_Sbs = Vrs_Sbs,
         Sb_cong = Sb_cong
-      } end
+      } : thm bmv_monad_axioms end
     ) (#ops model) (#Injs model) (#Sbs model) (#Vrs model) (#tacs model);
   in axioms end;
 

diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy
@@ -121,6 +121,7 @@ val model_FType = {
       K (Local_Defs.unfold0_tac ctxt @{thms SSupp_FType_def VVr_eq_Var}),
       REPEAT_DETERM o assume_tac ctxt
     ],
+    Vrs_bds = [[SOME (fn ctxt => resolve_tac ctxt @{thms FType.set_bd} 1)]],
     Vrs_Injs = [[SOME (fn ctxt => resolve_tac ctxt @{thms Vrs_Inj_FType} 1)]],
     Vrs_Sbs = [[SOME (fn ctxt => EVERY1 [
       resolve_tac ctxt @{thms Vrs_Sb_FType},
@@ -259,6 +260,7 @@ val model_ID = {
       K (Local_Defs.unfold0_tac ctxt @{thms comp_def id_def}),
       resolve_tac ctxt [refl]
     ],
+    Vrs_bds = [[SOME (fn ctxt => resolve_tac ctxt @{thms ID.set_bd} 1)]],
     Vrs_Injs = [[SOME (fn ctxt => EVERY1 [
       K (Local_Defs.unfold0_tac ctxt @{thms comp_def id_def}),
       resolve_tac ctxt [refl]
@@ -281,6 +283,9 @@ ML \<open>
 val id_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_ID @{context})
 \<close>
 
+lemma insert_bound: "Cinfinite r \<Longrightarrow> |A| <o r \<Longrightarrow> |insert x A| <o r"
+  by (metis Card_order_iff_ordLeq_card_of card_of_Field_ordIso card_of_Un_singl_ordLess_infinite1 cinfinite_def insert_is_Un ordLess_ordIso_trans ordLess_ordLeq_trans)
+
 ML \<open>
 val model_L = {
   ops = [@{typ "'a1 * 'a1 * ('c1 + 'c2)"}],
@@ -312,6 +317,12 @@ val model_L = {
       )),
       resolve_tac ctxt [refl]
     ],
+    Vrs_bds = [[SOME (fn ctxt => EVERY1 [
+      K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta}),
+      resolve_tac ctxt @{thms insert_bound},
+      resolve_tac ctxt @{thms natLeq_Cinfinite},
+      resolve_tac ctxt @{thms ID.set_bd}
+    ])]],
     Vrs_Injs = [],
     Vrs_Sbs = [[SOME (fn ctxt => EVERY1 [
       K (Local_Defs.unfold0_tac ctxt @{thms Sb_L_def case_prod_beta
@@ -385,6 +396,10 @@ val model_L1 = {
       )),
       resolve_tac ctxt [refl]
     ],
+    Vrs_bds = [
+      [SOME (fn ctxt => Local_Defs.unfold0_tac ctxt @{thms case_prod_beta} THEN resolve_tac ctxt @{thms ID.set_bd} 1), NONE],
+      [NONE, SOME (fn ctxt => Local_Defs.unfold0_tac ctxt @{thms case_prod_beta} THEN resolve_tac ctxt @{thms ID.set_bd} 1)]
+    ],
     Vrs_Injs = [],
     Vrs_Sbs = [
       [SOME (fn ctxt => EVERY1 [
@@ -465,6 +480,16 @@ val model_L2 = {
       )),
       resolve_tac ctxt [refl]
     ],
+    Vrs_bds = [
+      [SOME (fn ctxt => Local_Defs.unfold0_tac ctxt @{thms case_prod_beta Vrs_L2_1_def} THEN resolve_tac ctxt @{thms ID.set_bd} 1), NONE],
+      [NONE, SOME (fn ctxt => EVERY1 [
+        K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta Vrs_L2_2_def}),
+        resolve_tac ctxt @{thms insert_bound},
+        resolve_tac ctxt @{thms natLeq_Cinfinite},
+        resolve_tac ctxt @{thms ID.set_bd}
+      ])],
+      [NONE, SOME (fn ctxt => Local_Defs.unfold0_tac ctxt @{thms case_prod_beta Vrs_L2_3_def} THEN resolve_tac ctxt @{thms FType.set_bd} 1)]
+    ],
     Vrs_Injs = [],
     Vrs_Sbs = [
       [SOME (fn ctxt => EVERY1 [