From d9f512a8b7953c7557ba602bb99ca595521831e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= Date: Wed, 27 Nov 2024 18:25:23 +0000 Subject: [PATCH] Add basic automation for injection theorems --- Tools/mrbnf_sugar.ML | 73 +++++++++- operations/BMV_Monad.thy | 96 +++++++++++++ operations/Sugar.thy | 136 +++++++++++++++++- thys/Infinitary_FOL/InfFOL.thy | 4 - thys/Infinitary_Lambda_Calculus/ILC.thy | 22 +-- .../ILC_uniform.thy | 6 +- .../Infinitary_Lambda_Calculus/Iso_LC_ILC.thy | 4 +- thys/POPLmark/POPLmark_1A.thy | 22 +-- thys/POPLmark/SystemFSub.thy | 7 - thys/Pi_Calculus/Commitment.thy | 10 +- thys/Pi_Calculus/Pi.thy | 53 ------- thys/Prelim/Prelim.thy | 5 +- thys/STLC/STLC.thy | 27 +--- thys/Untyped_Lambda_Calculus/LC.thy | 27 +--- 14 files changed, 324 insertions(+), 168 deletions(-) create mode 100644 operations/BMV_Monad.thy diff --git a/Tools/mrbnf_sugar.ML b/Tools/mrbnf_sugar.ML index bf89f7dd..78917d7f 100644 --- a/Tools/mrbnf_sugar.ML +++ b/Tools/mrbnf_sugar.ML @@ -21,6 +21,7 @@ type binder_sugar = { mrbnf: MRBNF_Def.mrbnf, strong_induct: thm option, distinct: thm list, + inject: thm list, ctors: (term * thm) list }; @@ -63,11 +64,12 @@ type binder_sugar = { mrbnf: MRBNF_Def.mrbnf, strong_induct: thm option, distinct: thm list, + inject: thm list, ctors: (term * thm) list }; fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps, mrbnf, - strong_induct, distinct, ctors, bsetss, bset_bounds } = { + strong_induct, distinct, inject, ctors, bsetss, bset_bounds } = { map_simps = map (Morphism.thm phi) map_simps, permute_simps = map (Morphism.thm phi) permute_simps, set_simpss = map (map (Morphism.thm phi)) set_simpss, @@ -77,6 +79,7 @@ fun morph_binder_sugar phi { map_simps, permute_simps, set_simpss, subst_simps, mrbnf = MRBNF_Def.morph_mrbnf phi mrbnf, strong_induct = Option.map (Morphism.thm phi) strong_induct, distinct = map (Morphism.thm phi) distinct, + inject = map (Morphism.thm phi) inject, ctors = map (map_prod (Morphism.term phi) (Morphism.thm phi)) ctors } : binder_sugar; @@ -451,7 +454,69 @@ fun create_binder_datatype (spec : spec) lthy = ])] end ) ctors_tys) ctors_tys)); - (* TODO: map_bij (rename simps); injection *) + val inject = map_filter (fn ((ctor, ctor_def), tys) => if null tys then NONE else try (fn () => + let + val tys' = map (Term.typ_subst_atomic replace) tys; + val ((xs, ys), _) = names_lthy + |> mk_Frees "x" tys' + ||>> mk_Frees "y" tys'; + val ys' = @{map 3} (fn ty => fn x => fn y => + if exists (member (op=) bounds o TFree) (Term.add_tfreesT ty []) then + (if member (op=) bounds ty then x else raise TYPE ("typ contains binder", [ty], [])) else y + ) tys xs ys; + val xs_ys' = @{map_filter 2} (fn x => fn y' => if x = y' then NONE else SOME (x, y')) xs ys'; + + val goal = mk_Trueprop_eq ( + HOLogic.mk_eq (Term.list_comb (ctor, xs), Term.list_comb (ctor, ys')), + foldr1 HOLogic.mk_conj (map HOLogic.mk_eq xs_ys') + ); + in Goal.prove_sorry lthy (names (xs @ map snd xs_ys')) [] goal (fn {context=ctxt, ...} => EVERY1 [ + K (Local_Defs.unfold0_tac ctxt [ctor_def, #inject quotient]), + K (Local_Defs.unfold0_tac ctxt ( + @{thms map_sum.simps map_prod_simp comp_def sum_set_simps cSup_singleton Union_empty + Un_empty_left Un_empty_right Diff_empty UN_empty id_apply sum.inject prod.inject + prod_set_simps UN_single id_def[symmetric] UN_single UN_singleton + } + @ maps MRBNF_Def.set_map_of_mrbnf fp_nesting_mrbnfs + @ map MRBNF_Def.map_id_of_mrbnf fp_nesting_mrbnfs + @ MRBNF_Def.set_defs_of_mrbnf pre_mrbnf + @ [#Abs_inverse (snd info) OF @{thms UNIV_I}, #Abs_inject (snd info) OF @{thms UNIV_I UNIV_I}, + MRBNF_Def.map_def_of_mrbnf pre_mrbnf + ] + )), + rtac ctxt iffI, + SELECT_GOAL (EVERY1 [ + REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], + REPEAT_DETERM o (TRY o rtac ctxt conjI THEN' assume_tac ctxt), + IF_UNSOLVED o EVERY' [ + rotate_tac ~1, + dtac ctxt @{thm trans[rotated]}, + rtac ctxt sym, + resolve_tac ctxt (#permute_cong_id (#inner quotient) :: map (fn mrbnf => + trans OF [MRBNF_Def.map_cong_of_mrbnf mrbnf, MRBNF_Def.map_id_of_mrbnf mrbnf] + ) fp_nesting_mrbnfs), + REPEAT_DETERM o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms supp_id_bound bij_id}), + TRY o rtac ctxt refl, + K (Local_Defs.unfold0_tac ctxt @{thms id_apply}), + REPEAT_DETERM o EVERY' [ + dtac ctxt @{thm id_on_Diff}, + rtac ctxt @{thm id_onI}, + dtac ctxt @{thm singletonD}, + hyp_subst_tac ctxt, + assume_tac ctxt, + etac ctxt @{thm id_onD}, + REPEAT_DETERM o assume_tac ctxt + ] + ] + ]), + REPEAT_DETERM o rtac ctxt @{thm exI[of _ id]}, + REPEAT_DETERM o etac ctxt conjE, + REPEAT_DETERM o (resolve_tac ctxt ( + (trans OF [#permute_id quotient]) :: @{thms id_apply conjI supp_id_bound bij_id id_on_id} + @ map (fn mrbnf => trans OF [MRBNF_Def.map_id_of_mrbnf mrbnf]) fp_nesting_mrbnfs + ) ORELSE' assume_tac ctxt) + ]) end) () + ) ctors_tys; (* Term for variable substitution *) val x = length replace - #rec_vars spec; @@ -778,6 +843,7 @@ fun create_binder_datatype (spec : spec) lthy = bset_bounds = [], mrbnf = mrbnf, distinct = distinct, + inject = inject, ctors = ctors } : binder_sugar; @@ -793,7 +859,8 @@ fun create_binder_datatype (spec : spec) lthy = @ [("set", flat set_simpss, simp), ("map", map_simps, simp), ("permute", permute_simps, simp), - ("distinct", distinct, simp) + ("distinct", distinct, simp), + ("inject", inject, simp) ] @ the_default [] (Option.map (fn (_, tvsubst_simps) => [("subst", tvsubst_simps, simp)]) tvsubst_opt) ) |> (map (fn (thmN, thms, attrs) => ((Binding.qualify true (Binding.name_of (#fp_b spec)) (Binding.name thmN), attrs), [(thms, [])]) diff --git a/operations/BMV_Monad.thy b/operations/BMV_Monad.thy new file mode 100644 index 00000000..e9331571 --- /dev/null +++ b/operations/BMV_Monad.thy @@ -0,0 +1,96 @@ +theory BMV_Monad + imports "Binders.MRBNF_Recursor" +begin + +declare [[mrbnf_internals]] +binder_datatype 'a FType + = TyVar 'a + | TyApp "'a FType" "'a FType" + | TyAll a::'a t::"'a FType" binds a in t + +(* +SOps = { 'a FType } +L = 'a FType +m = 1 +*) +abbreviation Inj_FType_1 :: "'tyvar::var \ 'tyvar FType" where "Inj_FType_1 \ TyVar" +abbreviation Sb_FType :: "('tyvar::var \ 'tyvar FType) \ 'tyvar FType \ 'tyvar FType" where "Sb_FType \ tvsubst_FType" +abbreviation Vrs_FType_1 :: "'tyvar::var FType \ 'tyvar set" where "Vrs_FType_1 \ FVars_FType" + +lemma SSupp_Inj_FType[simp]: "SSupp_FType Inj_FType_1 = {}" unfolding SSupp_FType_def tvVVr_tvsubst_FType_def TyVar_def tv\_FType_tvsubst_FType_def by simp +lemma IImsupp_Inj_FType[simp]: "IImsupp_FType Inj_FType_1 = {}" unfolding IImsupp_FType_def by simp +lemma SSupp_IImsupp_bound[simp]: + fixes \::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| | \'::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| \ \') \ SSupp_FType \ \ SSupp_FType \'" + unfolding SSupp_FType_def tvVVr_tvsubst_FType_def tv\_FType_tvsubst_FType_def comp_def + apply (unfold TyVar_def[symmetric]) + apply (rule subsetI) + apply (unfold mem_Collect_eq) + apply simp + using assms(1) by force +lemma SSupp_comp_bound[simp]: + fixes \ \'::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| '| \ \')| ::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| \ Inj_FType_1 = \" + using assms by auto + +lemma Sb_comp_FType: + fixes \ \'::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| '| \ Sb_FType \' = Sb_FType (Sb_FType \ \ \')" + apply (rule ext) + apply (rule trans[OF comp_apply]) + subgoal for x + apply (binder_induction x avoiding: "IImsupp_FType \" "IImsupp_FType \'" "IImsupp_FType (Sb_FType \ \ \')" rule: FType.strong_induct) + using assms by (auto simp: IImsupp_FType_def FType.Un_bound FType.UN_bound FType.set_bd_UNIV) + done + +lemma Vrs_Inj_FType: "Vrs_FType_1 (Inj_FType_1 a) = {a}" + by simp + +lemma Vrs_Sb_FType: + fixes \::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| x) = (\a\Vrs_FType_1 x. Vrs_FType_1 (\ a))" +proof (binder_induction x avoiding: "IImsupp_FType \" rule: FType.strong_induct) + case (TyAll x1 x2) + then show ?case using assms by (auto intro!: FType.IImsupp_Diff[symmetric]) +qed (auto simp: assms) + +lemma Sb_cong_FType: + fixes \ \'::"'tyvar::var \ 'tyvar FType" + assumes "|SSupp_FType \| '| a. a \ Vrs_FType_1 t \ \ a = \' a" + shows "Sb_FType \ t = Sb_FType \' t" +using assms(3) proof (binder_induction t avoiding: "IImsupp_FType \" "IImsupp_FType \'" rule: FType.strong_induct) + case (TyAll x1 x2) + then show ?case using assms apply auto + by (smt (verit, ccfv_threshold) CollectI IImsupp_FType_def SSupp_FType_def Un_iff) +qed (auto simp: assms(1-2)) + +(* *) + +type_synonym ('var, 'tyvar, 'bvar, 'btyvar, 'rec, 'brec) FTerm_pre' = "('var + 'rec * 'rec + 'btyvar * 'brec) + ('bvar * 'tyvar FType * 'brec + 'rec * 'tyvar FType)" + + + +end \ No newline at end of file diff --git a/operations/Sugar.thy b/operations/Sugar.thy index cc485bf6..dd32bb6f 100644 --- a/operations/Sugar.thy +++ b/operations/Sugar.thy @@ -521,6 +521,140 @@ lemma T2_distinct[simp]: apply (rule notI, (erule exE conjE sum.distinct[THEN notE])+)+ done +lemmas map_id0_nesting = list.map_id0 prod.map_id0 +lemmas set_map_nesting = list.set_map prod.set_map + +lemma T1_inject[simp]: + "(Var_T1 x = Var_T1 y) = (x = y)" + "(TyVar_T1 x2 = TyVar_T1 y2) = (x2 = y2)" + "(App_T1 x3 x4 = App_T1 y3 y4) = (x3 = y3 \ x4 = y4)" + "(BFree_T1 x xs = BFree_T1 x ys) = (xs = ys)" + "(Lam_T1 x x3 = Lam_T1 x y3) = (x3 = y3)" + "(TyLam_T1 x2 x3 = TyLam_T1 x2 y3) = (x3 = y3)" + "(Ext_T1 x5 = Ext_T1 y5) = (x5 = y5)" + apply (unfold T1_ctors_defs TT_inject0s) + apply (unfold map_T1_pre_def comp_def map_sum.simps map_prod_simp Abs_T1_pre_inverse[OF UNIV_I] + set_simp_thms T1_pre_set_defs id_apply Abs_T1_pre_inject[OF UNIV_I UNIV_I] sum.inject prod.inject + set_map_nesting + ) + apply (unfold id_def[symmetric]) + (* REPEAT_DETERM *) + apply (rule iffI) + apply (erule exE conjE)+ + apply ((rule conjI)?, assumption)+ + apply (rule exI[of _ id])+ + apply ((erule conjE)+)? + apply (rule conjI bij_id supp_id_bound id_on_id | assumption)+ + (* repeated *) + apply (rule iffI) + apply (erule exE conjE)+ + apply ((rule conjI)?, assumption)+ + apply (rule exI[of _ id])+ + apply ((erule conjE)+)? + apply (rule conjI bij_id supp_id_bound id_on_id | assumption)+ + (* repeated *) + apply (rule iffI) + apply (erule exE conjE)+ + apply ((rule conjI)?, assumption)+ + apply (rule exI[of _ id])+ + apply (erule conjE)+ + apply (rule conjI bij_id supp_id_bound id_on_id | assumption)+ + (* repeated *) + apply (rule iffI) + apply (erule exE conjE)+ + apply hypsubst_thin + apply (rule sym) + apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)? + apply (drule id_on_Diff) + apply (rule id_onI) + apply (drule singletonD) + apply hypsubst + apply assumption + apply (erule id_onD) + apply (rule UN_I) + apply assumption+ + apply (rule refl) + apply (rule exI[of _ id])+ + apply ((erule conjE)+)? + apply (unfold list.map_id0 prod.map_id0) + apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+ + (* repeated *) + apply (rule iffI) + apply (erule exE conjE)+ + apply hypsubst_thin + apply (rule sym) + apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)? + apply (rule permute_cong_ids) + apply assumption+ + (* REPEAT_DETERM *) + apply (drule id_on_Diff) + apply (rule id_onI) + apply (drule singletonD) + apply hypsubst + apply assumption + apply (erule id_onD) + apply (rule UN_I)? + apply assumption+ + (* repeated *) + apply (drule id_on_Diff) + apply (rule id_onI) + apply (drule singletonD) + apply hypsubst + apply assumption + apply (erule id_onD) + apply (rule UN_I)? + apply assumption+ + (* END REPEAT_DETERM *) + apply (rule exI[of _ id])+ + apply ((erule conjE)+)? + apply (unfold list.map_id0 prod.map_id0 permute_id0s)? + apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+ + (* repeated *) + apply (rule iffI) + apply (erule exE conjE)+ + apply hypsubst_thin + apply (rule sym) + apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)? + apply (rule permute_cong_ids) + apply assumption+ + (* REPEAT_DETERM *) + apply (drule id_on_Diff) + apply (rule id_onI) + apply (drule singletonD) + apply hypsubst + apply assumption + apply (erule id_onD) + apply (rule UN_I)? + apply assumption+ + (* repeated *) + apply (drule id_on_Diff) + apply (rule id_onI) + apply (drule singletonD) + apply hypsubst + apply assumption + apply (erule id_onD) + apply (rule UN_I)? + apply assumption+ + (* END REPEAT_DETERM *) + apply (rule exI[of _ id])+ + apply ((erule conjE)+)? + apply (unfold list.map_id0 prod.map_id0 permute_id0s)? + apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+ + (* repeated *) + apply (rule iffI) + apply (erule exE conjE)+ + apply hypsubst_thin + apply (rule sym) + apply ((rule trans[OF list.map_cong[OF refl] list.map_id] trans[OF prod.map_cong[OF refl] prod.map_id], rule trans[rotated, OF id_apply[symmetric]])+)? + apply (rule permute_cong_ids, assumption+)? + apply (rule refl)? + apply (rule exI[of _ id])+ + apply ((erule conjE)+)? + apply (unfold list.map_id0 prod.map_id0 permute_id0s)? + apply (rule conjI bij_id supp_id_bound id_on_id trans[OF id_apply] refl | assumption)+ + (* END REPEAT_DETERM *) + done + abbreviation eta11 :: "'a \ ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g::var, 'h, 'i, 'j, 'k) T1_pre" where "eta11 x \ Abs_T1_pre (Inl (Inl (Inl x)))" abbreviation eta12 :: "'b \ ('a::var, 'b::var, 'c::var, 'd, 'e::var, 'f::var, 'g::var, 'h, 'i, 'j, 'k) T1_pre" where @@ -664,8 +798,6 @@ print_theorems lemmas prod_sum_simps = prod.set_map sum.set_map prod_set_simps sum_set_simps UN_empty UN_empty2 Un_empty_left Un_empty_right UN_singleton comp_def map_sum.simps map_prod_simp UN_single -lemmas map_id0_nesting = list.map_id0 prod.map_id0 -lemmas set_map_nesting = list.set_map prod.set_map lemma map_simps[simp]: fixes f1::"'a::var \ 'a" and f2::"'b::var \ 'b" and f3::"'c::var \ 'c" and f4::"'d \ 'e" diff --git a/thys/Infinitary_FOL/InfFOL.thy b/thys/Infinitary_FOL/InfFOL.thy index 03aeb4c9..874b077d 100644 --- a/thys/Infinitary_FOL/InfFOL.thy +++ b/thys/Infinitary_FOL/InfFOL.thy @@ -339,10 +339,6 @@ binder_inductive deduct unfolding induct_rulify_fallback split_beta apply (elim disj_forward exE) apply (auto simp: ifol'.permute_comp in_k_equiv in_k_equiv' isPerm_def ifol'.permute_id supp_inv_bound) - apply (rule exI) - apply (rule conjI) - apply (rule refl) - apply (rule allI impI)+ apply (unfold set\<^sub>k.map_comp) apply (subst ifol'.permute_comp0) apply (assumption | rule bij_imp_bij_inv supp_inv_bound)+ diff --git a/thys/Infinitary_Lambda_Calculus/ILC.thy b/thys/Infinitary_Lambda_Calculus/ILC.thy index 89bbaf6b..c6ad10f6 100644 --- a/thys/Infinitary_Lambda_Calculus/ILC.thy +++ b/thys/Infinitary_Lambda_Calculus/ILC.thy @@ -248,26 +248,6 @@ qed (auto simp: IImsupp_def iterm.UN_bound iterm.Un_bound iterm.set_bd_UNIV f g) (* *) -proposition iApp_inject[simp]: "(iApp a b = iApp c d) = (a = c \ b = d)" -proof - assume "iApp a b = iApp c d" - then show "a = c \ b = d" - unfolding iApp_def fun_eq_iff iterm.TT_inject0 - map_iterm_pre_def comp_def Abs_iterm_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id - Abs_iterm_pre_inject[OF UNIV_I UNIV_I] - by auto -qed simp - -proposition iVar_inject[simp]: "(iVar a = iVar b) = (a = b)" - apply (rule iffI[rotated]) - apply (rule arg_cong[of _ _ iVar]) - apply assumption - unfolding iVar_def iterm.TT_inject0 map_iterm_pre_def comp_def map_sum_def sum.case Abs_iterm_pre_inverse[OF UNIV_I] - id_def Abs_iterm_pre_inject[OF UNIV_I UNIV_I] sum.inject - apply (erule exE conjE)+ - apply assumption - done - lemma iLam_inject: "(iLam xs e = iLam xs' e') = (\f. bij f \ |supp (f::ivar \ ivar)| id_on (FFVars (iLam xs e)) f \ dsmap f xs = xs' \ irrename f e = e')" unfolding iterm.set @@ -1230,7 +1210,7 @@ apply safe lemma R_iApp_elim: assumes "R (iApp e1 es2) b" shows "\b1 bs2. R e1 b1 \ stream_all2 R es2 bs2 \ b = iAppB b1 bs2" -by (metis (no_types, lifting) R.cases assms iApp_inject iterm.distinct(3) iterm.distinct(6)) +by (metis (no_types, lifting) R.cases assms iterm.inject iterm.distinct(3) iterm.distinct(6)) lemma R_iLam_elim: assumes "R (iLam xs e) b" diff --git a/thys/Infinitary_Lambda_Calculus/ILC_uniform.thy b/thys/Infinitary_Lambda_Calculus/ILC_uniform.thy index 17013c32..8f0d6120 100644 --- a/thys/Infinitary_Lambda_Calculus/ILC_uniform.thy +++ b/thys/Infinitary_Lambda_Calculus/ILC_uniform.thy @@ -206,7 +206,7 @@ using uniformS_def3[unfolded reneqvS_def] . lemma uniformS_smap2_iApp_iff: "uniformS (smap2 iApp es ess) \ uniformS es \ uniformS (sflat ess)" unfolding uniformS_def4 sset_sflat sset_smap2 unfolding sset_range apply auto - apply (metis iApp_inject reneqv_iApp_casesR) + apply (metis iterm.inject reneqv_iApp_casesR) subgoal for i j i' j' apply(erule allE[of _ "iApp (es !! i) (ess !! i)"]) apply(erule allE[of _ "iApp (es !! i') (ess !! i')"]) apply auto using reneqv_iApp_casesR by fastforce @@ -366,7 +366,7 @@ proof- have u': "uniform (iLam xs e1)" using u uniform_iApp_iff by blast have fves2: "touchedSuper (\ (FFVars ` (sset es2))) = touchedSuper (FFVars e2) " - by (metis e2 iApp_inject reneqvS_def reneqv_iApp_casesL u uniformS_def3 uniformS_touchedSuper uniform_def3) + by (metis e2 iterm.inject reneqvS_def reneqv_iApp_casesL u uniformS_def3 uniformS_touchedSuper uniform_def3) have ss: "small (\ (FFVars ` (sset es2)))" unfolding small_def apply(rule iterm.UN_bound) @@ -460,4 +460,4 @@ shows "uniform e'" *) -end \ No newline at end of file +end diff --git a/thys/Infinitary_Lambda_Calculus/Iso_LC_ILC.thy b/thys/Infinitary_Lambda_Calculus/Iso_LC_ILC.thy index 3130ca33..f0953c54 100644 --- a/thys/Infinitary_Lambda_Calculus/Iso_LC_ILC.thy +++ b/thys/Infinitary_Lambda_Calculus/Iso_LC_ILC.thy @@ -427,7 +427,7 @@ lemma usetpD_snth_eq: "ustepD d ts ss \ snth ts i = snth ts j \ snth ss i = snth ss j" apply(induct arbitrary: i j rule: ustepD.induct) subgoal unfolding stream_all2_iff_snth using hred_determ by metis - subgoal by (metis iApp_inject snth_smap2) + subgoal by (metis iterm.inject snth_smap2) subgoal apply simp unfolding snth_sflat by (metis nat2_nat1 snth2.simps stream_eq_nth) subgoal by (metis iLam_same_inject snth_smap) . @@ -567,4 +567,4 @@ subgoal for ts apply(rule exI[of _ "snth ts 0"]) apply safe by simp (metis snth.simps(1)) . . -end \ No newline at end of file +end diff --git a/thys/POPLmark/POPLmark_1A.thy b/thys/POPLmark/POPLmark_1A.thy index a3fd59a8..09fa9c09 100644 --- a/thys/POPLmark/POPLmark_1A.thy +++ b/thys/POPLmark/POPLmark_1A.thy @@ -97,7 +97,7 @@ using assms(1,2) proof (binder_induction \ "\X<:S\<^sub>1. S\<^su using SA_All(6,9) well_scoped(2) by fastforce have fresh: "X \ FVars_typ T\<^sub>1" by (meson SA_All(4,9) in_mono well_scoped(1)) - have same: "R\<^sub>1 = S\<^sub>1" using SA_All(8) typ_inject(3) by blast + have same: "R\<^sub>1 = S\<^sub>1" using SA_All(8) typ_inject by blast have x: "\Y<:S\<^sub>1. R\<^sub>2 = \X<:S\<^sub>1. permute_typ (id(Y:=X,X:=Y)) R\<^sub>2" apply (rule Forall_swap) by (metis (no_types, lifting) SA_All(8) assms(1,2) in_mono sup.bounded_iff typ.set(4) well_scoped(1)) @@ -115,7 +115,7 @@ using assms(1,2) proof (binder_induction \ "\X<:S\<^sub>1. S\<^su using SA_All(1,9) apply (metis bij_swap SA_All(4) Un_iff context_map_cong_id fun_upd_apply id_apply infinite_var supp_swap_bound wf_FFVars wf_context) apply simp using fresh SA_All(3) apply simp - using x SA_All(8) unfolding same using Forall_inject_same by simp + using x SA_All(8) unfolding same by simp qed (auto simp: Top) lemma SA_AllE2[consumes 2, case_names SA_Trans_TVar SA_All]: @@ -132,15 +132,15 @@ using assms(1,2) proof (binder_induction \ S "\X<:T\<^sub>1. T\<^ using SA_All(9) apply blast by (metis SA_All(6) fst_conv wf_ConsE wf_context) have fresh2: "X \ FVars_typ T\<^sub>1" "Y \ FVars_typ T\<^sub>1" - apply (metis SA_All(4,8) in_mono fresh(1) typ_inject(3) well_scoped(1)) - by (metis SA_All(4,8) in_mono fresh(2) typ_inject(3) well_scoped(1)) - have same: "R\<^sub>1 = T\<^sub>1" using SA_All(8) typ_inject(3) by blast + apply (metis SA_All(4,8) in_mono fresh(1) typ_inject well_scoped(1)) + by (metis SA_All(4,8) in_mono fresh(2) typ_inject well_scoped(1)) + have same: "R\<^sub>1 = T\<^sub>1" using SA_All(8) typ_inject by blast have x: "\Y<:T\<^sub>1 . R\<^sub>2 = \X<:T\<^sub>1. permute_typ (id(Y:=X,X:=Y)) R\<^sub>2" apply (rule Forall_swap) by (metis SA_All(8) Un_iff assms(1,2) in_mono typ.set(4) well_scoped(2)) show ?case unfolding 1 apply (rule Forall) - apply (metis SA_All(4,8) typ_inject(3)) + apply (metis SA_All(4,8) typ_inject) apply (rule iffD2[OF arg_cong3[OF _ refl, of _ _ _ _ ty], rotated -1]) apply (rule ty.equiv) apply (rule bij_swap supp_swap_bound infinite_var)+ @@ -152,7 +152,7 @@ using assms(1,2) proof (binder_induction \ S "\X<:T\<^sub>1. T\<^ using fresh apply (metis bij_swap SA_All(4) Un_iff context_map_cong_id fun_upd_apply id_apply infinite_var supp_swap_bound wf_FFVars wf_context) apply simp using fresh2 unfolding same apply (metis bij_swap fun_upd_apply id_apply infinite_var supp_swap_bound typ.permute_cong_id) - using SA_All(8) x Forall_inject_same unfolding same by simp + using SA_All(8) x unfolding same by simp qed (auto simp: TyVar) lemma ty_transitivity : "\ \ \ S <: Q ; \ \ Q <: T \ \ \ \ S <: T" @@ -253,7 +253,7 @@ proof - then show ?thesis by (meson left(1,3) ty.SA_Arrow ty.SA_Top well_scoped(1)) next case right: (SA_Arrow U\<^sub>1 R\<^sub>1 R\<^sub>2 U\<^sub>2) - then show ?thesis using left by (metis Fun(1,3) SA_Arrow typ_inject(2)) + then show ?thesis using left by (metis Fun(1,3) SA_Arrow typ.inject) qed auto qed auto } note ty_trans = this @@ -412,8 +412,8 @@ next case (SA_Arrow \ U\<^sub>1 R\<^sub>1 R\<^sub>2 U\<^sub>2) show ?case apply (rule ty.SA_Arrow) - apply (metis Fun(1) SA_Arrow(1,5,6,8) typ_inject(2)) - by (metis Fun(2) SA_Arrow(3,5,7,8) typ_inject(2)) + apply (metis Fun(1) SA_Arrow(1,5,6,8) typ.inject) + by (metis Fun(2) SA_Arrow(3,5,7,8) typ.inject) qed auto qed auto next @@ -439,4 +439,4 @@ qed auto corollary ty_narrowing2: "\ \ , X <: Q, \ \ M <: N ; \ \ R <: Q \ \ \, X <: R, \ \ M <: N" using ty_narrowing_aux ty_transitivity2 by blast -end \ No newline at end of file +end diff --git a/thys/POPLmark/SystemFSub.thy b/thys/POPLmark/SystemFSub.thy index f41d5228..49edcf36 100644 --- a/thys/POPLmark/SystemFSub.thy +++ b/thys/POPLmark/SystemFSub.thy @@ -23,8 +23,6 @@ declare supp_swap_bound[OF cinfinite_imp_infinite[OF typ.UNIV_cinfinite], simp] declare typ.permute_id[simp] typ.permute_id0[simp] lemma typ_inject: - "TyVar x = TyVar y \ x = y" - "Fun T1 T2 = Fun R1 R2 \ T1 = R1 \ T2 = R2" "Forall x T1 T2 = Forall y R1 R2 \ T1 = R1 \ (\f. bij (f::'a::var \ 'a) \ |supp f| id_on (FVars_typ T2 - {x}) f \ f x = y \ permute_typ f T2 = R2)" apply (unfold TyVar_def Fun_def Forall_def typ.TT_inject0 set3_typ_pre_def comp_def Abs_typ_pre_inverse[OF UNIV_I] map_sum.simps sum_set_simps @@ -33,11 +31,6 @@ lemma typ_inject: sum.inject prod.inject map_prod_simp ) by auto -declare typ_inject(1,2)[simp] - -corollary Forall_inject_same[simp]: "Forall x T1 T2 = Forall x R1 R2 \ T1 = R1 \ T2 = R2" - using typ_inject(3) typ.permute_cong_id - by (metis (no_types, lifting) Diff_empty Diff_insert0 id_on_insert insert_Diff) lemma Forall_rrename: assumes "bij \" "|supp \| k = k'" 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 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 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 commit.TT_inject0 toUnfold map_commit_pre_def set3_commit_pre_def apply simp apply (rule iffI) @@ -52,9 +46,6 @@ unfolding Binp_def commit.TT_inject0 toUnfold map_commit_pre_def set3_commit_pre subgoal apply(rule exI[of _ "(id(y:=y',y':=y))"]) by (auto simp: id_on_def) . -lemma Tau_inj[simp]: "Tau P = Tau P' \ P = P'" -unfolding Tau_def commit.TT_inject0 toUnfold map_commit_pre_def by auto - (* Supply of fresh variables *) lemma finite_FVars_commit: "finite (FVars_commit (C::var commit))" @@ -138,6 +129,7 @@ local_setup \MRBNF_Sugar.register_binder_sugar "Commitment.commit" { ]], bset_bounds = @{thms bns_bound}, strong_induct = NONE, + inject = @{thms commit.inject}, mrbnf = the (MRBNF_Def.mrbnf_of @{context} "Commitment.commit_pre"), set_simpss = [], subst_simps = NONE diff --git a/thys/Pi_Calculus/Pi.thy b/thys/Pi_Calculus/Pi.thy index d42601ed..a3267a53 100644 --- a/thys/Pi_Calculus/Pi.thy +++ b/thys/Pi_Calculus/Pi.thy @@ -72,32 +72,6 @@ qed (* Properties of the constructors *) -proposition Sum_inject[simp]: "(Sum a b = Sum c d) = (a = c \ b = d)" -unfolding Sum_def fun_eq_iff term.TT_inject0 -map_term_pre_def comp_def Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id -Abs_term_pre_inject[OF UNIV_I UNIV_I] -by auto - -proposition Par_inject[simp]: "(Par a b = Par c d) = (a = c \ b = d)" -unfolding Par_def fun_eq_iff term.TT_inject0 -map_term_pre_def comp_def Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id -Abs_term_pre_inject[OF UNIV_I UNIV_I] by auto - -proposition Bang_inject[simp]: "(Bang a = Bang b) = (a = b)" -unfolding Bang_def fun_eq_iff term.TT_inject0 -map_term_pre_def comp_def Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id -Abs_term_pre_inject[OF UNIV_I UNIV_I] by auto - -proposition Match_inject[simp]: "(Match x1 y1 a1 = Match x2 y2 a2) = (x1 = x2 \ y1 = y2 \ a1 = a2)" -unfolding Match_def fun_eq_iff term.TT_inject0 -map_term_pre_def comp_def Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id -Abs_term_pre_inject[OF UNIV_I UNIV_I] by auto - -proposition Out_inject[simp]: "(Out x1 y1 a1 = Out x2 y2 a2) = (x1 = x2 \ y1 = y2 \ a1 = a2)" -unfolding Out_def fun_eq_iff term.TT_inject0 -map_term_pre_def comp_def Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id -Abs_term_pre_inject[OF UNIV_I UNIV_I] by auto - lemma Inp_inject: "(Inp x y e = Inp x' y' e') \ x = x' \ (\f. bij f \ |supp (f::var \ var)| set3_term_pre_def sum_set_simps Union_empty Un_empty_left prod_set_simps cSup_singleton set2_term_pre_def Un_empty_right UN_single by auto -lemma Inp_inject_same[simp]: "Inp x y e = Inp x' y e' \ ((x::var) = x' \ e = e')" - apply (rule trans[OF Inp_inject]) - apply (rule iffI) - apply (erule exE conjE)+ - apply (rule conjI) - apply assumption - apply (frule term.permute_cong_id[of _ e]) - apply assumption - apply (rule case_split[of "_ \ _", rotated]) - apply (erule id_onD) - apply (rule DiffI[rotated]) - apply assumption - apply assumption - apply (drule singletonD) - apply hypsubst - apply assumption - apply hypsubst - apply (erule sym) - apply (erule conjE) - apply (erule conjI) - apply (rule exI[of _ id]) - apply (rule bij_id supp_id_bound id_on_id id_apply conjI)+ - apply (rule trans) - apply (rule term.permute_id) - apply assumption - done - lemma Res_inject: "(Res y e = Res y' e') \ (\f. bij f \ |supp (f::var \ var)| id_on (FVars_term e - {y}) f \ f y = y' \ permute_term f e = e')" diff --git a/thys/Prelim/Prelim.thy b/thys/Prelim/Prelim.thy index 6bd63728..7ea1ff03 100644 --- a/thys/Prelim/Prelim.thy +++ b/thys/Prelim/Prelim.thy @@ -71,6 +71,9 @@ lemma id_on_id[simp,intro!]: "id_on A id" lemma id_on_insert[simp]: "id_on (insert x A) f \ f x = x \ id_on A f" unfolding id_on_def by blast +lemma id_on_Diff: "id_on (A - B) f \ id_on B f \ id_on A f" + unfolding id_on_def by blast + definition "eq_on A f g \ \ a. a \ A \ f a = g a" lemma eq_onI: "(\a. a \ A \ f a = g a) \ eq_on A f g" @@ -539,7 +542,7 @@ definition "hidden_id = id" lemma id_hid_o_hid: "id = hidden_id o hidden_id" unfolding hidden_id_def by simp -lemma emp_bound: "|{}::'a set| Cinfinite s \ regularCard r \ regularCard s \ regularCard (r +c s)" diff --git a/thys/STLC/STLC.thy b/thys/STLC/STLC.thy index 8691b603..5aa81658 100644 --- a/thys/STLC/STLC.thy +++ b/thys/STLC/STLC.thy @@ -70,24 +70,6 @@ corollary SSupp_upd_VVr_bound: "|SSupp_terms (tvVVr_tvsubst(a:=(t::'a::var terms lemma supp_subset_id_on: "supp f \ A \ id_on (B - A) f" unfolding supp_def id_on_def by blast -lemma App_inject[simp]: "(App a b = App c d) = (a = c \ b = d)" -proof - assume "App a b = App c d" - then show "a = c \ b = d" - unfolding App_def fun_eq_iff terms.TT_inject0 - map_terms_pre_def comp_def Abs_terms_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id - Abs_terms_pre_inject[OF UNIV_I UNIV_I] - by blast -qed simp -lemma Var_inject[simp]: "(Var a = Var b) = (a = b)" - apply (rule iffI[rotated]) - apply (rule arg_cong[of _ _ Var]) - apply assumption - unfolding Var_def terms.TT_inject0 map_terms_pre_def comp_def map_sum_def sum.case Abs_terms_pre_inverse[OF UNIV_I] - id_def Abs_terms_pre_inject[OF UNIV_I UNIV_I] sum.inject - apply (erule exE conjE)+ - apply assumption - done lemma Abs_inject: "(Abs x \ e = Abs x' \' e') = (\f. bij f \ |supp (f::'a::var \ 'a)| id_on (FVars_terms (Abs x \ e)) f \ f x = x' \ \ = \' \ permute_terms f e = e')" unfolding terms.set @@ -211,19 +193,12 @@ inductive Ty :: "('a::var * \) fset \ 'a terms \ \< lemma map_prod_comp0: "map_prod f1 f2 \ map_prod f3 f4 = map_prod (f1 \ f3) (f2 \ f4)" using prod.map_comp by auto -ML \ -Multithreading.parallel_proofs := 0 -\ binder_inductive Ty subgoal for R B \ x1 x2 x3 apply (elim disj_forward) apply (auto simp: map_prod_comp0 terms.permute_comp[OF _ _ bij_imp_bij_inv supp_inv_bound] terms.permute_id) apply force - apply (rule exI) - apply (rule conjI) - apply (rule refl) - apply (simp add: terms.permute_comp[OF _ _ bij_imp_bij_inv supp_inv_bound] terms.permute_id) unfolding fresh_def by force subgoal for R B x1 x2 x3 apply (rule exI[of _ B]) @@ -512,7 +487,7 @@ proof (induction "{||} :: ('a::var * \) fset" e \ arbitrary: e' rule: case (ST_Beta x \ e e2') then have "{||} \\<^sub>t\<^sub>y App (Abs x \ e) e2 : \\<^sub>2" using Ty_App Ty.Ty_App by fastforce have "{||} \\<^sub>t\<^sub>y Abs x \\<^sub>1 e : \\<^sub>1 \ \\<^sub>2" using Ty_App ST_Beta - by (smt (verit, ccfv_SIG) Abs_inject App_inject Ty.cases \.inject terms.distinct(2, 4)) + by (smt (verit, ccfv_SIG) Abs_inject terms.inject Ty.cases \.inject terms.distinct(2, 4)) then have "{||},x:\\<^sub>1 \\<^sub>t\<^sub>y e : \\<^sub>2" by (auto elim: Ty_AbsE') then have "{||} \\<^sub>t\<^sub>y tvsubst (tvVVr_tvsubst(x := e2')) e : \\<^sub>2" using substitution ST_Beta(1) Ty_App(3) unfolding fresh_def by fastforce then show ?thesis using ST_Beta by simp diff --git a/thys/Untyped_Lambda_Calculus/LC.thy b/thys/Untyped_Lambda_Calculus/LC.thy index 068f9f60..b11a79f4 100644 --- a/thys/Untyped_Lambda_Calculus/LC.thy +++ b/thys/Untyped_Lambda_Calculus/LC.thy @@ -135,26 +135,6 @@ proof- by auto metis . qed -proposition App_inject[simp]: "(App a b = App c d) = (a = c \ b = d)" -proof - assume "App a b = App c d" - then show "a = c \ b = d" - unfolding App_def fun_eq_iff term.TT_inject0 - map_term_pre_def comp_def Abs_term_pre_inverse[OF UNIV_I] map_sum_def sum.case prod.map_id - Abs_term_pre_inject[OF UNIV_I UNIV_I] - by blast -qed simp - -proposition Var_inject[simp]: "(Var a = Var b) = (a = b)" - apply (rule iffI[rotated]) - apply (rule arg_cong[of _ _ Var]) - apply assumption - unfolding Var_def term.TT_inject0 map_term_pre_def comp_def map_sum_def sum.case Abs_term_pre_inverse[OF UNIV_I] - id_def Abs_term_pre_inject[OF UNIV_I UNIV_I] sum.inject - apply (erule exE conjE)+ - apply assumption - done - lemma Lam_inject: "(Lam x e = Lam x' e') = (\f. bij f \ |supp (f::var \ var)| id_on (FVars_term (Lam x e)) f \ f x = x' \ rrename f e = e')" unfolding term.set @@ -165,11 +145,6 @@ lemma Lam_inject: "(Lam x e = Lam x' e') = (\f. bij f \ |supp (f::v apply (rule refl) done -lemma Lam_same_inject[simp]: "Lam (x::var) e = Lam x e' \ e = e'" -unfolding Lam_inject apply safe -apply(rule term.permute_cong_id[symmetric]) -unfolding id_on_def by auto - lemma bij_map_term_pre: "bij f \ |supp (f::var \ var)| bij (map_term_pre (id::var \var) f (rrename f) id)" apply (rule iffD2[OF bij_iff]) apply (rule exI[of _ "map_term_pre id (inv f) (rrename (inv f)) id"]) @@ -940,7 +915,7 @@ apply safe lemma R_App_elim: assumes "R (App e1 e2) b" shows "\b1 b2. R e1 b1 \ R e2 b2 \ b = AppB b1 b2" -by (metis App_inject R.simps assms term.distinct(1) term.distinct(4)) +by (metis term.inject(2) R.simps assms term.distinct(1) term.distinct(4)) lemma R_Lam_elim: assumes "R (Lam x e) b"