--- a/Quot/Nominal/Abs.thy Wed Feb 03 12:29:45 2010 +0100
+++ b/Quot/Nominal/Abs.thy Wed Feb 03 12:34:01 2010 +0100
@@ -133,17 +133,18 @@
assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
and b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
shows "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
- using b apply -
+ using b
+ apply -
apply(erule exE)
apply(rule_tac x="pi \<bullet> pia" in exI)
apply(simp add: alpha_gen.simps)
apply(erule conjE)+
apply(rule conjI)
apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
- apply(simp add: a[symmetric] atom_eqvt eqvts)
+ apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
apply(rule conjI)
apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
- apply(simp add: a[symmetric] eqvts atom_eqvt)
+ apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
apply(subst permute_eqvt[symmetric])
apply(simp)
done
--- a/Quot/Nominal/Nominal2_Eqvt.thy Wed Feb 03 12:29:45 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy Wed Feb 03 12:34:01 2010 +0100
@@ -6,6 +6,7 @@
theory Nominal2_Eqvt
imports Nominal2_Base
uses ("nominal_thmdecls.ML")
+ ("nominal_permeq.ML")
begin
section {* Logical Operators *}
@@ -43,25 +44,40 @@
by (simp add: permute_bool_def)
lemma all_eqvt:
+ shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
+lemma all_eqvt2:
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
unfolding permute_fun_def permute_bool_def
by (auto, drule_tac x="p \<bullet> x" in spec, simp)
lemma ex_eqvt:
+ shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ unfolding permute_fun_def permute_bool_def
+ by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+lemma ex_eqvt2:
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
unfolding permute_fun_def permute_bool_def
by (auto, rule_tac x="p \<bullet> x" in exI, simp)
lemma ex1_eqvt:
+ shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ unfolding Ex1_def
+ by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt)
+
+lemma ex1_eqvt2:
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
- unfolding Ex1_def ex_eqvt conj_eqvt all_eqvt imp_eqvt eq_eqvt
+ unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt
by simp
lemma the_eqvt:
assumes unique: "\<exists>!x. P x"
shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))"
apply(rule the1_equality [symmetric])
- apply(simp add: ex1_eqvt[symmetric])
+ apply(simp add: ex1_eqvt2[symmetric])
apply(simp add: permute_bool_def unique)
apply(simp add: permute_bool_def)
apply(rule theI'[OF unique])
@@ -78,12 +94,16 @@
unfolding mem_def permute_fun_def by (simp add: Not_eqvt)
lemma Collect_eqvt:
+ shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ unfolding Collect_def permute_fun_def ..
+
+lemma Collect_eqvt2:
shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
unfolding Collect_def permute_fun_def ..
lemma empty_eqvt:
shows "p \<bullet> {} = {}"
- unfolding empty_def Collect_eqvt False_eqvt ..
+ unfolding empty_def Collect_eqvt2 False_eqvt ..
lemma supp_set_empty:
shows "supp {} = {}"
@@ -95,20 +115,20 @@
lemma UNIV_eqvt:
shows "p \<bullet> UNIV = UNIV"
- unfolding UNIV_def Collect_eqvt True_eqvt ..
+ unfolding UNIV_def Collect_eqvt2 True_eqvt ..
lemma union_eqvt:
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
- unfolding Un_def Collect_eqvt disj_eqvt mem_eqvt by simp
+ unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp
lemma inter_eqvt:
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
- unfolding Int_def Collect_eqvt conj_eqvt mem_eqvt by simp
+ unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp
lemma Diff_eqvt:
fixes A B :: "'a::pt set"
shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
- unfolding set_diff_eq Collect_eqvt conj_eqvt Not_eqvt mem_eqvt by simp
+ unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp
lemma Compl_eqvt:
fixes A :: "'a::pt set"
@@ -122,7 +142,7 @@
lemma vimage_eqvt:
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
unfolding vimage_def permute_fun_def [where f=f]
- unfolding Collect_eqvt mem_eqvt ..
+ unfolding Collect_eqvt2 mem_eqvt ..
lemma image_eqvt:
shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
@@ -139,11 +159,6 @@
shows "p \<bullet> finite A = finite (p \<bullet> A)"
unfolding finite_permute_iff permute_bool_def ..
-lemma supp_eqvt: "p \<bullet> supp S = supp (p \<bullet> S)"
- unfolding supp_def
- by (simp only: Collect_eqvt Not_eqvt finite_eqvt eq_eqvt
- permute_eqvt [of p] swap_eqvt permute_minus_cancel)
-
section {* List Operations *}
@@ -205,22 +220,20 @@
section {* Equivariance automation *}
-text {*
- below is a construction site for a conversion that
- pushes permutations into a term as far as possible
-*}
-
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
use "nominal_thmdecls.ML"
-setup "NominalThmDecls.setup"
+setup "Nominal_ThmDecls.setup"
lemmas [eqvt] =
(* connectives *)
eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt
- True_eqvt False_eqvt
+ True_eqvt False_eqvt ex_eqvt all_eqvt
imp_eqvt [folded induct_implies_def]
+ (* nominal *)
+ permute_eqvt supp_eqvt fresh_eqvt
+
(* datatypes *)
permute_prod.simps
fst_eqvt snd_eqvt
@@ -229,142 +242,56 @@
empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
Diff_eqvt Compl_eqvt insert_eqvt
-(* A simple conversion pushing permutations into a term *)
-
-ML {*
-fun OF1 thm1 thm2 = thm2 RS thm1
-
-fun get_eqvt_thms ctxt =
- map (OF1 @{thm eq_reflection}) (NominalThmDecls.get_eqvt_thms ctxt)
-*}
+declare permute_pure [eqvt]
-ML {*
-fun eqvt_conv ctxt ctrm =
- case (term_of ctrm) of
- (Const (@{const_name "permute"}, _) $ _ $ t) =>
- (if is_Const (head_of t)
- then (More_Conv.rewrs_conv (get_eqvt_thms ctxt)
- then_conv eqvt_conv ctxt) ctrm
- else Conv.comb_conv (eqvt_conv ctxt) ctrm)
- | _ $ _ => Conv.comb_conv (eqvt_conv ctxt) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => eqvt_conv ctxt) ctxt ctrm
- | _ => Conv.all_conv ctrm
-*}
+(* thm eqvts *)
-ML {*
-fun eqvt_tac ctxt =
- CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
-*}
-
-lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"
-apply(tactic {* eqvt_tac @{context} 1 *})
-oops
-
-text {*
- Another conversion for pushing permutations into a term.
- It is designed not to apply rules like @{term permute_pure} to
- applications or abstractions, only to constants or free
- variables. Thus permutations are not removed too early, and they
- have a chance to cancel with bound variables.
-*}
+text {* helper lemmas for the eqvt_tac *}
definition
"unpermute p = permute (- p)"
-lemma push_apply:
- fixes f :: "'a::pt \<Rightarrow> 'b::pt" and x :: "'a::pt"
+lemma eqvt_apply:
+ fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ and x :: "'a::pt"
shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
unfolding permute_fun_def by simp
-lemma push_lambda:
+lemma eqvt_lambda:
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
unfolding permute_fun_def unpermute_def by simp
-lemma push_bound:
+lemma eqvt_bound:
shows "p \<bullet> unpermute p x \<equiv> x"
unfolding unpermute_def by simp
-ML {*
-structure PushData = Named_Thms
-(
- val name = "push"
- val description = "push permutations"
-)
-
-local
+use "nominal_permeq.ML"
-fun push_apply_conv ctxt ct =
- case (term_of ct) of
- (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
- let
- val (perm, t) = Thm.dest_comb ct
- val (_, p) = Thm.dest_comb perm
- val (f, x) = Thm.dest_comb t
- val a = ctyp_of_term x;
- val b = ctyp_of_term t;
- val ty_insts = map SOME [b, a]
- val term_insts = map SOME [p, f, x]
- in
- Drule.instantiate' ty_insts term_insts @{thm push_apply}
- end
- | _ => Conv.no_conv ct
-
-fun push_lambda_conv ctxt ct =
- case (term_of ct) of
- (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
- Conv.rewr_conv @{thm push_lambda} ct
- | _ => Conv.no_conv ct
-
-in
-fun push_conv ctxt ct =
- Conv.first_conv
- [ Conv.rewr_conv @{thm push_bound},
- push_apply_conv ctxt
- then_conv Conv.comb_conv (push_conv ctxt),
- push_lambda_conv ctxt
- then_conv Conv.abs_conv (fn (v, ctxt) => push_conv ctxt) ctxt,
- More_Conv.rewrs_conv (PushData.get ctxt),
- Conv.all_conv
- ] ct
-
-fun push_tac ctxt =
- CONVERSION (More_Conv.bottom_conv (fn ctxt => push_conv ctxt) ctxt)
-
-end
-*}
-
-setup PushData.setup
-
-declare permute_pure [THEN eq_reflection, push]
-
-lemma push_eq [THEN eq_reflection, push]:
- "p \<bullet> (op =) = (op =)"
- by (simp add: expand_fun_eq permute_fun_def eq_eqvt)
-
-lemma push_All [THEN eq_reflection, push]:
- "p \<bullet> All = All"
- by (simp add: expand_fun_eq permute_fun_def all_eqvt)
-
-lemma push_Ex [THEN eq_reflection, push]:
- "p \<bullet> Ex = Ex"
- by (simp add: expand_fun_eq permute_fun_def ex_eqvt)
-
-lemma "p \<bullet> (A \<longrightarrow> B = (C::bool))"
-apply (tactic {* push_tac @{context} 1 *})
+lemma "p \<bullet> (A \<longrightarrow> B = C)"
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
oops
-lemma "p \<bullet> (\<lambda>x. A \<longrightarrow> B x = (C::bool)) = foo"
-apply (tactic {* push_tac @{context} 1 *})
+lemma "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
oops
lemma "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
-apply (tactic {* push_tac @{context} 1 *})
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
oops
lemma "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
-apply (tactic {* push_tac @{context} 1 *})
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+oops
+
+lemma "p \<bullet> (\<lambda>q. q \<bullet> (r \<bullet> x)) = foo"
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
oops
+lemma "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
+apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *})
+oops
+
+
end
\ No newline at end of file
--- a/Quot/Nominal/Terms.thy Wed Feb 03 12:29:45 2010 +0100
+++ b/Quot/Nominal/Terms.thy Wed Feb 03 12:34:01 2010 +0100
@@ -646,13 +646,7 @@
quotient_type
qtrm4 = trm4 / alpha4 and
qtrm4list = "trm4 list" / alpha4list
- by (simp_all add: alpha4_equivp alpha4list_equivp)
-
-
-
-
-
-
+ by (simp_all add: alpha4_equivp alpha4list_equivp
datatype rtrm5 =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/nominal_permeq.ML Wed Feb 03 12:34:01 2010 +0100
@@ -0,0 +1,71 @@
+(* Title: nominal_thmdecls.ML
+ Author: Brian Huffman, Christian Urban
+*)
+
+signature NOMINAL_PERMEQ =
+sig
+ val eqvt_tac: Proof.context -> int -> tactic
+
+end;
+
+(* TODO:
+
+ - provide a method interface with the usual add and del options
+
+ - print a warning if for a constant no eqvt lemma is stored
+
+ - there seems to be too much simplified in case of multiple
+ permutations, like
+
+ p o q o r o x
+
+ we usually only want the outermost permutation to "float" in
+*)
+
+
+structure Nominal_Permeq: NOMINAL_PERMEQ =
+struct
+
+local
+
+fun eqvt_apply_conv ctxt ct =
+ case (term_of ct) of
+ (Const (@{const_name "permute"}, _) $ _ $ (_ $ _)) =>
+ let
+ val (perm, t) = Thm.dest_comb ct
+ val (_, p) = Thm.dest_comb perm
+ val (f, x) = Thm.dest_comb t
+ val a = ctyp_of_term x;
+ val b = ctyp_of_term t;
+ val ty_insts = map SOME [b, a]
+ val term_insts = map SOME [p, f, x]
+ in
+ Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
+ end
+ | _ => Conv.no_conv ct
+
+fun eqvt_lambda_conv ctxt ct =
+ case (term_of ct) of
+ (Const (@{const_name "permute"}, _) $ _ $ Abs _) =>
+ Conv.rewr_conv @{thm eqvt_lambda} ct
+ | _ => Conv.no_conv ct
+
+in
+
+fun eqvt_conv ctxt ct =
+ Conv.first_conv
+ [ Conv.rewr_conv @{thm eqvt_bound},
+ eqvt_apply_conv ctxt
+ then_conv Conv.comb_conv (eqvt_conv ctxt),
+ eqvt_lambda_conv ctxt
+ then_conv Conv.abs_conv (fn (v, ctxt) => eqvt_conv ctxt) ctxt,
+ More_Conv.rewrs_conv (Nominal_ThmDecls.get_eqvt_thms ctxt),
+ Conv.all_conv
+ ] ct
+
+fun eqvt_tac ctxt =
+ CONVERSION (More_Conv.bottom_conv (fn ctxt => eqvt_conv ctxt) ctxt)
+
+end
+
+end; (* structure *)
\ No newline at end of file
--- a/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 12:29:45 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 12:34:01 2010 +0100
@@ -1,13 +1,23 @@
-(* Title: HOL/Nominal/nominal_thmdecls.ML
- Author: Julien Narboux, TU Muenchen
- Author: Christian Urban, TU Muenchen
+(* Title: nominal_thmdecls.ML
+ Author: Christian Urban
+
+ Infrastructure for the lemma collection "eqvts".
+
+ Provides the attributes [eqvt] and [eqvt_force], and the theorem
+ list eqvt. In contrast to eqvt-force, the eqvt-lemmas that will be
+ stored are expected to be of the form
-Infrastructure for the lemma collection "eqvts".
+ p o (c x1 x2 ...) = c (p o x1) (p o x2) ...
+
+ and are transformed into the form
+
+ p o c == c
-By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored in
-a data-slot in the context. Possible modifiers are [... add] and
-[... del] for adding and deleting, respectively, the lemma from the
-data-slot.
+ TODO
+
+ - deal with eqvt-lemmas of the for
+
+ c x1 x2 ... ==> c (p o x1) (p o x2) ..
*)
signature NOMINAL_THMDECLS =
@@ -21,151 +31,89 @@
end;
-structure NominalThmDecls: NOMINAL_THMDECLS =
+structure Nominal_ThmDecls: NOMINAL_THMDECLS =
struct
-structure Data = Generic_Data
+structure EqvtData = Generic_Data
(
- type T = thm list
- val empty = []
- val extend = I
- val merge = Thm.merge_thms
-)
+ type T = thm Item_Net.T;
+ val empty = Thm.full_rules;
+ val extend = I;
+ val merge = Item_Net.merge;
+);
+
+val content = Item_Net.content o EqvtData.get;
+val get_eqvt_thms = content o Context.Proof;
-(* Exception for when a theorem does not conform with form of an equivariance lemma. *)
-(* There are two forms: one is an implication (for relations) and the other is an *)
-(* equality (for functions). In the implication-case, say P ==> Q, Q must be equal *)
-(* to P except that every free variable of Q, say x, is replaced by pi o x. In the *)
-(* equality case, say lhs = rhs, the lhs must be of the form pi o t and the rhs must *)
-(* be equal to t except that every free variable, say x, is replaced by pi o x. In *)
-(* the implicational case it is also checked that the variables and permutation fit *)
-(* together, i.e. are of the right "pt_class", so that a stronger version of the *)
-(* equality-lemma can be derived. *)
-exception EQVT_FORM of string
+val add_thm = EqvtData.map o Item_Net.update;
+val del_thm = EqvtData.map o Item_Net.remove;
+
+val add_force_thm = EqvtData.map o Item_Net.update;
+val del_force_thm = EqvtData.map o Item_Net.remove;
+
-val perm_boolE =
- @{lemma "pi \<bullet> P ==> P" by (simp add: permute_bool_def)};
-
-val perm_boolI =
- @{lemma "P ==> pi \<bullet> P" by (simp add: permute_bool_def)};
+fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
+ | dest_perm t = raise TERM("dest_perm", [t])
-fun prove_eqvt_tac ctxt orig_thm pi pi' =
+fun mk_perm p trm =
let
- val mypi = Thm.cterm_of ctxt pi
- val T = fastype_of pi'
- val mypifree = Thm.cterm_of ctxt (Const (@{const_name "uminus"}, T --> T) $ pi')
- val perm_pi_simp = @{thms permute_minus_cancel}
+ val ty = fastype_of trm
in
- EVERY1 [rtac @{thm iffI},
- dtac perm_boolE,
- etac orig_thm,
- dtac (Drule.cterm_instantiate [(mypi, mypifree)] orig_thm),
- rtac perm_boolI,
- full_simp_tac (HOL_basic_ss addsimps perm_pi_simp)]
-end;
-
-fun get_derived_thm ctxt hyp concl orig_thm pi =
- let
- val thy = ProofContext.theory_of ctxt;
- val pi' = Var (pi, @{typ "perm"});
- val lhs = Const (@{const_name "permute"}, @{typ "perm"} --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
- val ([goal_term, pi''], ctxt') = Variable.import_terms false
- [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
- in
- Goal.prove ctxt' [] [] goal_term
- (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
- singleton (ProofContext.export ctxt' ctxt)
- end
-
-(* replaces in t every variable, say x, with pi o x *)
-fun apply_pi trm pi =
-let
- fun replace n ty =
- let
- val c = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty)
- val v1 = Var (pi, @{typ "perm"})
- val v2 = Var (n, ty)
- in
- c $ v1 $ v2
- end
-in
- map_aterms (fn Var (n, ty) => replace n ty | t => t) trm
+ Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
end
-(* returns *the* pi which is in front of all variables, provided there *)
-(* exists such a pi; otherwise raises EQVT_FORM *)
-fun get_pi t thy =
- let fun get_pi_aux s =
- (case s of
- (Const (@{const_name "permute"} ,typrm) $
- (Var (pi,_)) $
- (Var (n,ty))) =>
- if (Sign.of_sort thy (ty, @{sort pt}))
- then [pi]
- else raise
- EQVT_FORM ("Could not find any permutation or an argument is not an instance of pt")
- | Abs (_,_,t1) => get_pi_aux t1
- | (t1 $ t2) => get_pi_aux t1 @ get_pi_aux t2
- | _ => [])
- in
- (* collect first all pi's in front of variables in t and then use distinct *)
- (* to ensure that all pi's must have been the same, i.e. distinct returns *)
- (* a singleton-list *)
- (case (distinct (op =) (get_pi_aux t)) of
- [pi] => pi
- | [] => raise EQVT_FORM "No permutations found"
- | _ => raise EQVT_FORM "All permutation should be the same")
- end;
-
-(* Either adds a theorem (orig_thm) to or deletes one from the equivariance *)
-(* lemma list depending on flag. To be added the lemma has to satisfy a *)
-(* certain form. *)
+fun eqvt_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}]
-fun eqvt_add_del_aux flag orig_thm context =
- let
- val thy = Context.theory_of context
- val thms_to_be_added = (case (prop_of orig_thm) of
- (* case: eqvt-lemma is of the implicational form *)
- (Const("==>", _) $ (Const ("Trueprop",_) $ hyp) $ (Const ("Trueprop",_) $ concl)) =>
- let
- val pi = get_pi concl thy
- in
- if (apply_pi hyp pi = concl)
- then
- (warning ("equivariance lemma of the relational form");
- [orig_thm,
- get_derived_thm (Context.proof_of context) hyp concl orig_thm pi])
- else raise EQVT_FORM "Type Implication"
- end
- (* case: eqvt-lemma is of the equational form *)
- | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
- (Const (@{const_name "permute"},typrm) $ Var (pi, _) $ lhs) $ rhs)) =>
- (if (apply_pi lhs pi) = rhs
- then [orig_thm]
- else raise EQVT_FORM "Type Equality")
- | _ => raise EQVT_FORM "Type unknown")
- in
- fold (fn thm => Data.map (flag thm)) thms_to_be_added context
- end
- handle EQVT_FORM s =>
- error (Display.string_of_thm (Context.proof_of context) orig_thm ^
- " does not comply with the form of an equivariance lemma (" ^ s ^").")
+(* transform equations into the required form *)
+fun transform_eq ctxt thm lhs rhs =
+let
+ val (p, t) = dest_perm lhs
+ val (c, args) = strip_comb t
+ val (c', args') = strip_comb rhs
+ val eargs = map Envir.eta_contract args
+ val eargs' = map Envir.eta_contract args'
+ val p_str = fst (fst (dest_Var p))
+ 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)"
+ else if eargs' <> map (mk_perm p) eargs
+ 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)
+end
+
+fun transform addel_fn thm context =
+let
+ val ctxt = Context.proof_of context
+ val trm = HOLogic.dest_Trueprop (prop_of thm)
+in
+ case trm of
+ Const (@{const_name "op ="}, _) $ lhs $ rhs =>
+ addel_fn (transform_eq ctxt thm lhs rhs RS @{thm eq_reflection}) context
+ | _ => raise (error "no other cases yet implemented")
+end
-val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (Thm.add_thm));
-val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (Thm.del_thm));
+val eqvt_add = Thm.declaration_attribute (transform add_thm);
+val eqvt_del = Thm.declaration_attribute (transform del_thm);
-val eqvt_force_add = Thm.declaration_attribute (Data.map o Thm.add_thm);
-val eqvt_force_del = Thm.declaration_attribute (Data.map o Thm.del_thm);
-
-val get_eqvt_thms = Context.Proof #> Data.get;
+val eqvt_force_add = Thm.declaration_attribute add_force_thm;
+val eqvt_force_del = Thm.declaration_attribute del_force_thm;
val setup =
- Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
- "equivariance theorem declaration"
- #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
- "equivariance theorem declaration (without checking the form of the lemma)"
- #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get)
+ 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"]) #>
+ Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del)
+ (cat_lines ["declaration of equivariance lemmas - they will will be",
+ "added/deleted directly to the eqvt thm-list"]) #>
+ PureThy.add_thms_dynamic (@{binding "eqvts"}, content);
end;