--- a/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 09:25:21 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML Wed Feb 03 12:06:10 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 "eqvt"}, content);
end;