--- a/Nominal-General/Nominal2_Eqvt.thy Sun Apr 11 22:48:49 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy Mon Apr 12 13:34:54 2010 +0200
@@ -11,13 +11,6 @@
("nominal_permeq.ML")
begin
-lemma r: "x = x"
-apply(auto)
-done
-
-ML {*
- prop_of @{thm r}
-*}
section {* Logical Operators *}
@@ -266,10 +259,7 @@
atom_eqvt add_perm_eqvt
lemmas [eqvt_raw] =
- permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
-
-thm eqvts
-thm eqvts_raw
+ permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
text {* helper lemmas for the eqvt_tac *}
--- a/Nominal-General/nominal_thmdecls.ML Sun Apr 11 22:48:49 2010 +0200
+++ b/Nominal-General/nominal_thmdecls.ML Mon Apr 12 13:34:54 2010 +0200
@@ -8,7 +8,11 @@
theorem in the eqvts list and also in the eqvts_raw list. For
the latter the theorem is expected to be of the form
- p o (c x1 x2 ...) = c (p o x1) (p o x2) ...
+ p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1)
+
+ or
+
+ c x1 x2 ... ==> c (p o x1) (p o x2) ... (2)
and it is stored in the form
@@ -16,11 +20,8 @@
The [eqvt_raw] attribute just adds the theorem to eqvts_raw.
- TODO:
-
- - deal with eqvt-lemmas of the form
-
- c x1 x2 ... ==> c (p o x1) (p o x2) ..
+ TODO: In case of the form in (2) one should also
+ add the equational form to eqvts
*)
signature NOMINAL_THMDECLS =
@@ -38,9 +39,6 @@
structure Nominal_ThmDecls: NOMINAL_THMDECLS =
struct
-fun mk_equiv r = r RS @{thm eq_reflection};
-fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
-
structure EqvtData = Generic_Data
( type T = thm Item_Net.T;
val empty = Thm.full_rules;
@@ -56,8 +54,8 @@
val eqvts = Item_Net.content o EqvtData.get;
val eqvts_raw = Item_Net.content o EqvtRawData.get;
-val get_eqvts_thms = eqvts o Context.Proof;
-val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
+val get_eqvts_thms = eqvts o Context.Proof;
+val get_eqvts_raw_thms = eqvts_raw o Context.Proof;
val add_thm = EqvtData.map o Item_Net.update;
val del_thm = EqvtData.map o Item_Net.remove;
@@ -66,13 +64,9 @@
| is_equiv _ = false
fun add_raw_thm thm =
-let
- val trm = prop_of thm
-in
- if is_equiv trm
- then (EqvtRawData.map o Item_Net.update) thm
- else raise THM ("Theorem must be a meta-equality", 0, [thm])
-end
+ case prop_of thm of
+ Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)
+ | _ => raise THM ("Theorem must be a meta-equality", 0, [thm])
val del_raw_thm = EqvtRawData.map o Item_Net.remove;
@@ -86,7 +80,7 @@
Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
end
-fun eqvt_transform_tac thm = REPEAT o FIRST'
+fun eq_transform_tac thm = REPEAT o FIRST'
[CHANGED o simp_tac (HOL_basic_ss addsimps @{thms permute_minus_cancel}),
rtac (thm RS @{thm trans}),
rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}]
@@ -104,25 +98,77 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
in
if c <> c'
- then error "eqvt lemma is not of the right form (constants do not agree)"
+ then error "Eqvt lemma is not of the right form (constants do not agree)"
else if eargs' <> map (mk_perm p) eargs
- then error "eqvt lemma is not of the right form (arguments do not agree)"
+ then error "Eqvt lemma is not of the right form (arguments do not agree)"
else if args = []
then thm
else Goal.prove ctxt [p_str] [] goal
- (fn _ => eqvt_transform_tac thm 1)
+ (fn _ => eq_transform_tac thm 1)
+end
+
+
+(* tests whether the lists of pis all agree, and that there is at least one p *)
+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
+
+fun mk_minus p =
+ Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
+
+fun imp_transform_tac thy p p' thm =
+let
+ val cp = Thm.cterm_of thy p
+ val cp' = Thm.cterm_of thy (mk_minus p')
+ val thm' = Drule.cterm_instantiate [(cp, cp')] thm
+ val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)}
+in
+ EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac,
+ rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp]
end
+fun 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, prem_args) = strip_comb prem
+ val (c', concl_args) = strip_comb concl
+ val ps = map (fst o dest_perm) concl_args handle TERM _ => []
+ val p = try hd ps
+in
+ if c <> c'
+ then error "Eqvt lemma is not of the right form (constants do not agree)"
+ else if is_bad_list ps
+ then error "Eqvt lemma is not of the right form (permutations do not agree)"
+ else if concl_args <> map (mk_perm (the p)) prem_args
+ then error "Eqvt lemma is not of the right form (arguments do not agree)"
+ else
+ let
+ val prem' = Const (@{const_name "permute"}, @{typ "perm => bool => bool"}) $ (the p) $ prem
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl))
+ val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt
+ in
+ Goal.prove ctxt' [] [] goal'
+ (fn _ => imp_transform_tac thy (the p) p' thm 1)
+ |> singleton (ProofContext.export ctxt' ctxt)
+ |> transform_eq ctxt
+ end
+end
+
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
+
fun transform addel_fun thm context =
let
val ctxt = Context.proof_of context
in
case (prop_of thm) of
- @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $ _ $ _) =>
- addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
- | @{const "==>"} $ _ $ _ =>
- error ("not yet implemented")
- | _ => raise (error "only (op=) case implemented yet")
+ @{const "Trueprop"} $ (Const (@{const_name "op ="}, _) $
+ (Const (@{const_name "permute"}, _) $ _ $ _) $ _) =>
+ addel_fun (safe_mk_equiv (transform_eq ctxt thm)) context
+ | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) =>
+ addel_fun (safe_mk_equiv (transform_imp ctxt thm)) context
+ | _ => raise error "Only _ = _ and _ ==> _ cases are implemented."
end
val eqvt_add = Thm.declaration_attribute (fn thm => (add_thm thm) o (transform add_raw_thm thm));
@@ -133,10 +179,10 @@
val setup =
Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del)
- (cat_lines ["declaration of equivariance lemmas - they will automtically be",
- "brought into the form p o c = c"]) #>
+ (cat_lines ["Declaration of equivariance lemmas - they will automtically be",
+ "brought into the form p o c == c"]) #>
Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del)
- (cat_lines ["declaration of equivariance lemmas - no",
+ (cat_lines ["Declaration of equivariance lemmas - no",
"transformation is performed"]) #>
PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #>
PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw);
--- a/Nominal/Ex/Lambda.thy Sun Apr 11 22:48:49 2010 +0200
+++ b/Nominal/Ex/Lambda.thy Mon Apr 12 13:34:54 2010 +0200
@@ -132,8 +132,14 @@
atac ])
*}
+ML {* try hd [1] *}
-lemma
+ML {*
+Skip_Proof.cheat_tac
+*}
+
+
+lemma [eqvt]:
assumes a: "valid Gamma"
shows "valid (p \<bullet> Gamma)"
using a
@@ -142,13 +148,8 @@
apply(tactic {* my_tac @{context} @{thms valid.intros} 1 *})
done
-lemma
- "(p \<bullet> valid) = valid"
-oops
-
-lemma temp[eqvt_raw]:
- "(p \<bullet> valid) \<equiv> valid"
-sorry
+thm eqvts
+thm eqvts_raw
inductive
typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
@@ -157,7 +158,7 @@
| 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"
-lemma
+lemma uu[eqvt]:
assumes a: "Gamma \<turnstile> t : T"
shows "(p \<bullet> Gamma) \<turnstile> (p \<bullet> t) : (p \<bullet> T)"
using a
@@ -167,6 +168,9 @@
apply(tactic {* my_tac @{context} @{thms typing.intros} 1 *})
done
+thm eqvts
+thm eqvts_raw
+
declare permute_lam_raw.simps[eqvt]
thm alpha_gen_real_eqvt[no_vars]