From 637e16f82598631248126009c8acae61d78941bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Thu, 12 Dec 2024 18:03:16 +0000 Subject: [PATCH] Have one Vrs operator per injection and (optionally) var type --- Tools/bmv_monad_def.ML | 82 ++++++++++-------- Tools/mrbnf_util.ML | 11 +++ operations/BMV_Monad.thy | 182 ++++++++++++++++----------------------- 3 files changed, 133 insertions(+), 142 deletions(-) diff --git a/Tools/bmv_monad_def.ML b/Tools/bmv_monad_def.ML index a218d0b..93fd0f2 100644 --- a/Tools/bmv_monad_def.ML +++ b/Tools/bmv_monad_def.ML @@ -8,8 +8,8 @@ signature BMV_MONAD_DEF = sig Sb_comp: 'a, Sb_cong: 'a, (* TODO: Add Vrs_bd axiom *) - Vrs_Injs: 'a list, (* TODO: One per Inj AND var kind *) - Vrs_Sbs: 'a list + Vrs_Injs: 'a option list list, + Vrs_Sbs: 'a option list list (* Add optional Map_Sb axiom (dependent on iff Map exists) *) }; @@ -24,7 +24,7 @@ signature BMV_MONAD_DEF = sig Injs: term list list, Sbs: term list, Maps: term option list, - Vrs: term list list, + Vrs: term option list list list, tacs: (Proof.context -> tactic) bmv_monad_axioms list } @@ -37,7 +37,7 @@ signature BMV_MONAD_DEF = sig val Injs_of_bmv_monad: bmv_monad -> term list list; val Sbs_of_bmv_monad: bmv_monad -> term list; val Maps_of_bmv_monad: bmv_monad -> term option list; - val Vrs_of_bmv_monad: bmv_monad -> term list list; + val Vrs_of_bmv_monad: bmv_monad -> term option list list list; val morph_bmv_monad: morphism -> bmv_monad -> bmv_monad; @@ -56,8 +56,8 @@ type 'a bmv_monad_axioms = { Sb_comp_Injs: 'a list, Sb_comp: 'a, Sb_cong: 'a, - Vrs_Injs: 'a list, - Vrs_Sbs: 'a list + Vrs_Injs: 'a option list list, + Vrs_Sbs: 'a option list list }; fun morph_bmv_axioms phi { @@ -67,8 +67,8 @@ fun morph_bmv_axioms phi { 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_Injs = map (Morphism.thm phi) Vrs_Injs, - Vrs_Sbs = map (Morphism.thm phi) Vrs_Sbs + 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 datatype bmv_monad = BMV of { @@ -81,7 +81,7 @@ datatype bmv_monad = BMV of { Injs: term list list, Sbs: term list, Maps: term option list, - Vrs: term list list (*list*), (* TODO: Need Vr operator per Injection *) + Vrs: term option list list list, axioms: thm bmv_monad_axioms list } @@ -97,7 +97,7 @@ fun morph_bmv_monad phi (BMV { Injs = map (map (Morphism.term phi)) Injs, Sbs = map (Morphism.term phi) Sbs, Maps = map (Option.map (Morphism.term phi)) Maps, - Vrs = map (map (Morphism.term phi)) Vrs, + Vrs = map (map (map (Option.map (Morphism.term phi)))) Vrs, axioms = map (morph_bmv_axioms phi) axioms } @@ -127,11 +127,11 @@ type bmv_monad_model = { Injs: term list list, Sbs: term list, Maps: term option list, - Vrs: term list list, + Vrs: term option list list list, tacs: (Proof.context -> tactic) bmv_monad_axioms list } -fun morph_bmv_monad_model phi { ops, bd, var_class, frees, lives, bmv_ops, leader, Injs, Sbs, Maps, Vrs, tacs } = { +fun morph_bmv_monad_model phi ({ ops, bd, var_class, frees, lives, bmv_ops, leader, Injs, Sbs, Maps, Vrs, tacs }: bmv_monad_model) = { ops = map (Morphism.typ phi) ops, bd = Morphism.term phi bd, var_class = var_class, @@ -142,7 +142,7 @@ fun morph_bmv_monad_model phi { ops, bd, var_class, frees, lives, bmv_ops, leade Injs = map (map (Morphism.term phi)) Injs, Sbs = map (Morphism.term phi) Sbs, Maps = map (Option.map (Morphism.term phi)) Maps, - Vrs = map (map (Morphism.term phi)) Vrs, + Vrs = map (map (map (Option.map (Morphism.term phi)))) Vrs, tacs = tacs } : bmv_monad_model; @@ -155,7 +155,8 @@ fun prove_axioms (model: bmv_monad_model) lthy = val axioms = @{map 5} (fn T => fn Injs => fn Sb => fn Vrs => fn tacs => let - val (own_Injs, other_Injs) = partition (fn Inj => body_type (fastype_of Inj) = T) Injs; + val (own_Injs, other_Injs) = partition (fn Inj => member (op=) (#ops model) (body_type (fastype_of Inj))) Injs; + val is_own_Inj = map (member (op=) (#ops model) o body_type o fastype_of) 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 "\" (map fastype_of Injs) @@ -199,30 +200,42 @@ fun prove_axioms (model: bmv_monad_model) lthy = )) )) (fn {context=ctxt, ...} => #Sb_comp tacs ctxt); - val Vrs_Injs = @{map 4} (fn Vrs => fn Inj => fn a => fn tac => Goal.prove_sorry lthy [] [] ( - Logic.all a (mk_Trueprop_eq (Vrs $ (Inj $ a), mk_singleton a)) - ) (fn {context=ctxt, ...} => tac ctxt)) (take nown Vrs) own_Injs (take nown aa) (#Vrs_Injs tacs); - - val Vrs_Sbs = map2 (fn Vr => fn tac => Goal.prove_sorry lthy [] [] (fold_rev Logic.all (rhos @ [x]) ( - fold_rev (curry Logic.mk_implies) small_prems (mk_Trueprop_eq ( - Vr $ (Term.list_comb (Sb, rhos) $ x), - foldl1 mk_Un (@{map_filter 2} (fn rho => Option.map (fn Vrs' => mk_UNION (Vr $ x) ( - Term.abs ("a", HOLogic.dest_setT (snd (dest_funT (fastype_of Vrs')))) ( - Vrs' $ (rho $ Bound 0) - ) - ))) rhos (map SOME (take nown Vrs) @ map (fn idx => - List.find (fn t => body_type (fastype_of t) = body_type (fastype_of Vr)) (nth Vrss idx) - ) other_idxs)) - )) - )) (fn {context=ctxt, ...} => tac ctxt)) Vrs (#Vrs_Sbs 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); + val T = HOLogic.dest_setT (body_type (fastype_of Vrs)); + in Goal.prove_sorry lthy [] [] ( + Logic.all a (mk_Trueprop_eq ( + Vrs $ (Inj $ a), + if fastype_of a = T then mk_singleton a else mk_bot T)) + ) (fn {context=ctxt, ...} => tac ctxt) end))) own_Injs (#Vrs_Injs tacs) (cond_keep Vrs is_own_Inj); + + val Vrs_Sbs = @{map 3} (fn rho => map2 (@{map_option 2} (fn Vrs => fn tac => + let + val var = HOLogic.dest_setT (body_type (fastype_of Vrs)); + val idx = find_index (fn T => body_type (fastype_of rho) = T) Ts; + val idx' = find_index (fn t => fastype_of t = fastype_of rho) (nth Injss idx); + val Vrs' = hd (map_filter (Option.mapPartial (fn t => + if HOLogic.dest_setT (body_type (fastype_of t)) = var then SOME t else NONE + )) (nth (nth Vrss idx) idx')); + + val goal = fold_rev Logic.all (rhos @ [x]) ( + fold_rev (curry Logic.mk_implies) small_prems (mk_Trueprop_eq ( + Vrs $ (Term.list_comb (Sb, rhos) $ x), + mk_UNION (Vrs $ x) (Term.abs ("a", var) (Vrs' $ (rho $ Bound 0))) + )) + ); + in Goal.prove_sorry lthy [] [] goal (fn {context=ctxt, ...} => tac ctxt) end + ))) rhos Vrs (#Vrs_Sbs tacs); val Sb_cong = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (rhos @ rhos' @ [x]) ( - fold_rev (curry Logic.mk_implies) (small_prems @ small_prems' @ @{map 4} (fn rho => fn rho' => fn Vrs => fn a => - Logic.all a (Logic.mk_implies ( + fold_rev (curry Logic.mk_implies) (small_prems @ small_prems' @ flat (@{map 3} (fn rho => fn rho' => map_filter (Option.map (fn Vrs => + let val a = the (List.find (fn t => fastype_of t = HOLogic.dest_setT (body_type (fastype_of Vrs))) aa) + in Logic.all a (Logic.mk_implies ( HOLogic.mk_Trueprop (HOLogic.mk_mem (a, Vrs $ x)), mk_Trueprop_eq (rho $ a, rho' $ a) - )) - ) rhos rhos' Vrs aa) (mk_Trueprop_eq ( + )) end + ))) rhos rhos' Vrs)) (mk_Trueprop_eq ( Term.list_comb (Sb, rhos) $ x, Term.list_comb (Sb, rhos') $ x ) @@ -247,6 +260,7 @@ fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lth fst (dest_ordLeq (HOLogic.dest_Trueprop (Thm.prop_of var_large))) ))); in if bd' <> #bd model then error "var_class does not match bound" else () end + val frees = map (fn T => TFree (apsnd ( Sign.minimize_sort (Proof_Context.theory_of lthy) o cons (#var_class model) ) (dest_TFree T))) (#frees model); diff --git a/Tools/mrbnf_util.ML b/Tools/mrbnf_util.ML index 953ae7d..06a3b75 100644 --- a/Tools/mrbnf_util.ML +++ b/Tools/mrbnf_util.ML @@ -360,6 +360,7 @@ val parameter = Parse.position Parse.nat >> (fn (n, pos) => fun indices n = map string_of_int (1 upto n); fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); +fun some n = implode (map (fn a => " (SOME x" ^ a ^ ")") (indices n)); fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); in @@ -373,6 +374,16 @@ val _ = Theory.setup \ | map_filter f" ^ cons n ^ " = let val ys = map_filter f" ^ vars "xs" n ^ " in the_default ys (Option.map (fn y => y::ys) (f" ^ vars "x" n ^ ")) end\n\ \ | map_filter _" ^ replicate_string n " _" ^ " = raise ListPair.UnequalLengths\n" ^ " in map_filter f end"))) + +val _ = Theory.setup + (ML_Antiquotation.value \<^binding>\map_option\ + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun map_option _" ^ replicate_string n " NONE" ^ " = NONE\n\ + \ | map_option f" ^ some n ^ " = SOME (f" ^ vars "x" n ^ ")\n\ + \ | map_option _" ^ replicate_string n " _" ^ " = raise ListPair.UnequalLengths\n" ^ + " in map_option f end"))) end; end; diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy index 0839f5e..059d85c 100644 --- a/operations/BMV_Monad.thy +++ b/operations/BMV_Monad.thy @@ -108,7 +108,7 @@ val model_FType = { Injs = [[@{term "TyVar :: 'a::var \ _"}]], Sbs = [@{term "tvsubst_FType :: _ => 'a::var FType => _"}], Maps = [NONE], - Vrs = [[@{term "FVars_FType :: _ => 'a::var set"}]], + Vrs = [[[SOME @{term "FVars_FType :: _ => 'a::var set"}]]], tacs = [{ Sb_Inj = fn ctxt => resolve_tac ctxt @{thms Sb_Inj_FType} 1, Sb_comp_Injs = [fn ctxt => EVERY1 [ @@ -121,12 +121,12 @@ val model_FType = { K (Local_Defs.unfold0_tac ctxt @{thms SSupp_FType_def VVr_eq_Var}), REPEAT_DETERM o assume_tac ctxt ], - Vrs_Injs = [fn ctxt => resolve_tac ctxt @{thms Vrs_Inj_FType} 1], - Vrs_Sbs = [fn ctxt => EVERY1 [ + 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}, K (Local_Defs.unfold0_tac ctxt @{thms SSupp_FType_def VVr_eq_Var}), assume_tac ctxt - ]], + ])]], Sb_cong = fn ctxt => EVERY1 [ resolve_tac ctxt @{thms Sb_cong_FType}, K (Local_Defs.unfold0_tac ctxt @{thms SSupp_FType_def VVr_eq_Var}), @@ -150,9 +150,10 @@ type_synonym ('a1, 'a2) L1 = "'a1 * 'a2" type_synonym ('a1, 'a2) L1_M1 = "'a1" type_synonym ('a1, 'a2) L1_M2 = "'a2" -type_synonym ('a1, 'a2) L2 = "'a1 * 'a2 FType" +type_synonym ('a1, 'a2) L2 = "'a1 * 'a2 * 'a2 * 'a2 FType" type_synonym ('a1, 'a2) L2_M1 = "'a1" - type_synonym ('a1, 'a2) L2_M2 = "'a2 FType" + type_synonym ('a1, 'a2) L2_M2 = "'a2" + type_synonym ('a1, 'a2) L2_M3 = "'a2 FType" (* Dispatcher *) (* from L_M1 *) @@ -205,19 +206,21 @@ definition Vrs_L2_M1_1 :: "('a1, 'a2) L2_M1 \ 'a1 set" where definition Vrs_L2_M1_2 :: "('a1, 'a2) L2_M1 \ 'a2 set" where "Vrs_L2_M1_2 \ \a. {}" (* corresponds to L2_M2 and Inj_L2_M2_2 *) *) (* and its minions M2 *) -definition Sb_L2_M2 :: "('a2::var \ 'a2 FType) \ ('a1, 'a2) L2_M2 \ ('a1, 'a2) L2_M2" where +definition Sb_L2_M2 :: "('a2::var \ 'a2 FType) \ ('a1, 'a2) L2_M3 \ ('a1, 'a2) L2_M3" where "Sb_L2_M2 \ tvsubst_FType" definition Vrs_L2_M2_1 :: "('a1, 'a2) L2_M2 \ 'a1 set" where "Vrs_L2_M2_1 \ \a. {}" (* corresponds to L2_M1 and Inj_L2_M1_1 *) -definition Vrs_L2_M2_2 :: "('a1, 'a2::var) L2_M2 \ 'a2 set" where +definition Vrs_L2_M2_2 :: "('a1, 'a2::var) L2_M3 \ 'a2 set" where "Vrs_L2_M2_2 \ FVars_FType" (* corresponds to L2_M2 and Inj_L2_M2_2 *) (* and then the leader L2 itself *) -definition Sb_L2 :: "('a1 \ 'a1) \ ('a2::var \ 'a2 FType) \ ('a1, 'a2) L2 \ ('a1, 'a2) L2" where - "Sb_L2 \ \f1 f2. map_prod (id f1) (tvsubst_FType f2)" +definition Sb_L2 :: "('a1 \ 'a1) \ ('a2 \ 'a2) \ ('a2::var \ 'a2 FType) \ ('a1, 'a2) L2 \ ('a1, 'a2) L2" where + "Sb_L2 \ \f1 f2 f3. map_prod (id f1) (map_prod (id f2) (map_prod (id f2) (tvsubst_FType f3)))" definition Vrs_L2_1 :: "('a1, 'a2) L2 \ 'a1 set" where - "Vrs_L2_1 \ \(x,x2). {x}" (* corresponds to L2_M1 and Inj_L2_M1_1 *) + "Vrs_L2_1 \ \(x,x2,x3,x4). {x}" (* corresponds to L2_M1 and Inj_L2_M1_1 *) definition Vrs_L2_2 :: "('a1, 'a2::var) L2 \ 'a2 set" where - "Vrs_L2_2 \ \(x,x2). FVars_FType x2" (* corresponds to L2_M2 and Inj_L2_M2_2 *) + "Vrs_L2_2 \ \(x,x2,x3,x4). {x2,x3}" (* corresponds to L2_M2 and Inj_L2_M2_2 *) +definition Vrs_L2_3 :: "('a1, 'a2::var) L2 \ 'a2 set" where + "Vrs_L2_3 \ \(x,x2,x3,x4). FVars_FType x4" (* corresponds to L2_M2 and Inj_L2_M2_2 *) (* Composition *) type_synonym ('a1, 'a2) LC = "('a1, 'a2, ('a1, 'a2) L1, ('a1, 'a2) L2) L" @@ -245,7 +248,7 @@ val model_ID = { Maps = [NONE], Injs = [[@{term "id :: 'a \ _"}]], Sbs = [@{term "id :: _ => 'a => 'a"}], - Vrs = [[@{term "\(x::'a). {x}"}]], + Vrs = [[[SOME @{term "\(x::'a). {x}"}]]], tacs = [{ Sb_Inj = fn ctxt => resolve_tac ctxt @{thms id_apply} 1, Sb_comp_Injs = [fn ctxt => EVERY1 [ @@ -256,14 +259,14 @@ val model_ID = { K (Local_Defs.unfold0_tac ctxt @{thms comp_def id_def}), resolve_tac ctxt [refl] ], - Vrs_Injs = [fn ctxt => EVERY1 [ + Vrs_Injs = [[SOME (fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms comp_def id_def}), resolve_tac ctxt [refl] - ]], - Vrs_Sbs = [fn ctxt => EVERY1 [ + ])]], + Vrs_Sbs = [[SOME (fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms UN_single id_def}), resolve_tac ctxt [refl] - ]], + ])]], Sb_cong = fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms comp_def id_def}), dresolve_tac ctxt @{thms meta_spec}, @@ -284,7 +287,7 @@ val model_L = { bd = @{term natLeq}, var_class = @{class var}, leader = 0, - frees = [@{typ "'a1"}, @{typ "'a2"}], + frees = [@{typ "'a1"}], lives = [@{typ "'c1"}, @{typ "'c2"}], bmv_ops = [BMV_Monad_Def.morph_bmv_monad ( MRBNF_Util.subst_typ_morphism ( @@ -293,9 +296,9 @@ val model_L = { Maps = [SOME @{term "\(f1::'c1 => 'c1') (f2::'c2 => 'c2') (a1::'a1, a2::'a1, p). (a1, a2, map_sum f1 f2 p)"}], Injs = [[@{term "id :: 'a1 \ 'a1"}]], Sbs = [@{term "Sb_L :: _ \ _ \ ('a1, 'a2, 'c1, 'c2) L"}], - Vrs = [[ - @{term "\(x1::'a1, x2::'a1, p::'c1 + 'c2). {x1, x2}"} - ]], + Vrs = [[[ + SOME @{term "\(x1::'a1, x2::'a1, p::'c1 + 'c2). {x1, x2}"} + ]]], tacs = [{ Sb_Inj = fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L_def prod.map_id0}), @@ -310,13 +313,13 @@ val model_L = { resolve_tac ctxt [refl] ], Vrs_Injs = [], - Vrs_Sbs = [fn ctxt => EVERY1 [ - K (Local_Defs.unfold0_tac ctxt @{thms Sb_L_def case_prod_beta + Vrs_Sbs = [[SOME (fn ctxt => EVERY1 [ + K (Local_Defs.unfold0_tac ctxt @{thms Sb_L_def case_prod_beta Product_Type.fst_map_prod Product_Type.snd_map_prod UN_insert UN_empty Un_empty_right insert_is_Un[symmetric] }), resolve_tac ctxt [refl] - ]], + ])]], Sb_cong = fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L_def case_prod_beta}), resolve_tac ctxt @{thms prod.map_cong0}, @@ -365,7 +368,10 @@ val model_L1 = { Maps = [NONE], Injs = [[@{term "id :: 'a1 \ 'a1"}, @{term "id :: 'a2 \ 'a2"}]], Sbs = [@{term "Sb_L1 :: _ \ _ \ _ \ ('a1, 'a2) L1"}], - Vrs = [[@{term "\(x::'a1, x2::'a2). {x}"}, @{term "\(x::'a1, x2::'a2). {x2}"}]], + Vrs = [[ + [SOME @{term "\(x::'a1, x2::'a2). {x}"}, NONE], + [NONE, SOME @{term "\(x::'a1, x2::'a2). {x2}"}] + ]], tacs = [{ Sb_Inj = fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L1_def prod.map_id0}), @@ -381,16 +387,16 @@ val model_L1 = { ], Vrs_Injs = [], Vrs_Sbs = [ - fn ctxt => EVERY1 [ + [SOME (fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L1_def case_prod_map_prod}), K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta UN_single}), resolve_tac ctxt [refl] - ], - fn ctxt => EVERY1 [ + ]), NONE], + [NONE, SOME (fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L1_def case_prod_map_prod}), K (Local_Defs.unfold0_tac ctxt @{thms case_prod_beta UN_single}), resolve_tac ctxt [refl] - ] + ])] ], Sb_cong = fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L1_def case_prod_beta}), @@ -416,16 +422,22 @@ ML \ val L1_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L1 @{context}) \ -(* ML \ +ML \ val model_L2 = { - ops = [@{typ "'a2 * 'a2::var FType"}], + ops = [@{typ "('a1, 'a2) L2"}], + bd = @{term natLeq}, + var_class = @{class var}, leader = 0, - frees = [@{typ "'a2::var"}], + frees = [@{typ 'a1}, @{typ "'a2"}], 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"}] + BMV_Monad_Def.frees_of_bmv_monad id_bmv ~~ [@{typ "'a1"}] + )) id_bmv, + BMV_Monad_Def.morph_bmv_monad ( + MRBNF_Util.subst_typ_morphism ( + BMV_Monad_Def.frees_of_bmv_monad id_bmv ~~ [@{typ "'a2"}] )) id_bmv, BMV_Monad_Def.morph_bmv_monad ( MRBNF_Util.subst_typ_morphism ( @@ -433,9 +445,13 @@ val model_L2 = { )) FType_bmv ], Maps = [NONE], - Injs = [([], [(@{term "id :: 'a2::var \ 'a2"}, 1), (@{term "TyVar :: 'a2::var \ 'a2 FType"}, 2)])], - Sbs = [@{term "Sb_L2 :: _ \ _ \ _ \ ('a2, 'a2::var) L2"}], - Vrs = [[@{term "Vrs_L2_1 :: ('a2, 'a2::var) L2 \ _"}, @{term "Vrs_L2_2 :: ('a2, 'a2::var) L2 \ _"}]], + Injs = [[@{term "id :: 'a1 \ 'a1"}, @{term "id :: 'a2 \ 'a2"}, @{term "TyVar :: 'a2::var \ 'a2 FType"}]], + Sbs = [@{term "Sb_L2 :: _ \ _ \ _ \ _ \ ('a1, 'a2::var) L2"}], + Vrs = [[ + [SOME @{term "Vrs_L2_1 :: ('a1, 'a2::var) L2 \ _"}, NONE], + [NONE, SOME @{term "Vrs_L2_2 :: ('a1, 'a2::var) L2 \ _"}], + [NONE, SOME @{term "Vrs_L2_3 :: ('a1, 'a2::var) L2 \ _"}] + ]], tacs = [{ Sb_Inj = fn ctxt => EVERY1 [ K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Sb_Inj_FType id_apply prod.map_id0}), @@ -451,21 +467,26 @@ val model_L2 = { ], Vrs_Injs = [], Vrs_Sbs = [ - fn ctxt => EVERY1 [ + [SOME (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 [ + ]), NONE], + [NONE, SOME (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 insert_is_Un[symmetric] UN_insert UN_empty Un_empty_right id_apply}), + resolve_tac ctxt [refl] + ])], + [NONE, SOME (fn ctxt => EVERY1 [ + K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_3_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\_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}), + K (Local_Defs.unfold0_tac ctxt @{thms Sb_L2_def Vrs_L2_1_def Vrs_L2_2_def Vrs_L2_3_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}, @@ -474,87 +495,32 @@ val model_L2 = { 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\_FType_tvsubst_FType_def TyVar_def[symmetric]]}, - REPEAT_DETERM o assume_tac ctxt, - rotate_tac ~3, + resolve_tac ctxt @{thms prod.map_cong0}, + eresolve_tac ctxt @{thms Basic_BNFs.fsts.cases}, + hyp_subst_tac ctxt, + rotate_tac ~2, dresolve_tac ctxt @{thms meta_spec}, dresolve_tac ctxt @{thms meta_mp}, - hyp_subst_tac ctxt, + resolve_tac ctxt @{thms insertI1}, assume_tac ctxt, - assume_tac ctxt - ] - } : (Proof.context -> tactic) BMV_Monad_Def.bmv_monad_axioms] -} : BMV_Monad_Def.bmv_monad_model; -\ -ML \ -val L2_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L2 @{context} -\ *) -ML \ -val model_L2 = { - ops = [@{typ "'a1 * 'a2::var FType"}], - bd = @{term natLeq}, - var_class = @{class var}, - leader = 0, - frees = [@{typ 'a1}, @{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 "'a1"}] - )) 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 :: 'a1 \ 'a1"}, @{term "TyVar :: 'a2::var \ 'a2 FType"}]], - Sbs = [@{term "Sb_L2 :: _ \ _ \ _ \ ('a1, 'a2::var) L2"}], - Vrs = [[@{term "Vrs_L2_1 :: ('a1, 'a2::var) L2 \ _"}, @{term "Vrs_L2_2 :: ('a1, 'a2::var) L2 \ _"}]], - 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\_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\_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}), + hyp_subst_tac ctxt, + eresolve_tac ctxt @{thms Basic_BNFs.snds.cases}, resolve_tac ctxt @{thms prod.map_cong0}, eresolve_tac ctxt @{thms Basic_BNFs.fsts.cases}, + hyp_subst_tac ctxt, + rotate_tac ~2, dresolve_tac ctxt @{thms meta_spec}, dresolve_tac ctxt @{thms meta_mp}, + resolve_tac ctxt @{thms insertI2}, resolve_tac ctxt @{thms singletonI}, - hyp_subst_tac ctxt, assume_tac ctxt, eresolve_tac ctxt @{thms Basic_BNFs.snds.cases}, + hyp_subst_tac ctxt, resolve_tac ctxt @{thms Sb_cong_FType[unfolded SSupp_FType_def tvVVr_tvsubst_FType_def[unfolded comp_def] tv\_FType_tvsubst_FType_def TyVar_def[symmetric]]}, REPEAT_DETERM o assume_tac ctxt, - rotate_tac ~3, + rotate_tac ~2, dresolve_tac ctxt @{thms meta_spec}, dresolve_tac ctxt @{thms meta_mp}, - hyp_subst_tac ctxt, assume_tac ctxt, assume_tac ctxt ]