# HG changeset patch # User Christian Urban # Date 1394702491 0 # Node ID b52e8651591fa362279c696d1bb4f500d7e88f18 # Parent 040519ec99e95adb1d2ded1e9190e5131e3354e8 updated to Isabelle changes diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/CPS/CPS2_DanvyNielsen.thy --- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Thu Mar 13 09:21:31 2014 +0000 @@ -98,8 +98,8 @@ apply blast --"" apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh) - apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)") - apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") + apply (subgoal_tac "Lam b (Sum_Type.projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.projr (CPSv_CPS_sumC (Inr M))<(a~)>)") + apply (subgoal_tac "Lam ba (Sum_Type.projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)") apply (simp only:) apply (erule Abs_lst1_fcb) apply (simp add: Abs_fresh_iff) diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Ex/Lambda.thy Thu Mar 13 09:21:31 2014 +0000 @@ -593,7 +593,7 @@ "transdb (Var x) l = vindex l x 0" | "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\d1. Option.bind (transdb t2 xs) (\d2. Some (DBApp d1 d2)))" -| "x \ set xs \ transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))" +| "x \ set xs \ transdb (Lam [x].t) xs = Option.map_option DBLam (transdb t (x # xs))" apply(simp add: eqvt_def transdb_graph_aux_def) apply(rule TrueI) apply (case_tac x) diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/Pi.thy --- a/Nominal/Ex/Pi.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Ex/Pi.thy Thu Mar 13 09:21:31 2014 +0000 @@ -130,20 +130,20 @@ lemma testl: assumes a: "\y. f = Inl y" - shows "(p \ (Sum_Type.Projl f)) = Sum_Type.Projl (p \ f)" + shows "(p \ (Sum_Type.projl f)) = Sum_Type.projl (p \ f)" using a by auto lemma testrr: assumes a: "\y. f = Inr (Inr y)" - shows "(p \ (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \ f))" + shows "(p \ (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \ f))" using a by auto lemma testlr: assumes a: "\y. f = Inr (Inl y)" - shows "(p \ (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \ f))" + shows "(p \ (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \ f))" using a by auto -nominal_primrec (default "sum_case (\x. Inl undefined) (sum_case (\x. Inr (Inl undefined)) (\x. Inr (Inr undefined)))") +nominal_primrec (default "case_sum (\x. Inl undefined) (case_sum (\x. Inr (Inl undefined)) (\x. Inr (Inr undefined)))") subsGuard_mix :: "guardedTerm_mix \ name \ name \ guardedTerm_mix" ("_[_::=\\_]" [100, 100, 100] 100) and subsList_mix :: "sumList_mix \ name \ name \ sumList_mix" ("_[_::=\\_]" [100, 100, 100] 100) and subs_mix :: "piMix \ name \ name \ piMix" ("_[_::=\_]" [100, 100, 100] 100) @@ -240,33 +240,33 @@ apply (metis Inr_not_Inl) apply (metis Inr_inject Inr_not_Inl) apply (metis Inr_inject Inr_not_Inl) -apply (rule_tac x="<\a>\Sum_Type.Projr - (Sum_Type.Projr +apply (rule_tac x="<\a>\Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="Sum_Type.Projr - (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \\ - Sum_Type.Projr - (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) +apply (rule_tac x="Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \\ + Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="[(a[xb:::=y])\\(bb[xb:::=y])]Sum_Type.Projr - (Sum_Type.Projr +apply (rule_tac x="[(a[xb:::=y])\\(bb[xb:::=y])]Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="\\{Sum_Type.Projl - (Sum_Type.Projr +apply (rule_tac x="\\{Sum_Type.projl + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="\(a[xb:::=y])?\.Sum_Type.Projr - (Sum_Type.Projr +apply (rule_tac x="\(a[xb:::=y])?\.Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) apply clarify @@ -333,33 +333,33 @@ apply (metis Inr_not_Inl) apply (metis Inr_inject Inr_not_Inl) apply (metis Inr_inject Inr_not_Inl) -apply (rule_tac x="<\a>\Sum_Type.Projr - (Sum_Type.Projr +apply (rule_tac x="<\a>\Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="Sum_Type.Projr - (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \\ - Sum_Type.Projr - (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) +apply (rule_tac x="Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \\ + Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="[(a[xb:::=y])\\(bb[xb:::=y])]Sum_Type.Projr - (Sum_Type.Projr +apply (rule_tac x="[(a[xb:::=y])\\(bb[xb:::=y])]Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="\\{Sum_Type.Projl - (Sum_Type.Projr +apply (rule_tac x="\\{Sum_Type.projl + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="\(a[xb:::=y])?\.Sum_Type.Projr - (Sum_Type.Projr +apply (rule_tac x="\(a[xb:::=y])?\.Sum_Type.projr + (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) apply clarify diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/TypeSchemes2.thy --- a/Nominal/Ex/TypeSchemes2.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Ex/TypeSchemes2.thy Thu Mar 13 09:21:31 2014 +0000 @@ -41,27 +41,27 @@ lemma TEST1: assumes "x = Inl y" - shows "(p \ Sum_Type.Projl x) = Sum_Type.Projl (p \ x)" + shows "(p \ Sum_Type.projl x) = Sum_Type.projl (p \ x)" using assms by simp lemma TEST2: assumes "x = Inr y" - shows "(p \ Sum_Type.Projr x) = Sum_Type.Projr (p \ x)" + shows "(p \ Sum_Type.projr x) = Sum_Type.projr (p \ x)" using assms by simp lemma test: assumes a: "\y. f x = Inl y" - shows "(p \ (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \ f) (p \ x))" -using a -by (metis Inl_eqvt Projl_Inl permute_fun_app_eq) + shows "(p \ (Sum_Type.projl (f x))) = Sum_Type.projl ((p \ f) (p \ x))" +using a TEST1 +by (metis eqvt_bound eqvt_lambda permute_eq_iff) lemma test2: assumes a: "\y. f x = Inl y" - shows "(p \ (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \ (f x))" + shows "(p \ (Sum_Type.projl (f x))) = Sum_Type.projl (p \ (f x))" using a by clarsimp -nominal_primrec (default "sum_case (\x. Inl undefined) (\x. Inr undefined)") +nominal_primrec (default "case_sum (\x. Inl undefined) (\x. Inr undefined)") subst :: "(name \ ty) list \ ty \ ty" and substs :: "(name \ ty) list \ tys \ tys" where @@ -103,8 +103,8 @@ apply clarify apply (rule the1_equality) apply blast apply assumption -apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\, T1)))) - (Sum_Type.Projl (subst_substs_sum (Inl (\, T2)))))" in exI) +apply (rule_tac x="(Fun (Sum_Type.projl (subst_substs_sum (Inl (\, T1)))) + (Sum_Type.projl (subst_substs_sum (Inl (\, T2)))))" in exI) apply clarify apply (rule the1_equality) apply blast apply assumption diff -r 040519ec99e9 -r b52e8651591f Nominal/GPerm.thy --- a/Nominal/GPerm.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/GPerm.thy Thu Mar 13 09:21:31 2014 +0000 @@ -53,7 +53,7 @@ by (rule perm_eq_equivp) definition perm_add_raw where - "perm_add_raw p q = map (map_pair id (perm_apply p)) q @ [a\p. fst a \ fst ` set q]" + "perm_add_raw p q = map (map_prod id (perm_apply p)) q @ [a\p. fst a \ fst ` set q]" lemma perm_apply_del[simp]: "e \ b \ perm_apply [a\l. fst a \ b] e = perm_apply l e" @@ -146,7 +146,7 @@ lemma valid_perm_add_minus: "valid_perm a \ perm_apply (map swap_pair a) (perm_apply a e) = e" apply (auto simp add: filter_map_swap_pair filter_eq_nil filter_rev_eq_nil perm_apply_def split: list.split) apply (metis filter_eq_nil(2) neq_Nil_conv valid_perm_def) - apply (metis hd.simps hd_in_set image_eqI list.simps(2) member_project project_set snd_conv) + apply (metis list.sel(1) hd_in_set image_eqI list.simps(2) member_project project_set snd_conv) apply (frule filter_fst_eq(1)) apply (frule filter_fst_eq(2)) apply (auto simp add: swap_pair_def) @@ -162,9 +162,9 @@ "perm_eq x y \ perm_eq (map swap_pair x) (map swap_pair y)" by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def) -lemma fst_snd_map_pair[simp]: - "fst ` map_pair f g ` set l = f ` fst ` set l" - "snd ` map_pair f g ` set l = g ` snd ` set l" +lemma fst_snd_map_prod[simp]: + "fst ` map_prod f g ` set l = f ` fst ` set l" + "snd ` map_prod f g ` set l = g ` snd ` set l" by (induct l) auto lemma fst_diff[simp]: diff -r 040519ec99e9 -r b52e8651591f Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Nominal2.thy Thu Mar 13 09:21:31 2014 +0000 @@ -399,8 +399,8 @@ val qperm_bns = map #qconst qperm_bns_info val _ = trace_msg (K "Lifting of theorems...") - val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def - prod.cases} + val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def rel_prod_def + prod.case} val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, @@ -747,6 +747,3 @@ end - - - diff -r 040519ec99e9 -r b52e8651591f Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Nominal2_Abs.thy Thu Mar 13 09:21:31 2014 +0000 @@ -479,14 +479,14 @@ shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" and "(op= ===> op= ===> alpha_abs_res) Pair Pair" and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" - unfolding fun_rel_def + unfolding rel_fun_def by (auto intro: alphas_abs_refl) lemma [quot_respect]: shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute" and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" - unfolding fun_rel_def + unfolding rel_fun_def by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) lemma Abs_eq_iff: @@ -1045,18 +1045,18 @@ definition prod_alpha :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b \ 'a \ 'b \ bool)" where - "prod_alpha = prod_rel" + "prod_alpha = rel_prod" lemma [quot_respect]: - shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" - unfolding fun_rel_def - unfolding prod_rel_def + shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv" + unfolding rel_fun_def + unfolding rel_prod_def by auto lemma [quot_preserve]: assumes q1: "Quotient3 R1 abs1 rep1" and q2: "Quotient3 R2 abs2 rep2" - shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv" + shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_prod rep1 rep2 ---> id) prod_fv = prod_fv" by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [mono]: @@ -1067,7 +1067,7 @@ lemma [eqvt]: shows "p \ prod_alpha A B x y = prod_alpha (p \ A) (p \ B) (p \ x) (p \ y)" unfolding prod_alpha_def - unfolding prod_rel_def + unfolding rel_prod_def by (perm_simp) (rule refl) lemma [eqvt]: diff -r 040519ec99e9 -r b52e8651591f Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/Nominal2_Base.thy Thu Mar 13 09:21:31 2014 +0000 @@ -618,7 +618,7 @@ lemma permute_fset_rsp[quot_respect]: shows "(op = ===> list_eq ===> list_eq) permute permute" - unfolding fun_rel_def + unfolding rel_fun_def by (simp add: set_eqvt[symmetric]) instantiation fset :: (pt) pt @@ -1191,8 +1191,8 @@ subsubsection {* Equivariance for @{typ "'a option"} *} -lemma option_map_eqvt[eqvt]: - shows "p \ (Option.map f x) = Option.map (p \ f) (p \ x)" +lemma map_option_eqvt[eqvt]: + shows "p \ (map_option f x) = map_option (p \ f) (p \ x)" by (cases x) (simp_all) @@ -1565,21 +1565,21 @@ proof - { assume "a \ supp p" "a \ supp q" then have "(p + q) \ a = (q + p) \ a" - by (simp add: supp_perm) + by (simp add: supp_perm) } moreover { assume a: "a \ supp p" "a \ supp q" then have "p \ a \ supp p" by (simp add: supp_perm) then have "p \ a \ supp q" using asm by auto with a have "(p + q) \ a = (q + p) \ a" - by (simp add: supp_perm) + by (simp add: supp_perm) } moreover { assume a: "a \ supp p" "a \ supp q" then have "q \ a \ supp q" by (simp add: supp_perm) then have "q \ a \ supp p" using asm by auto with a have "(p + q) \ a = (q + p) \ a" - by (simp add: supp_perm) + by (simp add: supp_perm) } ultimately show "(p + q) \ a = (q + p) \ a" using asm by blast @@ -2793,19 +2793,19 @@ by (auto simp: swap_atom) moreover { have "{q \ a, p \ a} \ insert a bs \ p \ insert a bs" - using ** - apply (auto simp: supp_perm insert_eqvt) - apply (subgoal_tac "q \ a \ bs \ p \ bs") - apply(auto)[1] - apply(subgoal_tac "q \ a \ {a. q \ a \ a}") - apply(blast) - apply(simp) - done + using ** + apply (auto simp: supp_perm insert_eqvt) + apply (subgoal_tac "q \ a \ bs \ p \ bs") + apply(auto)[1] + apply(subgoal_tac "q \ a \ {a. q \ a \ a}") + apply(blast) + apply(simp) + done then have "supp (q \ a \ p \ a) \ insert a bs \ p \ insert a bs" unfolding supp_swap by auto moreover have "supp q \ insert a bs \ p \ insert a bs" - using ** by (auto simp: insert_eqvt) + using ** by (auto simp: insert_eqvt) ultimately have "supp q' \ insert a bs \ p \ insert a bs" unfolding q'_def using supp_plus_perm by blast @@ -2862,19 +2862,19 @@ unfolding q'_def using 2 * `a \ set bs` by (auto simp: swap_atom) moreover { have "{q \ a, p \ a} \ set (a # bs) \ p \ (set (a # bs))" - using ** - apply (auto simp: supp_perm insert_eqvt) - apply (subgoal_tac "q \ a \ set bs \ p \ set bs") - apply(auto)[1] - apply(subgoal_tac "q \ a \ {a. q \ a \ a}") - apply(blast) - apply(simp) - done + using ** + apply (auto simp: supp_perm insert_eqvt) + apply (subgoal_tac "q \ a \ set bs \ p \ set bs") + apply(auto)[1] + apply(subgoal_tac "q \ a \ {a. q \ a \ a}") + apply(blast) + apply(simp) + done then have "supp (q \ a \ p \ a) \ set (a # bs) \ p \ set (a # bs)" unfolding supp_swap by auto moreover have "supp q \ set (a # bs) \ p \ (set (a # bs))" - using ** by (auto simp: insert_eqvt) + using ** by (auto simp: insert_eqvt) ultimately have "supp q' \ set (a # bs) \ p \ (set (a # bs))" unfolding q'_def using supp_plus_perm by blast diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_basics.ML --- a/Nominal/nominal_basics.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_basics.ML Thu Mar 13 09:21:31 2014 +0000 @@ -35,8 +35,8 @@ val mk_All: (string * typ) -> term -> term val mk_exists: (string * typ) -> term -> term - val sum_case_const: typ -> typ -> typ -> term - val mk_sum_case: term -> term -> term + val case_sum_const: typ -> typ -> typ -> term + val mk_case_sum: term -> term -> term val mk_equiv: thm -> thm val safe_mk_equiv: thm -> thm @@ -148,15 +148,15 @@ fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) -fun sum_case_const ty1 ty2 ty3 = - Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) +fun case_sum_const ty1 ty2 ty3 = + Const (@{const_name case_sum}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) -fun mk_sum_case trm1 trm2 = +fun mk_case_sum trm1 trm2 = let val ([ty1], ty3) = strip_type (fastype_of trm1) val ty2 = domain_type (fastype_of trm2) in - sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 + case_sum_const ty1 ty2 ty3 $ trm1 $ trm2 end fun mk_equiv r = r RS @{thm eq_reflection} diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_dt_alpha.ML Thu Mar 13 09:21:31 2014 +0000 @@ -463,7 +463,7 @@ fun cases_tac intros ctxt = let - val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def} + val prod_simps = @{thms split_conv prod_alpha_def rel_prod_def} val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac @@ -504,7 +504,7 @@ in resolve_tac prems' 1 end) ctxt - val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas} + val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_def alphas} in EVERY' [ etac exi_neg, @@ -556,7 +556,7 @@ fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let - val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def} + val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_def} in resolve_tac intros THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' @@ -570,7 +570,7 @@ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) end - + fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result @@ -685,7 +685,7 @@ val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns val simpset = - put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} + put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct @@ -706,8 +706,8 @@ val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val simpset = - put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def - permute_prod_def prod.cases prod.recs}) + put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_def + permute_prod_def prod.case prod.rec}) val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset in @@ -719,9 +719,9 @@ fun raw_constr_rsp_tac ctxt alpha_intros simps = let - val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms fun_rel_def} - val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def prod_rel_def - prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps + val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def} + val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_def + prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps in asm_full_simp_tac pre_simpset THEN' REPEAT o (resolve_tac @{thms allI impI}) @@ -738,15 +738,15 @@ NONE => HOLogic.eq_const ty | SOME alpha => alpha - fun fun_rel_app (t1, t2) = - Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2 + fun rel_fun_app (t1, t2) = + Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2 fun prep_goal trm = trm |> strip_type o fastype_of |> (fn (tys, ty) => tys @ [ty]) |> map lookup - |> foldr1 fun_rel_app + |> foldr1 rel_fun_app |> (fn t => t $ trm $ trm) |> Syntax.check_term ctxt |> HOLogic.mk_Trueprop @@ -762,7 +762,7 @@ val rsp_equivp = @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q" - by (simp only: fun_rel_def equivp_def, metis)} + by (simp only: rel_fun_def equivp_def, metis)} (* we have to reorder the alpha_bn_imps theorems in order @@ -791,7 +791,7 @@ (* rsp for permute_bn functions *) val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f" - by (simp add: fun_rel_def)} + by (simp add: rel_fun_def)} fun raw_prove_perm_bn_tac alpha_result simps ctxt = SUBPROOF (fn {prems, context, ...} => @@ -819,7 +819,7 @@ val perm_bn_ty = range_type o range_type o fastype_of val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms) - val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt + val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, @{typ perm}) fun mk_prop t = @@ -844,7 +844,7 @@ (* transformation of the natural rsp-lemmas into standard form *) val fun_rsp = @{lemma - "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} + "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: rel_fun_def)} fun mk_funs_rsp ctxt thm = thm @@ -855,7 +855,7 @@ val permute_rsp = @{lemma "(!x y p. R x y --> R (permute p x) (permute p y)) - ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)} + ==> ((op =) ===> R ===> R) permute permute" by (simp add: rel_fun_def)} fun mk_alpha_permute_rsp ctxt thm = thm diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_dt_quot.ML Thu Mar 13 09:21:31 2014 +0000 @@ -303,8 +303,8 @@ val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} -val thms3 = @{thms alphas prod_alpha_def prod_fv.simps prod_rel_def permute_prod_def - prod.recs prod.cases prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} +val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_def permute_prod_def + prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps fv_bn_eqvts qinduct bclausess ctxt = @@ -355,7 +355,7 @@ val props = map mk_goal qbns val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @ - @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) + @{thms set_simps set_append finite_insert finite.emptyI finite_Un})) in induct_prove qtys props qinduct (K ss_tac) ctxt end @@ -532,7 +532,7 @@ |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |> HOLogic.mk_Trueprop - val ss = fprops @ @{thms set.simps set_append union_eqvt} + val ss = fprops @ @{thms set_simps set_append union_eqvt} @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset fresh_star_set} @@ -580,7 +580,7 @@ REPEAT o (etac @{thm conjE}), REPEAT o (dtac setify), full_simp_tac (put_simpset HOL_basic_ss ctxt'' - addsimps @{thms set_append set.simps})]) abs_eq_thms ctxt' + addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt' val (abs_eqs, peqs) = split_filter is_abs_eq eqs diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_function_core.ML --- a/Nominal/nominal_function_core.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_function_core.ML Thu Mar 13 09:21:31 2014 +0000 @@ -91,14 +91,14 @@ (* Theory dependencies. *) val acc_induct_rule = @{thm accp_induct_rule} -val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence} -val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness} -val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff} +val ex1_implies_ex = @{thm Fun_Def.fundef_ex1_existence} +val ex1_implies_un = @{thm Fun_Def.fundef_ex1_uniqueness} +val ex1_implies_iff = @{thm Fun_Def.fundef_ex1_iff} val acc_downward = @{thm accp_downward} val accI = @{thm accp.accI} val case_split = @{thm HOL.case_split} -val fundef_default_value = @{thm FunDef.fundef_default_value} +val fundef_default_value = @{thm Fun_Def.fundef_default_value} val not_acc_down = @{thm not_accp_down} @@ -657,7 +657,7 @@ fun define_function fdefname (fname, mixfix) domT ranT G default lthy = let val f_def = - Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) + Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |> Syntax.check_term lthy in @@ -881,8 +881,8 @@ (** Termination rule **) val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} -val wf_in_rel = @{thm FunDef.wf_in_rel} -val in_rel_def = @{thm FunDef.in_rel_def} +val wf_in_rel = @{thm Fun_Def.wf_in_rel} +val in_rel_def = @{thm Fun_Def.in_rel_def} fun mk_nest_term_case thy globals R' ihyp clause = let @@ -943,7 +943,7 @@ val R' = Free ("R", fastype_of R) val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) - val inrel_R = Const (@{const_name FunDef.in_rel}, + val inrel_R = Const (@{const_name Fun_Def.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_induct.ML --- a/Nominal/nominal_induct.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_induct.ML Thu Mar 13 09:21:31 2014 +0000 @@ -66,7 +66,7 @@ let val tune = if internal then Name.internal - else fn x => the_default x (try Name.dest_internal x); + else perhaps (try Name.dest_internal); val n = length xs; fun rename prem = let diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_library.ML Thu Mar 13 09:21:31 2014 +0000 @@ -52,7 +52,7 @@ val supp_rel_ty: typ -> typ val supp_rel_const: typ -> term val mk_supp_rel_ty: typ -> term -> term -> term - val mk_supp_rel: term -> term -> term + val mk_supp_rel: term -> term -> term val supports_const: typ -> term val mk_supports_ty: typ -> term -> term -> term @@ -359,7 +359,7 @@ val size_ss = simpset_of (put_simpset HOL_ss @{context} addsimprocs [@{simproc natless_cancel_numerals}] - addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral + addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral zero_less_Suc prod.size(1) mult_Suc_right}) val natT = @{typ nat} @@ -374,7 +374,7 @@ end fun snd_const T1 T2 = - Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2) + Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) fun mk_measure_trm f ctxt T = @@ -390,7 +390,7 @@ fun mk_size_measure T = case T of (Type (@{type_name Sum_Type.sum}, [T1, T2])) => - SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) + Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | (Type (@{type_name Product_Type.prod}, [T1, T2])) => HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) | _ => HOLogic.size_const T @@ -406,7 +406,7 @@ fun mk_size_measure T = case T of (Type (@{type_name Sum_Type.sum}, [T1, T2])) => - SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) + Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | (Type (@{type_name Product_Type.prod}, [T1, T2])) => prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) | _ => HOLogic.size_const T @@ -512,4 +512,4 @@ end (* structure *) -open Nominal_Library; \ No newline at end of file +open Nominal_Library; diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_mutual.ML --- a/Nominal/nominal_mutual.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_mutual.ML Thu Mar 13 09:21:31 2014 +0000 @@ -13,7 +13,6 @@ signature NOMINAL_FUNCTION_MUTUAL = sig - val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((string * typ) * mixfix) list @@ -22,10 +21,8 @@ -> ((thm (* goalstate *) * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *) ) * local_theory) - end - structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = struct @@ -95,8 +92,8 @@ val dresultTs = distinct (op =) resultTs val n' = length dresultTs - val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs - val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs + val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs + val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs val fsum_type = ST --> RST @@ -108,7 +105,7 @@ val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 - val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) + val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) val rew = (n, fold_rev lambda vars f_exp) @@ -124,8 +121,8 @@ val rhs' = rhs |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t) in - (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), - Envir.beta_norm (SumTree.mk_inj RST n' i' rhs')) + (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), + Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs')) end val qglrs = map convert_eqs fqgars @@ -205,8 +202,8 @@ |> export end -val inl_perm = @{lemma "x = Inl y ==> Sum_Type.Projl (permute p x) = permute p (Sum_Type.Projl x)" by simp} -val inr_perm = @{lemma "x = Inr y ==> Sum_Type.Projr (permute p x) = permute p (Sum_Type.Projr x)" by simp} +val inl_perm = @{lemma "x = Inl y ==> projl (permute p x) = permute p (projl x)" by simp} +val inr_perm = @{lemma "x = Inr y ==> projr (permute p x) = permute p (projr x)" by simp} fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, _) import (export : thm -> thm) sum_psimp_eq = @@ -224,13 +221,12 @@ val ([p], ctxt'') = ctxt' |> fold Variable.declare_term args - |> Variable.variant_fixes ["p"] + |> Variable.variant_fixes ["p"] val p = Free (p, @{typ perm}) val simpset = put_simpset HOL_basic_ss ctxt'' addsimps - @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ - @{thms Projr.simps Projl.simps} @ + @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric] sum.sel} @ [(cond MRS eqvt_thm) RS @{thm sym}] @ [inl_perm, inr_perm, simp] val goal_lhs = mk_perm p (list_comb (f, args)) @@ -272,21 +268,21 @@ end val Ps = map2 mk_P parts newPs - val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps + val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps val induct_inst = Thm.forall_elim (cert case_exp) induct - |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) + |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) fun project rule (MutualPart {cargTs, i, ...}) k = let val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) - val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) + val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) in (rule |> Thm.forall_elim (cert inj) - |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt) + |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |> fold_rev (Thm.forall_intr o cert) (afs @ newPs), k + length cargTs) end @@ -427,13 +423,13 @@ let val (tys, ty) = strip_type T val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty) - val inj_fun = absdummy dummyT (SumTree.mk_inj RST n' i' (Bound 0)) + val inj_fun = absdummy dummyT (Sum_Tree.mk_inj RST n' i' (Bound 0)) in Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var) end - val sum_case_exp = map mk_cases parts - |> SumTree.mk_sumcases RST + val case_sum_exp = map mk_cases parts + |> Sum_Tree.mk_sumcases RST val (G_name, G_type) = dest_Free G val G_name_aux = G_name ^ "_aux" @@ -441,7 +437,7 @@ val GIntros_aux = GIntro_thms |> map prop_of |> map (Term.subst_free subst) - |> map (subst_all sum_case_exp) + |> map (subst_all case_sum_exp) val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' @@ -456,10 +452,10 @@ fun mk_inj_goal (MutualPart {i', ...}) = let - val injs = SumTree.mk_inj ST n' i' (Bound 0) + val injs = Sum_Tree.mk_inj ST n' i' (Bound 0) val projs = y - |> SumTree.mk_proj RST n' i' - |> SumTree.mk_inj RST n' i' + |> Sum_Tree.mk_proj RST n' i' + |> Sum_Tree.mk_inj RST n' i' in Const (@{const_name "All"}, dummyT) $ absdummy dummyT (HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y))) @@ -474,7 +470,7 @@ val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem) |> all x |> all y - val simp_thms = @{thms Projl.simps Projr.simps sum.inject sum.cases sum.distinct o_apply} + val simp_thms = @{thms sum.sel sum.inject sum.case sum.distinct o_apply} val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_permeq.ML --- a/Nominal/nominal_permeq.ML Mon Jan 13 15:42:10 2014 +0000 +++ b/Nominal/nominal_permeq.ML Thu Mar 13 09:21:31 2014 +0000 @@ -22,8 +22,8 @@ val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic - val perm_simp_meth: thm list * string list -> Proof.context -> Method.method - val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method + val perm_simp_meth: thm list * string list -> Proof.context -> Proof.method + val perm_strict_simp_meth: thm list * string list -> Proof.context -> Proof.method val args_parser: (thm list * string list) context_parser val trace_eqvt: bool Config.T @@ -219,9 +219,9 @@ Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- - (Scan.repeat (Args.const true))) [] + (Scan.repeat (Args.const {proper = true, strict = true}))) [] -val args_parser = add_thms_parser -- exclude_consts_parser +val args_parser = add_thms_parser -- exclude_consts_parser fun perm_simp_meth (thms, consts) ctxt = SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt (eqvt_relaxed_config addpres thms addexcls consts)))