--- 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]]
--- 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
--- 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 \<bullet> 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 \<bullet> 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
--- 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\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
where
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
- | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+ | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
| t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
-inductive
- typing' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<Turnstile> _ : _" [60,60,60] 60)
-where
- t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T"
- | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2"
- | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2"
-
-inductive
- typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60)
-where
- t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T"
- | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2"
- | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2"
-
-inductive
- typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60)
-and valid' :: "(name\<times>ty) list \<Rightarrow> bool"
-where
- v1[intro]: "valid' []"
- | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)"
- | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T"
- | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"
- | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>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 \<bullet> t1) (p \<bullet> 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