From 3c5ee89c5af203b4b3650a42441915863a95a948 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Thu, 21 Nov 2024 22:18:20 +0000 Subject: [PATCH] Replace custom ML for commitment type --- Tools/binder_inductive.ML | 3 - Tools/mrbnf_sugar.ML | 12 +- Tools/mrbnf_util.ML | 4 + Tools/parser.ML | 4 +- thys/Pi_Calculus/Commitment.thy | 241 +++------------------- thys/Pi_Calculus/Pi_Transition_Common.thy | 2 +- thys/Pi_Calculus/Pi_cong.thy | 2 +- 7 files changed, 47 insertions(+), 221 deletions(-) diff --git a/Tools/binder_inductive.ML b/Tools/binder_inductive.ML index d1d36b0..af85c04 100644 --- a/Tools/binder_inductive.ML +++ b/Tools/binder_inductive.ML @@ -16,9 +16,6 @@ fun long_name ctxt name = fun collapse (Inl x) = x | collapse (Inr x) = x -fun mk_insert x S = - Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S; - fun binder_inductive_cmd ((pred_name, binds_opt), perms_supps) no_defs_lthy = let val binds = the_default [] binds_opt; diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML index e5030da..bf89f7d 100644 --- a/Tools/mrbnf_sugar.ML +++ b/Tools/mrbnf_sugar.ML @@ -370,7 +370,15 @@ fun create_binder_datatype (spec : spec) lthy = | NONE => FVars $ t) | t => if member (op=) rec_vars (HOLogic.dest_setT (fastype_of t)) then mk_UNION t FVars else t ) (flat (map_filter I (map2 (fn T => fn x => get_sets T vars x) tys xs))); - val sets = get_set (free::subtract (op=) rec_bounds rec_vars) + + val sets = get_set (free::subtract (op=) rec_bounds rec_vars); + fun incorporate xs = case xs of [] => I | (x::_) => cons (fold_rev mk_insert xs (mk_bot (fastype_of x))); + val (xtra, sets) = fold_rev ( + fn Const (@{const_name insert}, _) $ t $ Const (@{const_name bot}, _) => (fn (xs, acc) => (t::xs, acc)) + | t => fn (xs, acc) => ([], incorporate xs (t::acc)) + ) sets ([], []); + val sets = incorporate xtra sets; + val brec_sets = get_set (the_default [] (Option.map single bfree_opt) @ rec_bounds) val bsets = map (fn (t as Free _) => mk_singleton t | t => t) ( flat (map_filter I (map2 (fn T => fn x => get_sets T [bound] x) tys xs)) @@ -396,7 +404,7 @@ fun create_binder_datatype (spec : spec) lthy = | _ => foldl1 MRBNF_Util.mk_Un sets )); val thms = @{thms sum.set_map prod.set_map comp_def UN_empty UN_empty2 Un_empty_left Un_empty_right - UN_singleton UN_single sum_set_simps prod_set_simps Diff_empty UN_Un + UN_singleton UN_single sum_set_simps prod_set_simps Diff_empty UN_Un Un_assoc[symmetric] insert_is_Un[of _ "{_}"] }; in (bset_opt, Goal.prove_sorry lthy (names xs) [] goal (fn {context=ctxt, ...} => EVERY1 [ K (Local_Defs.unfold0_tac ctxt ( diff --git a/Tools/mrbnf_util.ML b/Tools/mrbnf_util.ML index 1eb1b4a..4491a49 100644 --- a/Tools/mrbnf_util.ML +++ b/Tools/mrbnf_util.ML @@ -30,6 +30,7 @@ sig val mk_minus: term * term -> term; val mk_all: string * typ -> term -> term; val mk_ex: string * typ -> term -> term; + val mk_insert: term -> term -> term; val strip_ex: term -> (string * typ) list * term @@ -84,6 +85,9 @@ val mk_minus = HOLogic.mk_binop @{const_name minus}; fun mk_all (x, T) t = HOLogic.mk_all (x, T, t); fun mk_ex (x, T) t = HOLogic.mk_exists (x, T, t); +fun mk_insert x S = + Const (@{const_name Set.insert}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S; + fun mk_def_t_syn syn public b qualify name n rhs lthy = let val b' = qualify (Binding.name name); diff --git a/Tools/parser.ML b/Tools/parser.ML index 66bf580..1fe4647 100644 --- a/Tools/parser.ML +++ b/Tools/parser.ML @@ -64,9 +64,9 @@ fun create_ctor_spec T_names ((((sel, name), xs), mixfix), binds) (lthy, params) val names = maps (find_names o YXML.content_of o snd o snd) xs; fun mk_typedecl name = Typedecl.basic_typedecl {final = true} (Binding.name name, 0, NoSyn) - val (fake_names, lthy) = fold_map mk_typedecl names lthy; + val (fake_names, names_lthy) = fold_map mk_typedecl names lthy; - val (sels, Ts) = split_list (map (apsnd (Syntax.read_typ lthy) o snd) xs); + val (sels, Ts) = split_list (map (apsnd (Syntax.read_typ names_lthy) o snd) xs); fun fold_map_typ f (Type (n, Ts)) x = let val (Ts', x') = fold_map (fold_map_typ f) Ts x diff --git a/thys/Pi_Calculus/Commitment.thy b/thys/Pi_Calculus/Commitment.thy index ba681c5..12ac785 100644 --- a/thys/Pi_Calculus/Commitment.thy +++ b/thys/Pi_Calculus/Commitment.thy @@ -2,7 +2,7 @@ theory Commitment imports Pi "Prelim.Curry_LFP" "Binders.Generic_Barendregt_Enhanced_Rule_Induction" begin -local_setup \fn lthy => +(*local_setup \fn lthy => let val name1 = "commit_internal" val name2 = "commit" @@ -41,27 +41,21 @@ let ((name1, mrbnf1), 1), ((name2, mrbnf2), 1) ] rel lthy; in lthy end -\ +\*) print_theorems +binder_datatype 'var commit = + Finp 'var 'var "'var term" + | Fout 'var 'var "'var term" + | Bout 'var x::'var "(t::'var) term" binds x in t + | Tau "'var term" + | Binp 'var x::'var "(t::'var) term" binds x in t (* Monomorphization: *) type_synonym cmt = "var commit" instance var :: var_commit_pre by standard -instance var :: var_commit_internal_pre by standard - -definition Finp :: "var \ var \ trm \ cmt" where - "Finp x y t \ commit_ctor (Abs_commit_pre (Inl (x, y, t)))" -definition Fout :: "var \ var \ trm \ cmt" where - "Fout x y t \ commit_ctor (Abs_commit_pre (Inr (Inl (x, y, t))))" -definition Bout :: "var \ var \ trm \ cmt" where - "Bout x y t \ commit_ctor (Abs_commit_pre (Inr (Inr (Inl (x, y, commit_internal_ctor (Abs_commit_internal_pre t))))))" -definition Tau :: "trm \ cmt" where - "Tau t \ commit_ctor (Abs_commit_pre (Inr (Inr (Inr (Inl t)))))" -definition Binp :: "var \ var \ trm \ cmt" where - "Binp x y t \ commit_ctor (Abs_commit_pre (Inr (Inr (Inr (Inr (x, y, commit_internal_ctor (Abs_commit_internal_pre t)))))))" - -lemmas toUnfold = set1_commit_internal_pre_def + +lemmas toUnfold = UN_empty UN_empty2 UN_single Un_empty_left Un_empty_right comp_def empty_Diff map_prod_simp prod_set_simps @@ -69,181 +63,40 @@ lemmas toUnfold = set1_commit_internal_pre_def Sup_empty cSup_singleton (* *) Abs_commit_pre_inverse[OF UNIV_I] - set1_commit_pre_def set2_commit_pre_def set4_commit_pre_def set3_commit_pre_def - Abs_commit_internal_pre_inverse[OF UNIV_I] - set1_commit_internal_pre_def set2_commit_internal_pre_def - set3_commit_internal_pre_def set4_commit_internal_pre_def - -lemma FVars_commit_simps[simp]: - "FVars_commit (Finp x y t) = {x, y} \ FFVars t" - "FVars_commit (Fout x y t) = {x, y} \ FFVars t" - "FVars_commit (Binp x y t) = {x} \ (FFVars t - {y})" - "FVars_commit (Bout x y t) = {x} \ (FFVars t - {y})" - "FVars_commit (Tau t) = FFVars t" - apply (unfold Binp_def Bout_def Finp_def Fout_def Tau_def) - apply (unfold commit.FVars_ctor) - apply (unfold toUnfold) - apply (unfold commit_internal.FVars_ctor) - apply (unfold toUnfold) - apply auto - done + set1_commit_pre_def set2_commit_pre_def lemmas commit_pre.map_id0[simp] -lemmas commit_pre_map_cong_id = commit_pre.map_cong[of _ _ "id::var\var" "id::var\var" _ _ _ id _ id, simplified] - -lemma map_commit_pre_Inl_aux: "bij f \ |supp f| - map_commit_pre (id::var\var) (f::var\var) (permute_commit_internal f) id (Abs_commit_pre (Inl (x, y, P))) = - Abs_commit_pre (Inl (x, y, P))" -apply(rule commit_pre_map_cong_id) unfolding toUnfold by auto - -lemma map_commit_pre_Inr_Inl_aux: "bij f \ |supp f| - map_commit_pre (id::var\var) (f::var\var) (permute_commit_internal f) id (Abs_commit_pre (Inr (Inl (x, y, P)))) = - Abs_commit_pre (Inr (Inl (x, y, P)))" -apply(rule commit_pre_map_cong_id) unfolding toUnfold by auto - -lemma map_commit_pre_Inr_Inr_Inl_aux: "bij f \ |supp f| - map_commit_pre id f (permute_commit_internal f) id - (Abs_commit_pre (Inr (Inr (Inl (x::var, y::var, commit_internal_ctor (Abs_commit_internal_pre P)))))) = - Abs_commit_pre (Inr (Inr (Inl (x, f y, commit_internal_ctor (Abs_commit_internal_pre (rrename f P))))))" -unfolding map_commit_pre_def toUnfold apply auto -unfolding commit_internal.permute_ctor -unfolding map_commit_internal_pre_def by (simp add: toUnfold(27)) - -lemma map_commit_pre_Inr_Inr_Inr_Inl_aux: "bij f \ |supp f| - map_commit_pre (id::var\var) (f::var\var) (permute_commit_internal f) id (Abs_commit_pre (Inr (Inr (Inr (Inl P))))) = - Abs_commit_pre (Inr (Inr (Inr (Inl P))))" -apply(rule commit_pre_map_cong_id) unfolding toUnfold by auto - -lemma map_commit_pre_Inr_Inr_Inr_Inr_aux: "bij f \ |supp f| - map_commit_pre (id::var\var) (f::var\var) (permute_commit_internal f) id (Abs_commit_pre (Inr (Inr (Inr (Inr (x::var, y::var, commit_internal_ctor (Abs_commit_internal_pre P))))))) = - Abs_commit_pre (Inr (Inr (Inr (Inr (x, f y, commit_internal_ctor (Abs_commit_internal_pre (rrename f P)))))))" -unfolding map_commit_pre_def toUnfold apply auto -unfolding commit_internal.permute_ctor -unfolding map_commit_internal_pre_def by (simp add: toUnfold(27)) +lemmas commit_pre_map_cong_id = commit_pre.map_cong[of _ _ _ id id id, simplified] lemma Abs_commit_pre_inj[simp]: "Abs_commit_pre k = Abs_commit_pre k' \ k = k'" -by (metis toUnfold(22)) - -lemma Abs_commit_internal_pre_inj[simp]: "Abs_commit_internal_pre k = Abs_commit_internal_pre k' \ k = k'" -by (metis toUnfold(27)) + by (metis toUnfold(21)) lemma Finp_inj[simp]: "Finp x y P = Finp x' y' P' \ x = x' \ y = y' \ P = P'" -unfolding Finp_def unfolding commit.TT_inject0 apply simp -unfolding toUnfold apply auto - subgoal for f apply(subst (asm) map_commit_pre_Inl_aux) by auto - subgoal for f apply(subst (asm) map_commit_pre_Inl_aux) by auto - subgoal for f apply(subst (asm) map_commit_pre_Inl_aux) by auto - subgoal apply(rule exI[of _ id]) apply(subst map_commit_pre_Inl_aux) by auto . + unfolding Finp_def commit.TT_inject0 toUnfold map_commit_pre_def by auto lemma Fout_inj[simp]: "Fout x y P = Fout x' y' P' \ x = x' \ y = y' \ P = P'" -unfolding Fout_def unfolding commit.TT_inject0 apply simp -unfolding toUnfold apply auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inl_aux) by auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inl_aux) by auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inl_aux) by auto - subgoal apply(rule exI[of _ id]) apply(subst map_commit_pre_Inr_Inl_aux) by auto . + unfolding Fout_def commit.TT_inject0 toUnfold map_commit_pre_def by auto lemma Bout_inj[simp]: "Bout x y P = Bout x' y' P' \ x = x' \ ((y' \ FFVars P \ y' = y) \ P' = swap P y y')" -unfolding Bout_def unfolding commit.TT_inject0 apply simp -unfolding toUnfold apply auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inl_aux) by auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inl_aux) - unfolding id_on_def apply auto unfolding commit_internal.FVars_ctor toUnfold by auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inl_aux) - unfolding id_on_def apply auto unfolding commit_internal.FVars_ctor toUnfold - unfolding commit_internal.TT_inject0 id_on_def - unfolding map_commit_internal_pre_def apply (auto simp: toUnfold id_on_def) - apply(rule term.permute_cong) by auto - subgoal apply(rule exI[of _ "(id(y:=y',y':=y))"]) - apply(subst map_commit_pre_Inr_Inr_Inl_aux) apply auto - unfolding commit_internal.FVars_ctor by (auto simp: toUnfold id_on_def) + unfolding Bout_def commit.TT_inject0 toUnfold map_commit_pre_def set3_commit_pre_def apply simp + apply (rule iffI) + apply (auto simp: id_on_def)[1] + apply (rule term.permute_cong) + apply auto subgoal apply(rule exI[of _ "(id(y:=y',y':=y))"]) - apply(subst map_commit_pre_Inr_Inr_Inl_aux) by auto . + by (auto simp: id_on_def) . lemma Binp_inj[simp]: "Binp x y P = Binp x' y' P' \ x = x' \ ((y' \ FFVars P \ y' = y) \ P' = swap P y y')" -unfolding Binp_def unfolding commit.TT_inject0 apply simp -unfolding toUnfold apply auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inr_Inr_aux) by auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inr_Inr_aux) - unfolding id_on_def apply auto unfolding commit_internal.FVars_ctor toUnfold by auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inr_Inr_aux) - unfolding id_on_def apply auto unfolding commit_internal.FVars_ctor toUnfold - unfolding commit_internal.TT_inject0 id_on_def - unfolding map_commit_internal_pre_def apply (auto simp: toUnfold id_on_def) - apply(rule term.permute_cong) by auto - subgoal apply(rule exI[of _ "(id(y:=y',y':=y))"]) - apply(subst map_commit_pre_Inr_Inr_Inr_Inr_aux) apply auto - unfolding commit_internal.FVars_ctor by (auto simp: toUnfold id_on_def) +unfolding Binp_def commit.TT_inject0 toUnfold map_commit_pre_def set3_commit_pre_def apply simp + apply (rule iffI) + apply (auto simp: id_on_def)[1] + apply (rule term.permute_cong) + apply auto subgoal apply(rule exI[of _ "(id(y:=y',y':=y))"]) - apply(subst map_commit_pre_Inr_Inr_Inr_Inr_aux) by auto . + by (auto simp: id_on_def) . lemma Tau_inj[simp]: "Tau P = Tau P' \ P = P'" -unfolding Tau_def unfolding commit.TT_inject0 apply simp -unfolding toUnfold apply auto - subgoal for f apply(subst (asm) map_commit_pre_Inr_Inr_Inr_Inl_aux) by auto - subgoal apply(rule exI[of _ id]) apply(subst map_commit_pre_Inr_Inr_Inr_Inl_aux) by auto . - -(* *) - -lemma Finp_Fout_diff[simp]: "Finp x y P \ Fout x' y' P'" -unfolding Finp_def Fout_def -by (metis Abs_commit_pre_inj Inl_Inr_False commit.TT_inject0 map_commit_pre_Inl_aux) - -lemmas Fout_Finp_diff[simp] = Finp_Fout_diff[symmetric] - -lemma Finp_Bout_diff[simp]: "Finp x y P \ Bout x' y' P'" -unfolding Finp_def Bout_def -by (metis Abs_commit_pre_inj Inl_Inr_False commit.TT_inject0 map_commit_pre_Inl_aux) - -lemmas Bout_Finp_diff[simp] = Finp_Bout_diff[symmetric] - -lemma Finp_Tau_diff[simp]: "Finp x y P \ Tau P'" -unfolding Finp_def Tau_def -by (metis Abs_commit_pre_inj Inl_Inr_False commit.TT_inject0 map_commit_pre_Inl_aux) - -lemmas Tau_Finp_diff[simp] = Finp_Tau_diff[symmetric] - -lemma Fout_Bout_diff[simp]: "Fout x y P \ Bout x' y' P'" -unfolding Fout_def Bout_def -by (metis Abs_commit_pre_inj Inl_Inr_False commit.TT_inject0 map_commit_pre_Inr_Inl_aux sum.inject(2)) - -lemmas Bout_Fout_diff[simp] = Fout_Bout_diff[symmetric] - -lemma Fout_Tau_diff[simp]: "Fout x y P \ Tau P'" -unfolding Fout_def Tau_def -by (metis Abs_commit_pre_inj Inl_Inr_False commit.TT_inject0 map_commit_pre_Inr_Inl_aux sum.inject(2)) - -lemmas Tau_Fout_diff[simp] = Fout_Tau_diff[symmetric] - -lemma Bout_Tau_diff[simp]: "Bout x y P \ Tau P'" -unfolding Bout_def Tau_def -by (smt (verit) Inl_Inr_False Inr_inject commit.TT_inject0 map_commit_pre_Inr_Inr_Inl_aux toUnfold(22)) - -lemmas Tau_Bout_diff[simp] = Bout_Tau_diff[symmetric] - -lemma Binp_Bout_diff[simp]: "Binp x y P \ Bout x' y' P'" - unfolding Binp_def Bout_def - by (smt (verit) Inl_Inr_False Inr_inject commit.TT_inject0 map_commit_pre_Inr_Inr_Inl_aux toUnfold(22)) - -lemmas Bout_Binp_diff[simp] = Binp_Bout_diff[symmetric] - -lemma Binp_Finp_diff[simp]: "Binp x y P \ Finp x' y' P'" - unfolding Binp_def Finp_def - by (metis Abs_commit_pre_inj Inl_Inr_False commit.TT_inject0 map_commit_pre_Inl_aux) - -lemmas Finp_Binp_diff[simp] = Binp_Finp_diff[symmetric] - -lemma Binp_Fout_diff[simp]: "Binp x y P \ Fout x' y' P'" - unfolding Binp_def Fout_def - by (metis Abs_commit_pre_inj Inl_Inr_False Inr_inject commit.TT_inject0 map_commit_pre_Inr_Inl_aux) - -lemmas Fout_Binp_diff[simp] = Binp_Fout_diff[symmetric] - -lemma Binp_Tau_diff[simp]: "Binp x y P \ Tau P'" - unfolding Binp_def Tau_def - by (metis Abs_commit_pre_inj Inr_not_Inl commit.TT_inject0 map_commit_pre_Inr_Inr_Inr_Inl_aux old.sum.inject(2)) - -lemmas Tau_Binp_diff[simp] = Binp_Tau_diff[symmetric] +unfolding Tau_def commit.TT_inject0 toUnfold map_commit_pre_def by auto (* Supply of fresh variables *) @@ -263,39 +116,6 @@ proof- thus ?thesis by auto qed -(* *) - -lemma permute_commit_Finp[simp]: "bij \ \ |supp \| - permute_commit \ (Finp a u P) = Finp (\ a) (\ u) (rrename \ P)" -unfolding Finp_def unfolding commit.permute_ctor -unfolding map_commit_pre_def unfolding toUnfold by simp - -lemma permute_commit_Fout[simp]: "bij \ \ |supp \| - permute_commit \ (Fout a u P) = Fout (\ a) (\ u) (rrename \ P)" -unfolding Fout_def unfolding commit.permute_ctor -unfolding map_commit_pre_def unfolding toUnfold by simp - -lemma permute_commit_Bout[simp]: "bij \ \ |supp \| - permute_commit \ (Bout a u P) = Bout (\ a) (\ u) (rrename \ P)" -unfolding Bout_def unfolding commit.permute_ctor -unfolding map_commit_pre_def unfolding toUnfold -unfolding commit.permute_ctor commit_internal.permute_ctor -unfolding map_commit_internal_pre_def unfolding toUnfold by simp - -lemma permute_commit_Binp[simp]: "bij \ \ |supp \| - permute_commit \ (Binp a u P) = Binp (\ a) (\ u) (rrename \ P)" -unfolding Binp_def unfolding commit.permute_ctor -unfolding map_commit_pre_def unfolding toUnfold -unfolding commit.permute_ctor commit_internal.permute_ctor -unfolding map_commit_internal_pre_def unfolding toUnfold by simp - -lemma permute_commit_Tau[simp]: "bij \ \ |supp \| - permute_commit \ (Tau P) = Tau (rrename \ P)" -unfolding Tau_def unfolding commit.permute_ctor -unfolding map_commit_pre_def unfolding toUnfold -unfolding commit.permute_ctor(1) -unfolding map_commit_internal_pre_def unfolding toUnfold by simp - (* Actions *) datatype (vars:'a) action = finp 'a 'a | fout 'a 'a | is_bout: bout 'a 'a | binp 'a 'a | tau @@ -349,10 +169,7 @@ local_setup \MRBNF_Sugar.register_binder_sugar "Commitment.commit" { (@{term Binp}, @{thm Binp_def}), (@{term Cmt}, @{thm refl}) ], - permute_simps = @{thms - permute_commit_Finp permute_commit_Fout permute_commit_Bout - permute_commit_Binp permute_commit_Tau - }, + permute_simps = @{thms commit.permute}, map_simps = [], distinct = [], bsetss = [[ diff --git a/thys/Pi_Calculus/Pi_Transition_Common.thy b/thys/Pi_Calculus/Pi_Transition_Common.thy index e725464..73d7337 100644 --- a/thys/Pi_Calculus/Pi_Transition_Common.thy +++ b/thys/Pi_Calculus/Pi_Transition_Common.thy @@ -10,7 +10,7 @@ abbreviation Tsupp :: "trm \ cmt \ var set" where (* Supply of fresh variables: *) lemma finite_Tsupp: "finite (Tsupp e1 e2)" - by (metis FVars_commit_simps(5) finite_FVars_commit finite_Un) + by (metis commit.set(4) finite_FVars_commit finite_Un) lemma finite_vars: "finite (vars act)" by (cases act) auto diff --git a/thys/Pi_Calculus/Pi_cong.thy b/thys/Pi_Calculus/Pi_cong.thy index 140cc1d..8b3581a 100644 --- a/thys/Pi_Calculus/Pi_cong.thy +++ b/thys/Pi_Calculus/Pi_cong.thy @@ -41,7 +41,7 @@ thm cong.strong_induct thm cong.equiv lemma finite_Tsupp: "finite (Tsupp x1 x2)" - by (metis FVars_commit_simps(5) finite_FVars_commit finite_Un) + by (metis commit.set(4) finite_FVars_commit finite_Un) lemma exists_fresh: "\ z. z \ set xs \ (z \ Tsupp x1 x2)"