diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML index 0569b560..6a33ac09 100644 --- a/Tools/mrbnf_sugar.ML +++ b/Tools/mrbnf_sugar.ML @@ -79,7 +79,7 @@ fun create_binder_type (fp : MRBNF_Util.fp_kind) (spec : spec) lthy = val ((mrsbnf, (Ds, absinfo)), lthy) = MRSBNF_Comp.seal_mrsbnf I (bmv_unfolds @ BMV_Monad_Def.unfolds_of_bmv_monad (MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf), snd accum) (Binding.name pre_name) (#vars spec) tys mrsbnf NONE lthy; - + val mrbnf = hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf); val FVars_names = case #set_bs spec of @@ -1146,7 +1146,7 @@ fun create_binder_datatype co (spec : spec) lthy = (single o HOLogic.mk_Trueprop o mk_bij) bounds mapx tac end; - val (lthy, tvsubst_opt) = if not (null (map_filter I (#etas tvsubst_model))) andalso not co then + val (tvsubst_opt, lthy) = if not (null (map_filter I (#etas tvsubst_model))) andalso not co then let val recursor_result = #recursor_result (the vvsubst_res_opt); val rec_mrbnf = #rec_mrbnf (the vvsubst_res_opt); @@ -1257,8 +1257,32 @@ fun create_binder_datatype co (spec : spec) lthy = in map (Local_Defs.unfold0 lthy bmv_unfolds) ( mk_map_simps lthy false true Sbs plives (fs @ rhos) mk_supp_bound mk_imsupp (K []) [] (#tvsubst tvsubst_res) tac ) end; - in (lthy, SOME (tvsubst_res, tvsubst_simps)) end - else (lthy, NONE); + + in (SOME (tvsubst_res, tvsubst_simps), lthy) end + else (NONE, lthy); + + val (tvsubst1_opt, lthy) = (case tvsubst_opt of + NONE => (NONE, lthy) + | SOME tvsubst => + let + (* prepare spec (we need the original tv names for RVrs) *) + val ctor_Ts = map snd (#ctors spec); + + fun is_RVr (NT, x) = + let + val (Inj_count, arity) = fold (fn Ts => fn (cnt, arity) => + (if member (op=) Ts (TFree NT) + then (1 + cnt, arity orelse length Ts > 1) + else (cnt, arity)) + ) ctor_Ts (0, false); + in x = Free_Var andalso (Inj_count <> 1 orelse arity) end; + + val RVr_Ns = filter is_RVr (#vars spec) + |> map ((fn N => String.extract (N, 1, NONE)) o fst o fst); + in + TVSubst.create_tvsubst1_of_result (#tvsubst_b spec, RVr_Ns) tvsubst lthy + |> apfst SOME + end); val simp = @{attributes [simp]} val induct_attrib = Attrib.internal Position.none (K (Induct.induct_type (fst (dest_Type qT)))) @@ -1339,7 +1363,9 @@ fun create_binder_datatype co (spec : spec) lthy = ("IImsupp_permute_commute", #IImsupp_permute_commutes res, []), ("IImsupp_Diff", #IImsupp_Diffs res, []), ("tvsubst_permute", [#tvsubst_permute res], []) - ]) tvsubst_opt)) + ]) tvsubst_opt) @ the_default [] (Option.map (map (fn (N, tvsubst1_simps) => + (N, tvsubst1_simps, simp) + )) tvsubst1_opt)) |> filter_out (null o #2) |> (map (fn (thmN, thms, attrs) => ((Binding.qualify true (Binding.name_of (#fp_b spec)) (Binding.name thmN), attrs), [(thms, [])]) diff --git a/Tools/tvsubst.ML b/Tools/tvsubst.ML index 6b7d2c73..311011d2 100644 --- a/Tools/tvsubst.ML +++ b/Tools/tvsubst.ML @@ -29,6 +29,9 @@ sig -> MRSBNF_Def.mrsbnf -> MRBNF_Def.mrbnf -> thm -> thm -> thm list -> binding -> (Proof.context -> tactic) eta_model option list -> string -> local_theory -> tvsubst_result * local_theory + + val create_tvsubst1_of_result: binding * string list -> tvsubst_result * thm list -> local_theory + -> (string * thm list) list * local_theory end structure TVSubst : TVSUBST = @@ -2495,4 +2498,159 @@ fun create_tvsubst_of_mrsbnf qualify fp_res mrsbnf rec_mrbnf vvsubst_ctor map_pe }: tvsubst_result; in (result, lthy) end; + +local + fun mk_Free N T lthy' = mk_Frees N [T] lthy' |>> the_single; + + fun drop_at j xs = (take j xs, drop (j+1) xs); + + (* |Inj x| (Inj, x) *) + fun dest_set_bd_UNIV (Trueprop $ (member $ (Pair $ (card_of $ (set $ x)) $ card_of_top) $ ordLess)) = (set, x) + | dest_set_bd_UNIV t = raise TERM("dest_set_bd_UNIV", [t]) +in +fun create_tvsubst1_of_result (tvsubst_b, RVr_Ns) (result, simps) lthy = + let + val Sb as Const (_, Sb_T) = #tvsubst result; + + val mrsbnf = #mrsbnf result; + val mrbnf = hd (MRSBNF_Def.mrbnfs_of_mrsbnf mrsbnf); + + val bmv = MRSBNF_Def.bmv_monad_of_mrsbnf mrsbnf; + + val RVrs = hd (BMV_Monad_Def.RVrs_of_bmv_monad bmv); + val Injs = hd (BMV_Monad_Def.Injs_of_bmv_monad bmv); + + val n = length RVrs + length Injs; + + val (delta_Ts, _) = fastype_of Sb |> binder_types |> split_last; + val (id_Ts, Inj_Ts) = partition (op= o dest_funT) delta_Ts; + + (* map Set to fact "|Set ?x| map (`(Thm.prop_of #> dest_set_bd_UNIV #> fst #> dest_Const_name)); + + (* construct the identities for RVrs and their respective unary Sb bindings *) + val ids = map2 (fn T => fn N => (N, Const ("Fun.id", T))) + id_Ts (take (length id_Ts) RVr_Ns); + + (* construct the Injection ctors and their respective bindings *) + val Injs = map2 (fn T => dest_Const #> (fn (N, _) => + (Long_Name.base_name N, Const (N, T))) + ) Inj_Ts Injs; + + (* all together *) + val (Ns, trms) = split_list (ids @ Injs); + + (* accumulate simplification theorems by index, name, and term: *) + fun alg k N trm (acc, lthy) = + let + val (_, lthy) = Local_Theory.begin_nested lthy; + val b = Binding.map_name (fn str => str ^ "_" ^ N) tvsubst_b; + + (* "pure" terms surrounding the current delta term *) + val (pre, post) = drop_at k trms; + + val (v_T, t_T) = fastype_of trm |> dest_funT; + val (t, (v, names_lthy)) = mk_Free "t" t_T lthy ||> mk_Free "v" v_T; + + (* construct unary Sb definition: subst id... X{k}(v := t) Inj... *) + val upd = Quickcheck_Common.mk_fun_upd v_T t_T (v, t) trm; + + val deltas = pre @ upd :: post; + val cdeltas = map (SOME o Thm.cterm_of lthy) deltas; + + val def = list_comb (Sb, deltas) + |> Term.absfree (dest_Free t) + |> Term.absfree (dest_Free v); + + val ((_, (_, def_thm)), lthy) = Local_Theory.define + ((b, NoSyn), ((Thm.def_binding b, []), def)) lthy; + + (* expand definition thm to make the Local_Defs.fold go through *) + val def_expanded = def_thm + RS @{thm meta_fun_cong} (* v *) + RS @{thm meta_fun_cong} (* t *) + RS @{thm meta_fun_cong} (* x *); + + (* map trivial premise to theorem that discharge it *) + fun trivial_fact prem = case prem |> HOLogic.dest_Trueprop of + (* |?A| + (case A of + (* {} *) + Const (@{const_name "bot"}, _) => @{thm emp_bound} + (* supp (id(v := t)) *) + | Const (@{const_name "supp"}, _) $ + (Const (@{const_name "fun_upd"}, _) $ Const (@{const_name "id"}, _) $ _ $ _) => + @{thm supp_fun_upd_var} + (* SSupp Inj (Inj(v := t)) *) + | Const (@{const_name "SSupp"}, _) $ _ $ (Const (@{const_name "fun_upd"}, _) $ _ $ _ $ _) => + @{thm SSupp_fun_upd_Inj_bound} + (* IImsupp Inj ?Set (Inj(v := t) *) + | Const (@{const_name "IImsupp"}, _) $ _ $ Set $ + (Const (@{const_name "fun_upd"}, _) $ _ $ _ $ _) => + the (AList.lookup op= set_bd_UNIV_tab (dest_Const_name Set)) RS + @{thm IImsupp_fun_upd_Inj_bound} + (* fallback (skip) *) + | _ => @{thm asm_rl} + ) + (* ?x \ {} *) + | Const (@{const_name "Not"}, _) $ (Const (@{const_name "Set.member"}, _) $ + _ $ Const (@{const_name "bot"}, _)) => + @{thm empty_iff[symmetric, unfolded simp_thms(13)]} + (* fallback (skip) *) + | _ => @{thm asm_rl}; + + fun discharge_trivial simp_thm = + let + (* discharge premises (reverse order in case we don't fully resolve it) *) + val iprems = Thm.prop_of simp_thm + |> Logic.strip_imp_prems + |> map_index (fn (i, prem) => (i+1, trivial_fact prem)); + in fold_rev (fn (i,P) => fn thm => P RSN (i, thm)) iprems simp_thm end; + + (* get rid of all SSupp, IImssupp, SSupp, and imsupp mentions: *) + val tidy = + (* unfold "x \ {IImssupp,SSupp,imsupp} .." \ "t = Var v \ ..." *) + Local_Defs.unfold lthy @{thms not_in_SSupp_fun_upd_Inj_iff not_in_IImsupp_fun_upd_Inj_iff not_in_imsupp_fun_upd_id_iff} + (* rewrite \ t = Var v \ ?A1; t = Var v \ ?A2 ... \ \ \ t = Var \ (?A1 \ ...); ... \ *) + #> Local_Defs.unfold lthy @{thms atomize_conjL} + (* tidy up a bit *) + #> Local_Defs.unfold lthy @{thms int_SSupp_fun_upd_iff int_imsupp_id_fun_upd_iff int_IImsupp_fun_upd_iff Int_empty_right simp_thms(6) simp_thms(21,22) True_implies_equals} + #> ( + let + fun RS_tac thm = TRY (fn thm' => Seq.single (thm RS thm') handle THM _ => Seq.empty) + + val tac = EVERY + [REPEAT (CHANGED (Local_Defs.fold_tac lthy @{thms conj_assoc disj_conj_distribL})), + Local_Defs.unfold_tac lthy @{thms conj_assoc}, + RS_tac @{thm disjI2}, + RS_tac @{thm conjI}] + in REPEAT (CHANGED tac) #> Seq.hd end + ); + + (* adapt the simp theorems to the unary case: *) + val adapt = map ( + (* specialize the simps with unary Sb *) + Drule.infer_instantiate' lthy cdeltas + #> Local_Defs.fold lthy [def_expanded] + (* unfold trivial/unary supports *) + #> Local_Defs.unfold lthy @{thms SSupp_Inj IImsupp_Inj supp_id imsupp_id} + (* discharge premises like "|{}| discharge_trivial + #> tidy + #> singleton (Variable.export names_lthy lthy) + ); + val (lthy, old_lthy) = `Local_Theory.end_nested lthy; + val phi = Proof_Context.export_morphism old_lthy lthy; + + in (("subst_" ^ N, adapt simps |> Morphism.fact phi) :: acc, lthy) end; + + in @{fold 3} alg (0 upto n-1) Ns trms ([], lthy) end; +end; + end diff --git a/tests/Regression_Tests.thy b/tests/Regression_Tests.thy index 5886d146..959aa0b0 100644 --- a/tests/Regression_Tests.thy +++ b/tests/Regression_Tests.thy @@ -7,6 +7,9 @@ binder_datatype 'a trm = Var 'a | Abs x::'a t::"'a trm" binds x in t +thm trm.subst +thm trm.subst_Var + (* #69 *) binder_datatype 'a LLC = Var 'a diff --git a/thys/Classes.thy b/thys/Classes.thy index 3b253f13..49ebf97c 100644 --- a/thys/Classes.thy +++ b/thys/Classes.thy @@ -114,6 +114,7 @@ lemma IImsupp_Inj_comp_bound1: "inj Inj \ |supp (f::'a::var \a. Vrs (Inj a) = {}) \ |IImsupp Inj Vrs (Inj \ f)| |SSupp Inj f| x. |Vrs x| |IImsupp Inj Vrs (Inj(x := t))| IImsupp lemma notin_SSupp: "a \ SSupp Inj f \ f a = Inj a" unfolding SSupp_def by blast +lemma not_in_SSupp_fun_upd_Inj_iff: + \u \ SSupp Inj (Inj(v := t)) \ t = Inj v \ u \ v\ + by (simp add: SSupp_def) + +lemma not_in_IImsupp_fun_upd_Inj_iff: + \u \ IImsupp Inj Set (Inj(v := t)) \ t = Inj v \ u \ Set t\ + by (simp add: IImsupp_def SSupp_def) + +lemma not_in_imsupp_fun_upd_id_iff: + \u \ imsupp (id(v := t)) \ t = v \ (u \ v \ u \ t)\ + by (auto simp: imsupp_def supp_def) + +lemma int_SSupp_fun_upd_iff: + \A \ SSupp Inj (Inj(v := t)) = {} \ t = Inj v \ v \ A\ + by (auto simp: SSupp_def) + +lemma int_imsupp_id_fun_upd_iff: + \A \ imsupp (id(v := t)) = {} \ t = v \ v \ A \ t \ A\ + by (simp add: imsupp_id_fun_upd) + +lemma int_IImsupp_fun_upd_iff: + \A \ IImsupp Inj Vrs (Inj(v := t)) = {} \ + t = Inj v \ A \ Vrs t = {}\ + by (simp add: IImsupp_def SSupp_def) + lemma IImsupp_chain1: assumes "\a. Vrs2 (Inj2 a) = {a}" "\1 = \' \ \1 = \2" shows "(\x\SSupp Inj2 \1. \x\Vrs2 (\' x). Vrs2 (\2 x)) \ IImsupp Inj2 Vrs2 \2 \ IImsupp Inj2 Vrs2 \'"