diff -r 46cc6708c3b3 -r fa810f01f7b5 Quot/Nominal/nominal_thmdecls.ML --- /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 \ P ==> P" by (simp add: permute_bool_def)}; + +val perm_boolI = + @{lemma "P ==> pi \ 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;