# HG changeset patch # User Christian Urban # Date 1240699379 -7200 # Node ID 2bbc22bd6a9519da5faf98bba0958247dded566f # Parent 2a22c6613dcf150973f37531a8c03b782a8bd738# Parent 047fa04a9fe8a4040b5e8d425b4feb794af4cd75 merged diff -r 2a22c6613dcf -r 2bbc22bd6a95 src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy Sat Apr 25 23:42:30 2009 +0200 +++ b/src/HOL/Nominal/Examples/Fsub.thy Sun Apr 26 00:42:59 2009 +0200 @@ -245,7 +245,7 @@ apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs]) done -lemma ty_vrs_fresh[fresh]: +lemma ty_vrs_fresh: fixes x::"vrs" and T::"ty" shows "x \ T" @@ -422,7 +422,7 @@ by (nominal_induct T avoiding: X T' rule: ty.strong_induct) (perm_simp add: fresh_left)+ -lemma type_subst_fresh[fresh]: +lemma type_subst_fresh: fixes X::"tyvrs" assumes "X \ T" and "X \ P" shows "X \ T[Y \ P]\<^sub>\" @@ -430,7 +430,7 @@ by (nominal_induct T avoiding: X Y P rule:ty.strong_induct) (auto simp add: abs_fresh) -lemma fresh_type_subst_fresh[fresh]: +lemma fresh_type_subst_fresh: assumes "X\T'" shows "X\T[X \ T']\<^sub>\" using assms @@ -458,18 +458,19 @@ | "(VarB X U)[Y \ T]\<^sub>b = VarB X (U[Y \ T]\<^sub>\)" by auto -lemma binding_subst_fresh[fresh]: +lemma binding_subst_fresh: fixes X::"tyvrs" assumes "X \ a" and "X \ P" shows "X \ a[Y \ P]\<^sub>b" using assms -by (nominal_induct a rule:binding.strong_induct) - (auto simp add: freshs) +by (nominal_induct a rule: binding.strong_induct) + (auto simp add: type_subst_fresh) -lemma binding_subst_identity: "X \ B \ B[X \ U]\<^sub>b = B" - by (induct B rule: binding.induct) - (simp_all add: fresh_atm type_subst_identity) +lemma binding_subst_identity: + shows "X \ B \ B[X \ U]\<^sub>b = B" +by (induct B rule: binding.induct) + (simp_all add: fresh_atm type_subst_identity) consts subst_tyc :: "env \ tyvrs \ ty \ env" ("_[_ \ _]\<^sub>e" [100,100,100] 100) @@ -478,14 +479,14 @@ "([])[Y \ T]\<^sub>e= []" "(B#\)[Y \ T]\<^sub>e = (B[Y \ T]\<^sub>b)#(\[Y \ T]\<^sub>e)" -lemma ctxt_subst_fresh'[fresh]: +lemma ctxt_subst_fresh': fixes X::"tyvrs" assumes "X \ \" and "X \ P" shows "X \ \[Y \ P]\<^sub>e" using assms by (induct \) - (auto simp add: fresh_list_cons freshs) + (auto simp add: fresh_list_cons binding_subst_fresh) lemma ctxt_subst_mem_TVarB: "TVarB X T \ set \ \ TVarB X (T[Y \ U]\<^sub>\) \ set (\[Y \ U]\<^sub>e)" by (induct \) auto @@ -1188,8 +1189,8 @@ using assms by (induct, auto) nominal_inductive typing - by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain - simp: abs_fresh fresh_prod fresh_atm freshs valid_ty_domain_fresh fresh_trm_domain) +by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain type_subst_fresh + simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_domain_fresh fresh_trm_domain) lemma ok_imp_VarB_closed_in: assumes ok: "\ \ ok" diff -r 2a22c6613dcf -r 2bbc22bd6a95 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Apr 25 23:42:30 2009 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Apr 26 00:42:59 2009 +0200 @@ -1,12 +1,12 @@ (* Authors: Julien Narboux and Christian Urban This file introduces the infrastructure for the lemma - declaration "eqvts" "bijs" and "freshs". + collection "eqvts". - By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored - in a data-slot in the context. Possible modifiers - are [attribute add] and [attribute del] for adding and deleting, - respectively the lemma from the data-slot. + By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets + 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 = @@ -17,9 +17,6 @@ val eqvt_force_del: attribute val setup: theory -> theory val get_eqvt_thms: Proof.context -> thm list - val get_fresh_thms: Proof.context -> thm list - val get_bij_thms: Proof.context -> thm list - val NOMINAL_EQVT_DEBUG : bool ref end; @@ -29,13 +26,11 @@ structure Data = GenericDataFun ( - type T = {eqvts:thm list, freshs:thm list, bijs:thm list}; - val empty = ({eqvts=[], freshs=[], bijs=[]}:T); - val extend = I; - fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2), - freshs = Thm.merge_thms (#freshs r1, #freshs r2), - bijs = Thm.merge_thms (#bijs r1, #bijs r2)} -); + type T = thm list + val empty = []:T + val extend = I + fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2) +) (* 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 *) @@ -46,45 +41,40 @@ (* 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 get_eqvt_thms = Context.Proof #> Data.get #> #eqvts; -val get_fresh_thms = Context.Proof #> Data.get #> #freshs; -val get_bij_thms = Context.Proof #> Data.get #> #bijs; +exception EQVT_FORM of string (* FIXME: should be a function in a library *) -fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)); +fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T)) -val NOMINAL_EQVT_DEBUG = ref false; +val NOMINAL_EQVT_DEBUG = ref false -fun tactic (msg,tac) = - if !NOMINAL_EQVT_DEBUG - then tac THEN print_tac ("after "^msg) - else tac +fun tactic (msg, tac) = + if !NOMINAL_EQVT_DEBUG + then tac THEN' (K (print_tac ("after " ^ msg))) + else tac fun tactic_eqvt ctx orig_thm pi pi' = - let - val mypi = Thm.cterm_of ctx pi - val T = fastype_of pi' - val mypifree = Thm.cterm_of ctx (Const ("List.rev", T --> T) $ pi') - val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp" - in - EVERY [tactic ("iffI applied",rtac iffI 1), - tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)), - tactic ("solve with orig_thm", (etac orig_thm 1)), - tactic ("applies orig_thm instantiated with rev pi", - dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1), - tactic ("getting rid of the pi on the right", - (rtac @{thm perm_boolI} 1)), - tactic ("getting rid of all remaining perms", - full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)] - end; +let + val mypi = Thm.cterm_of ctx pi + val T = fastype_of pi' + val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi') + val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp" +in + EVERY1 [tactic ("iffI applied",rtac @{thm iffI}), + tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}), + tactic ("solve with orig_thm", etac orig_thm), + tactic ("applies orig_thm instantiated with rev pi", + dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), + tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}), + tactic ("getting rid of all remaining perms", + full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))] +end; fun get_derived_thm ctxt hyp concl orig_thm pi typi = let val thy = ProofContext.theory_of ctxt; val pi' = Var (pi, typi); - val lhs = Const ("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp; + val lhs = Const (@{const_name "Nominal.perm"}, typi --> 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 val _ = Display.print_cterm (cterm_of thy goal_term) @@ -95,23 +85,25 @@ end (* replaces every variable x in t with pi o x *) -fun apply_pi trm (pi,typi) = - let - fun only_vars t = - (case t of - Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty))) - | _ => t) - in - map_aterms only_vars trm - end; +fun apply_pi trm (pi, typi) = +let + fun only_vars t = + (case t of + Var (n, ty) => + (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty) + $ (Var (pi, typi)) $ (Var (n, ty))) + | _ => t) +in + map_aterms only_vars 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 ("Nominal.perm",typrm) $ - (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $ + (Const (@{const_name "Nominal.perm"} ,typrm) $ + (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $ (Var (n,ty))) => let (* FIXME: this should be an operation the library *) @@ -130,7 +122,7 @@ (* 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,typi)] => (pi,typi) + [(pi,typi)] => (pi, typi) | _ => raise EQVT_FORM "All permutation should be the same") end; @@ -155,8 +147,8 @@ else raise EQVT_FORM "Type Implication" end (* case: eqvt-lemma is of the equational form *) - | (Const ("Trueprop", _) $ (Const ("op =", _) $ - (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) => + | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $ + (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) => (if (apply_pi lhs (pi,typi)) = rhs then [orig_thm] else raise EQVT_FORM "Type Equality") @@ -165,38 +157,26 @@ fold (fn thm => Data.map (flag thm)) thms_to_be_added context end handle EQVT_FORM s => - error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").") + error (Display.string_of_thm orig_thm ^ + " does not comply with the form of an equivariance lemma (" ^ s ^").") -(* in cases of bij- and freshness, we just add the lemmas to the *) -(* data-slot *) -fun eqvt_map f (r:Data.T) = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r}; -fun fresh_map f (r:Data.T) = {eqvts = #eqvts r, freshs = f (#freshs r), bijs = #bijs r}; -fun bij_map f (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = f (#bijs r)}; +fun eqvt_map f (r:Data.T) = f r; val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm)); val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm)); val eqvt_force_add = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm); val eqvt_force_del = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm); -val bij_add = Thm.declaration_attribute (Data.map o bij_map o Thm.add_thm); -val bij_del = Thm.declaration_attribute (Data.map o bij_map o Thm.del_thm); -val fresh_add = Thm.declaration_attribute (Data.map o fresh_map o Thm.add_thm); -val fresh_del = Thm.declaration_attribute (Data.map o fresh_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)" #> - Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del) - "freshness theorem declaration" #> - Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del) - "bijection theorem declaration" #> - PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #> - PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #> - PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get); + 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;