diff --git a/Tools/binder_induction.ML b/Tools/binder_induction.ML index 329707c..267fb4d 100644 --- a/Tools/binder_induction.ML +++ b/Tools/binder_induction.ML @@ -124,14 +124,6 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking | NONE => error "Automatic detection of induction rule is not supported yet, please specify with rule:" ); - fun dest_ordLess t = - let val t' = case HOLogic.dest_mem t of - (t', Const (@{const_name ordLess}, _)) => t' - | _ => raise TERM ("dest_ordLess", [t]) - in HOLogic.dest_prod t' end - fun dest_card_of (Const (@{const_name card_of}, _) $ t) = t - | dest_card_of t = raise TERM ("dest_card_of", [t]) - fun strip_all (Const (@{const_name HOL.All}, _) $ t) = (case t of Abs (x, T, t) => let val a = Free (x, T) in apfst (curry (op::) a) (strip_all (Term.subst_bound (a, t))) end @@ -150,8 +142,8 @@ fun gen_binder_context_tactic mod_cases simp def_insts arbitrary avoiding taking val vars_prems = map (try ( HOLogic.dest_Trueprop #> snd o strip_all - #> fst o dest_ordLess - #> dest_card_of + #> fst o MRBNF_Util.dest_ordLess + #> MRBNF_Util.dest_card_of #> fst o Term.strip_comb #> snd o Term.dest_Var #> HOLogic.dest_setT o range_type diff --git a/Tools/bmv_monad_def.ML b/Tools/bmv_monad_def.ML index b3499e7..a218d0b 100644 --- a/Tools/bmv_monad_def.ML +++ b/Tools/bmv_monad_def.ML @@ -5,7 +5,7 @@ signature BMV_MONAD_DEF = sig type 'a bmv_monad_axioms = { Sb_Inj: 'a, Sb_comp_Injs: 'a list, - Sb_comp: 'a, (* require typeclass on free vars to bound *) + Sb_comp: 'a, Sb_cong: 'a, (* TODO: Add Vrs_bd axiom *) Vrs_Injs: 'a list, (* TODO: One per Inj AND var kind *) @@ -15,6 +15,8 @@ signature BMV_MONAD_DEF = sig type bmv_monad_model = { ops: typ list, + bd: term, + var_class: class, bmv_ops: bmv_monad list, frees: typ list, lives: typ list, @@ -27,6 +29,8 @@ signature BMV_MONAD_DEF = sig } val ops_of_bmv_monad: bmv_monad -> typ list; + val bd_of_bmv_monad: bmv_monad -> term; + val var_class_of_bmv_monad: bmv_monad -> class; val leader_of_bmv_monad: bmv_monad -> int; val frees_of_bmv_monad: bmv_monad -> typ list; val lives_of_bmv_monad: bmv_monad -> typ list; @@ -38,9 +42,9 @@ signature BMV_MONAD_DEF = sig val morph_bmv_monad: morphism -> bmv_monad -> bmv_monad; val bmv_monad_def: BNF_Def.inline_policy -> (Proof.context -> BNF_Def.fact_policy) - -> (binding -> binding) -> bmv_monad_model -> local_theory -> bmv_monad + -> (binding -> binding) -> bmv_monad_model -> local_theory -> bmv_monad * local_theory - val compose_bmv_monad: (binding -> binding) -> bmv_monad -> bmv_monad list -> local_theory -> bmv_monad + val compose_bmv_monad: (binding -> binding) -> bmv_monad -> bmv_monad list -> local_theory -> bmv_monad * local_theory end structure BMV_Monad_Def : BMV_MONAD_DEF = struct @@ -67,9 +71,10 @@ 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, + bd: term, + var_class: class, leader: int, frees: typ list, lives: typ list, @@ -80,11 +85,29 @@ datatype bmv_monad = BMV of { axioms: thm bmv_monad_axioms list } +fun morph_bmv_monad phi (BMV { + ops, bd, var_class, leader, frees, lives, Injs, Sbs, Maps, Vrs, axioms +}) = BMV { + ops = map (Morphism.typ phi) ops, + bd = Morphism.term phi bd, + leader = leader, + var_class = var_class, + frees = map (Morphism.typ phi) frees, + lives = map (Morphism.typ phi) lives, + 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, + axioms = map (morph_bmv_axioms phi) axioms +} + datatype supported_functor = Supported_Functor (* TODO *) fun Rep_bmv (BMV x) = x val ops_of_bmv_monad = #ops o Rep_bmv +val bd_of_bmv_monad = #bd o Rep_bmv +val var_class_of_bmv_monad = #var_class o Rep_bmv; val leader_of_bmv_monad = #leader o Rep_bmv val frees_of_bmv_monad = #frees o Rep_bmv val lives_of_bmv_monad = #lives o Rep_bmv @@ -95,6 +118,8 @@ val Vrs_of_bmv_monad = #Vrs o Rep_bmv type bmv_monad_model = { ops: typ list, + bd: term, + var_class: class, frees: typ list, lives: typ list, bmv_ops: bmv_monad list, @@ -106,19 +131,20 @@ type bmv_monad_model = { tacs: (Proof.context -> tactic) bmv_monad_axioms list } -fun morph_bmv_monad phi (BMV { - ops, leader, frees, lives, Injs, Sbs, Maps, Vrs, axioms -}) = BMV { +fun morph_bmv_monad_model phi { ops, bd, var_class, frees, lives, bmv_ops, leader, Injs, Sbs, Maps, Vrs, tacs } = { ops = map (Morphism.typ phi) ops, - leader = leader, + bd = Morphism.term phi bd, + var_class = var_class, frees = map (Morphism.typ phi) frees, lives = map (Morphism.typ phi) lives, + bmv_ops = map (morph_bmv_monad phi) bmv_ops, + leader = leader, 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, - axioms = map (morph_bmv_axioms phi) axioms -} + tacs = tacs +} : bmv_monad_model; fun prove_axioms (model: bmv_monad_model) lthy = let @@ -215,10 +241,23 @@ fun prove_axioms (model: bmv_monad_model) lthy = fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lthy = let + val _ = let + val var_large = MRBNF_Def.get_class_assumption [#var_class model] "large" lthy; + val bd' = snd (dest_comb (dest_card_of ( + 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); + val model = morph_bmv_monad_model (MRBNF_Util.subst_typ_morphism (#frees model ~~ frees)) model; + val axioms = prove_axioms model lthy; val bmv = BMV { ops = #ops model @ maps (#ops o Rep_bmv) (#bmv_ops model), + bd = #bd model, + var_class = #var_class model, leader = #leader model, frees = #frees model, lives = #lives model, @@ -228,7 +267,7 @@ fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lth 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 + in (bmv, lthy) end (* Cleanup: Throw away op iff any: - not the leader diff --git a/Tools/mrbnf_def.ML b/Tools/mrbnf_def.ML index 21d2155..c582791 100644 --- a/Tools/mrbnf_def.ML +++ b/Tools/mrbnf_def.ML @@ -255,6 +255,8 @@ sig val mrbnf_cmd: ((((((((binding * string) * string) * (var_type * string) list) * string) * string list) * string option) * string option) * string option) * (Proof.context -> Plugin_Name.filter) -> Proof.context -> Proof.state + + val get_class_assumption: string list -> string -> Proof.context -> thm; end; structure MRBNF_Def : MRBNF_DEF = @@ -1655,14 +1657,13 @@ fun define_mrbnf_consts const_policy fact_policy internal Ds_opt classes_opt map in bs ~~ set_rhss end; val bd_bind_def = (fn () => def_qualify (mk_prefix_binding bdN), bd_rhs); - val ((((mrbnf_map_term, raw_map_def), + val (((mrbnf_map_term, raw_map_def), (mrbnf_set_terms, raw_set_defs)), - _ (* (mrbnf_bd_term, raw_bd_def) *)), (lthy, lthy_old)) = + (lthy, lthy_old)) = no_defs_lthy |> Local_Theory.begin_nested |> snd |> maybe_define true map_bind_def ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs - ||>> (fn lthy => ((bd_rhs, Drule.reflexive_thm), lthy)) (* maybe_define true bd_bind_def*) ||> `Local_Theory.end_nested; val phi = Proof_Context.export_morphism lthy_old lthy; diff --git a/Tools/mrbnf_util.ML b/Tools/mrbnf_util.ML index e9c43ea..953ae7d 100644 --- a/Tools/mrbnf_util.ML +++ b/Tools/mrbnf_util.ML @@ -35,6 +35,10 @@ sig val mk_ex: string * typ -> term -> term; val mk_insert: term -> term -> term; + val dest_ordLess: term -> term * term; + val dest_ordLeq: term -> term * term; + val dest_card_of: term -> term; + val strip_ex: term -> (string * typ) list * term val mk_conj_thms: int -> local_theory -> thm * thm @@ -99,6 +103,19 @@ fun subst_typ_morphism subst = Morphism.morphism "subst_typ" { typ = [K (Term.typ_subst_atomic subst)] }; +fun dest_ordLess t = + let val t' = case HOLogic.dest_mem t of + (t', Const (@{const_name ordLess}, _)) => t' + | _ => raise TERM ("dest_ordLess", [t]) + in HOLogic.dest_prod t' end +fun dest_ordLeq t = + let val t' = case HOLogic.dest_mem t of + (t', Const (@{const_name ordLeq}, _)) => t' + | _ => raise TERM ("dest_ordLeq", [t]) + in HOLogic.dest_prod t' end +fun dest_card_of (Const (@{const_name card_of}, _) $ t) = t + | dest_card_of t = raise TERM ("dest_card_of", [t]) + fun mk_def_t_syn syn public b qualify name n rhs lthy = let val b' = qualify (Binding.name name); diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy index acd354f..0839f5e 100644 --- a/operations/BMV_Monad.thy +++ b/operations/BMV_Monad.thy @@ -99,6 +99,8 @@ Multithreading.parallel_proofs := 0 ML \ val model_FType = { ops = [@{typ "'a::var FType"}], + bd = @{term natLeq}, + var_class = @{class var}, leader = 0, frees = [@{typ "'a::var"}], lives = [], @@ -136,7 +138,7 @@ val model_FType = { \ ML \ -val FType_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_FType @{context} +val FType_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_FType @{context}) \ @@ -234,6 +236,8 @@ declare [[ML_print_depth=10000]] ML \ val model_ID = { ops = [@{typ "'a"}], + bd = @{term natLeq}, + var_class = @{class var}, leader = 0, frees = [@{typ "'a"}], lives = [], @@ -271,12 +275,14 @@ val model_ID = { } : BMV_Monad_Def.bmv_monad_model; \ ML \ -val id_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_ID @{context} +val id_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_ID @{context}) \ ML \ val model_L = { ops = [@{typ "'a1 * 'a1 * ('c1 + 'c2)"}], + bd = @{term natLeq}, + var_class = @{class var}, leader = 0, frees = [@{typ "'a1"}, @{typ "'a2"}], lives = [@{typ "'c1"}, @{typ "'c2"}], @@ -335,12 +341,14 @@ val model_L = { } : BMV_Monad_Def.bmv_monad_model; \ ML \ -val L_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L @{context} +val L_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L @{context}) \ ML \ val model_L1 = { ops = [@{typ "'a1 * 'a2"}], + bd = @{term natLeq}, + var_class = @{class var}, leader = 0, frees = [@{typ "'a1"}, @{typ "'a2"}], lives = [], @@ -405,7 +413,7 @@ val model_L1 = { } : BMV_Monad_Def.bmv_monad_model; \ ML \ -val L1_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L1 @{context} +val L1_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L1 @{context}) \ (* ML \ @@ -484,6 +492,8 @@ val L2_bmv = BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_No 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 = [], @@ -552,11 +562,9 @@ val model_L2 = { } : 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} +val L2_bmv = fst (BMV_Monad_Def.bmv_monad_def BNF_Def.Smart_Inline (K BNF_Def.Dont_Note) I model_L2 @{context}) \ -ML \ -val x = BMV_Monad_Def.compose_bmv_monad I L_bmv [L1_bmv, L2_bmv] @{context} -\ +local_setup \snd o BMV_Monad_Def.compose_bmv_monad I L_bmv [L1_bmv, L2_bmv]\ end \ No newline at end of file