# HG changeset patch # User Christian Urban # Date 1272179596 -7200 # Node ID 51f411b1197d8532ba23ab2000d1eb0b3d065a7d # Parent 3395e87d94b8d4da56a03cd03d42829a535b61e9 tuned and cleaned diff -r 3395e87d94b8 -r 51f411b1197d Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Sun Apr 25 08:18:06 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Sun Apr 25 09:13:16 2010 +0200 @@ -287,27 +287,13 @@ use "nominal_permeq.ML" setup Nominal_Permeq.setup -ML {* -val add_thms = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; -val exclude_consts = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- - (Scan.repeat (Args.const true))) [] - -val parser = - add_thms -- exclude_consts || - exclude_consts -- add_thms >> swap -*} - method_setup perm_simp = - {* parser >> - (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL - (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} - {* pushes permutations inside *} + {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} + {* pushes permutations inside. *} method_setup perm_strict_simp = - {* parser >> - (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL - (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} - {* pushes permutations inside, raises an error if it cannot solve all permutations *} + {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} + {* pushes permutations inside, raises an error if it cannot solve all permutations. *} declare [[trace_eqvt = true]] diff -r 3395e87d94b8 -r 51f411b1197d Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Sun Apr 25 08:18:06 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Sun Apr 25 09:13:16 2010 +0200 @@ -7,6 +7,11 @@ sig val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic val eqvt_strict_tac: Proof.context -> thm list -> string list -> 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 args_parser: (thm list * string list) context_parser + val trace_eqvt: bool Config.T val setup: theory -> theory end; @@ -157,4 +162,21 @@ val setup = trace_eqvt_setup + +(** methods **) + +val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; +val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- + (Scan.repeat (Args.const true))) [] + +val args_parser = + add_thms_parser -- exclude_consts_parser || + exclude_consts_parser -- add_thms_parser >> swap + +fun perm_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) + +fun perm_strict_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) + end; (* structure *) \ No newline at end of file diff -r 3395e87d94b8 -r 51f411b1197d Nominal-General/nominal_thmdecls.ML --- a/Nominal-General/nominal_thmdecls.ML Sun Apr 25 08:18:06 2010 +0200 +++ b/Nominal-General/nominal_thmdecls.ML Sun Apr 25 09:13:16 2010 +0200 @@ -45,7 +45,8 @@ fun get_ps trm = case trm of - Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm]) + Const (@{const_name permute}, _) $ p $ (Bound _) => + raise TERM ("get_ps called on bound", [trm]) | Const (@{const_name permute}, _) $ p $ _ => [p] | t $ u => get_ps t @ get_ps u | Abs (_, _, t) => get_ps t @@ -59,7 +60,8 @@ | Abs (x, ty, t) => Abs (x, ty, put_p p t) | _ => mk_perm p trm -(* tests whether the lists of ps all agree, and that there is at least one p *) +(* tests whether there is a disagreement between the permutations, + and that there is at least one permutation *) fun is_bad_list [] = true | is_bad_list [_] = false | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true @@ -88,8 +90,7 @@ fun add_raw_thm thm = case prop_of thm of - Const ("==", _) $ _ $ _ => - EqvtRawData.map (Item_Net.update (zero_var_indexes thm)) + Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) val del_raw_thm = EqvtRawData.map o Item_Net.remove; @@ -98,7 +99,7 @@ (** transformation of eqvt lemmas **) -(* transforms equations into the "p o c = c"-form +(* transforms equations into the "p o c == c"-form from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) fun eqvt_transform_eq_tac thm = @@ -113,18 +114,21 @@ fun eqvt_transform_eq ctxt thm = let - val ((p, t), rhs) = apfst dest_perm - (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) - handle TERM _ => error "Eqvt lemma is not of the form p \ c... = c..." + val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) + handle TERM _ => error "Equivariance lemma must be an equality." + val (p, t) = dest_perm lhs + handle TERM _ => error "Equivariance lemma is not of the form p \ c... = c..." + val ps = get_ps rhs handle TERM _ => [] val (c, c') = (head_of t, head_of rhs) + val msg = "Equivariance lemma is not of the right form " in if c <> c' - then error "Eqvt lemma is not of the right form (constants do not agree)" + then error (msg ^ "(constants do not agree).") else if is_bad_list (p::ps) - then error "Eqvt lemma is not of the right form (permutations do not agree)" + then error (msg ^ "(permutations do not agree).") else if not (rhs aconv (put_p p t)) - then error "Eqvt lemma is not of the right form (arguments do not agree)" + then error (msg ^ "(arguments do not agree).") else if is_Const t then safe_mk_equiv thm else @@ -135,14 +139,16 @@ Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |> singleton (ProofContext.export ctxt' ctxt) |> safe_mk_equiv + |> zero_var_indexes end end -(* transforms equations into the "p o c = c"-form +(* transforms equations into the "p o c == c"-form from R x1 ...xn ==> R (p o x1) ... (p o xn) *) -fun eqvt_transform_imp_tac thy p p' thm = +fun eqvt_transform_imp_tac ctxt p p' thm = let + val thy = ProofContext.theory_of ctxt val cp = Thm.cterm_of thy p val cp' = Thm.cterm_of thy (mk_minus p') val thm' = Drule.cterm_instantiate [(cp, cp')] thm @@ -154,18 +160,18 @@ fun eqvt_transform_imp ctxt thm = let - val thy = ProofContext.theory_of ctxt val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) val (c, c') = (head_of prem, head_of concl) val ps = get_ps concl handle TERM _ => [] val p = try hd ps + val msg = "Equivariance lemma is not of the right form " in if c <> c' - then error "Eqvt lemma is not of the right form (constants do not agree)" + then error (msg ^ "(constants do not agree).") else if is_bad_list ps - then error "Eqvt lemma is not of the right form (permutations do not agree)" + then error (msg ^ "(permutations do not agree).") else if not (concl aconv (put_p (the p) prem)) - then error "Eqvt lemma is not of the right form (arguments do not agree)" + then error (msg ^ "(arguments do not agree).") else let val prem' = mk_perm (the p) prem @@ -173,7 +179,7 @@ val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt in Goal.prove ctxt' [] [] goal' - (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) + (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |> singleton (ProofContext.export ctxt' ctxt) |> eqvt_transform_eq ctxt end diff -r 3395e87d94b8 -r 51f411b1197d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Sun Apr 25 08:18:06 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Sun Apr 25 09:13:16 2010 +0200 @@ -126,38 +126,11 @@ typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) where t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" - | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" + | t_App[intro]: "\\ \ t1 : T1 \ T2; \ \ t2 : T1\ \ \ \ App t1 t2 : T2" | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" -inductive - typing' :: "(name\ty) list\lam\ty\bool" ("_ \ _ : _" [60,60,60] 60) -where - t'_Var[intro]: "\valid \; (x,T)\set \\ \ \ \ Var x : T" - | t'_App[intro]: "\\ \ t1 : T1\T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" - | t'_Lam[intro]: "\atom x\\;(x,T1)#\ \ t : T2\ \ \ \ Lam x t : T1\T2" - -inductive - typing2' :: "(name\ty) list\lam\ty\bool" ("_ 2\ _ : _" [60,60,60] 60) -where - t2'_Var[intro]: "\valid \; (x,T)\set \\ \ \ 2\ Var x : T" - | t2'_App[intro]: "\\ 2\ t1 : T1\T2 \ \ 2\ t2 : T1\ \ \ 2\ App t1 t2 : T2" - | t2'_Lam[intro]: "\atom x\\;(x,T1)#\ 2\ t : T2\ \ \ 2\ Lam x t : T1\T2" - -inductive - typing'' :: "(name\ty) list\lam\ty\bool" ("_ |\ _ : _" [60,60,60] 60) -and valid' :: "(name\ty) list \ bool" -where - v1[intro]: "valid' []" - | v2[intro]: "\valid' \;atom x\\\\ valid' ((x,T)#\)" - | t'_Var[intro]: "\valid' \; (x,T)\set \\ \ \ |\ Var x : T" - | t'_App[intro]: "\\ |\ t1 : T1\T2; \ |\ t2 : T1\ \ \ |\ App t1 t2 : T2" - | t'_Lam[intro]: "\atom x\\;(x,T1)#\ |\ t : T2\ \ \ |\ Lam x t : T1\T2" - equivariance valid equivariance typing -equivariance typing' -equivariance typing2' -equivariance typing'' thm valid.eqvt thm typing.eqvt @@ -189,27 +162,9 @@ declare permute_lam_raw.simps[eqvt] declare alpha_gen_eqvt[eqvt] equivariance alpha_lam_raw' + thm eqvts_raw - - -(* HERE *) - -lemma - assumes a: "alpha_lam_raw' t1 t2" - shows "alpha_lam_raw' (p \ t1) (p \ t2)" -using a -apply(induct) -apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*}) -apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*}) -(* -apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*}) -*) -oops - section {* size function *} lemma size_eqvt_raw: @@ -367,6 +322,8 @@ done *) + + end