added an LamEx example together with the new nominal infrastructure
(* Title: HOL/Nominal/nominal_thmdecls.ML Author: Julien Narboux, TU Muenchen Author: Christian Urban, TU MuenchenInfrastructure for the lemma collection "eqvts".By attaching [eqvt] or [eqvt_force] to a lemma, it will get stored ina data-slot in the context. Possible modifiers are [... add] and[... del] for adding and deleting, respectively, the lemma from thedata-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 listend;structure NominalThmDecls: NOMINAL_THMDECLS =structstructure 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 stringval 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 endin map_aterms (fn Var (n, ty) => replace n ty | t => t) trmend(* 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;