--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Nominal/nominal_thmdecls.ML Tue Jan 26 20:07:50 2010 +0100
@@ -0,0 +1,171 @@
+(* Title: HOL/Nominal/nominal_thmdecls.ML
+ Author: Julien Narboux, TU Muenchen
+ Author: Christian Urban, TU Muenchen
+
+Infrastructure for the lemma collection "eqvts".
+
+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.
+*)
+
+signature NOMINAL_THMDECLS =
+sig
+ val eqvt_add: attribute
+ val eqvt_del: attribute
+ val eqvt_force_add: attribute
+ val eqvt_force_del: attribute
+ val setup: theory -> theory
+ val get_eqvt_thms: Proof.context -> thm list
+
+end;
+
+structure NominalThmDecls: NOMINAL_THMDECLS =
+struct
+
+structure Data = Generic_Data
+(
+ type T = thm list
+ val empty = []
+ val extend = I
+ val merge = Thm.merge_thms
+)
+
+(* 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 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 prove_eqvt_tac ctxt orig_thm pi pi' =
+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}
+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
+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_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 ^").")
+
+
+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_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 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)
+
+
+end;