1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy Sat Apr 25 23:42:30 2009 +0200
1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy Sun Apr 26 00:42:59 2009 +0200
1.3 @@ -245,7 +245,7 @@
1.4 apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs])
1.5 done
1.6
1.7 -lemma ty_vrs_fresh[fresh]:
1.8 +lemma ty_vrs_fresh:
1.9 fixes x::"vrs"
1.10 and T::"ty"
1.11 shows "x \<sharp> T"
1.12 @@ -422,7 +422,7 @@
1.13 by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
1.14 (perm_simp add: fresh_left)+
1.15
1.16 -lemma type_subst_fresh[fresh]:
1.17 +lemma type_subst_fresh:
1.18 fixes X::"tyvrs"
1.19 assumes "X \<sharp> T" and "X \<sharp> P"
1.20 shows "X \<sharp> T[Y \<mapsto> P]\<^sub>\<tau>"
1.21 @@ -430,7 +430,7 @@
1.22 by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
1.23 (auto simp add: abs_fresh)
1.24
1.25 -lemma fresh_type_subst_fresh[fresh]:
1.26 +lemma fresh_type_subst_fresh:
1.27 assumes "X\<sharp>T'"
1.28 shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
1.29 using assms
1.30 @@ -458,18 +458,19 @@
1.31 | "(VarB X U)[Y \<mapsto> T]\<^sub>b = VarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
1.32 by auto
1.33
1.34 -lemma binding_subst_fresh[fresh]:
1.35 +lemma binding_subst_fresh:
1.36 fixes X::"tyvrs"
1.37 assumes "X \<sharp> a"
1.38 and "X \<sharp> P"
1.39 shows "X \<sharp> a[Y \<mapsto> P]\<^sub>b"
1.40 using assms
1.41 -by (nominal_induct a rule:binding.strong_induct)
1.42 - (auto simp add: freshs)
1.43 +by (nominal_induct a rule: binding.strong_induct)
1.44 + (auto simp add: type_subst_fresh)
1.45
1.46 -lemma binding_subst_identity: "X \<sharp> B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
1.47 - by (induct B rule: binding.induct)
1.48 - (simp_all add: fresh_atm type_subst_identity)
1.49 +lemma binding_subst_identity:
1.50 + shows "X \<sharp> B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
1.51 +by (induct B rule: binding.induct)
1.52 + (simp_all add: fresh_atm type_subst_identity)
1.53
1.54 consts
1.55 subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100)
1.56 @@ -478,14 +479,14 @@
1.57 "([])[Y \<mapsto> T]\<^sub>e= []"
1.58 "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
1.59
1.60 -lemma ctxt_subst_fresh'[fresh]:
1.61 +lemma ctxt_subst_fresh':
1.62 fixes X::"tyvrs"
1.63 assumes "X \<sharp> \<Gamma>"
1.64 and "X \<sharp> P"
1.65 shows "X \<sharp> \<Gamma>[Y \<mapsto> P]\<^sub>e"
1.66 using assms
1.67 by (induct \<Gamma>)
1.68 - (auto simp add: fresh_list_cons freshs)
1.69 + (auto simp add: fresh_list_cons binding_subst_fresh)
1.70
1.71 lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
1.72 by (induct \<Gamma>) auto
1.73 @@ -1188,8 +1189,8 @@
1.74 using assms by (induct, auto)
1.75
1.76 nominal_inductive typing
1.77 - by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain
1.78 - simp: abs_fresh fresh_prod fresh_atm freshs valid_ty_domain_fresh fresh_trm_domain)
1.79 +by (auto dest!: typing_ok intro: closed_in_fresh fresh_domain type_subst_fresh
1.80 + simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_domain_fresh fresh_trm_domain)
1.81
1.82 lemma ok_imp_VarB_closed_in:
1.83 assumes ok: "\<turnstile> \<Gamma> ok"
2.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Apr 25 23:42:30 2009 +0200
2.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Apr 26 00:42:59 2009 +0200
2.3 @@ -1,12 +1,12 @@
2.4 (* Authors: Julien Narboux and Christian Urban
2.5
2.6 This file introduces the infrastructure for the lemma
2.7 - declaration "eqvts" "bijs" and "freshs".
2.8 + collection "eqvts".
2.9
2.10 - By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored
2.11 - in a data-slot in the context. Possible modifiers
2.12 - are [attribute add] and [attribute del] for adding and deleting,
2.13 - respectively the lemma from the data-slot.
2.14 + By attaching [eqvt], [eqvt_force] to a lemma, the lemma gets
2.15 + stored in a data-slot in the context. Possible modifiers
2.16 + are [... add] and [... del] for adding and deleting, respectively
2.17 + the lemma from the data-slot.
2.18 *)
2.19
2.20 signature NOMINAL_THMDECLS =
2.21 @@ -17,9 +17,6 @@
2.22 val eqvt_force_del: attribute
2.23 val setup: theory -> theory
2.24 val get_eqvt_thms: Proof.context -> thm list
2.25 - val get_fresh_thms: Proof.context -> thm list
2.26 - val get_bij_thms: Proof.context -> thm list
2.27 -
2.28
2.29 val NOMINAL_EQVT_DEBUG : bool ref
2.30 end;
2.31 @@ -29,13 +26,11 @@
2.32
2.33 structure Data = GenericDataFun
2.34 (
2.35 - type T = {eqvts:thm list, freshs:thm list, bijs:thm list};
2.36 - val empty = ({eqvts=[], freshs=[], bijs=[]}:T);
2.37 - val extend = I;
2.38 - fun merge _ (r1:T,r2:T) = {eqvts = Thm.merge_thms (#eqvts r1, #eqvts r2),
2.39 - freshs = Thm.merge_thms (#freshs r1, #freshs r2),
2.40 - bijs = Thm.merge_thms (#bijs r1, #bijs r2)}
2.41 -);
2.42 + type T = thm list
2.43 + val empty = []:T
2.44 + val extend = I
2.45 + fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
2.46 +)
2.47
2.48 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
2.49 (* There are two forms: one is an implication (for relations) and the other is an *)
2.50 @@ -46,45 +41,40 @@
2.51 (* the implicational case it is also checked that the variables and permutation fit *)
2.52 (* together, i.e. are of the right "pt_class", so that a stronger version of the *)
2.53 (* equality-lemma can be derived. *)
2.54 -exception EQVT_FORM of string;
2.55 -
2.56 -val get_eqvt_thms = Context.Proof #> Data.get #> #eqvts;
2.57 -val get_fresh_thms = Context.Proof #> Data.get #> #freshs;
2.58 -val get_bij_thms = Context.Proof #> Data.get #> #bijs;
2.59 +exception EQVT_FORM of string
2.60
2.61 (* FIXME: should be a function in a library *)
2.62 -fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T));
2.63 +fun mk_permT T = HOLogic.listT (HOLogic.mk_prodT (T, T))
2.64
2.65 -val NOMINAL_EQVT_DEBUG = ref false;
2.66 +val NOMINAL_EQVT_DEBUG = ref false
2.67
2.68 -fun tactic (msg,tac) =
2.69 - if !NOMINAL_EQVT_DEBUG
2.70 - then tac THEN print_tac ("after "^msg)
2.71 - else tac
2.72 +fun tactic (msg, tac) =
2.73 + if !NOMINAL_EQVT_DEBUG
2.74 + then tac THEN' (K (print_tac ("after " ^ msg)))
2.75 + else tac
2.76
2.77 fun tactic_eqvt ctx orig_thm pi pi' =
2.78 - let
2.79 - val mypi = Thm.cterm_of ctx pi
2.80 - val T = fastype_of pi'
2.81 - val mypifree = Thm.cterm_of ctx (Const ("List.rev", T --> T) $ pi')
2.82 - val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
2.83 - in
2.84 - EVERY [tactic ("iffI applied",rtac iffI 1),
2.85 - tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)),
2.86 - tactic ("solve with orig_thm", (etac orig_thm 1)),
2.87 - tactic ("applies orig_thm instantiated with rev pi",
2.88 - dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm) 1),
2.89 - tactic ("getting rid of the pi on the right",
2.90 - (rtac @{thm perm_boolI} 1)),
2.91 - tactic ("getting rid of all remaining perms",
2.92 - full_simp_tac (HOL_basic_ss addsimps perm_pi_simp) 1)]
2.93 - end;
2.94 +let
2.95 + val mypi = Thm.cterm_of ctx pi
2.96 + val T = fastype_of pi'
2.97 + val mypifree = Thm.cterm_of ctx (Const (@{const_name "List.rev"}, T --> T) $ pi')
2.98 + val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp"
2.99 +in
2.100 + EVERY1 [tactic ("iffI applied",rtac @{thm iffI}),
2.101 + tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
2.102 + tactic ("solve with orig_thm", etac orig_thm),
2.103 + tactic ("applies orig_thm instantiated with rev pi",
2.104 + dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
2.105 + tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
2.106 + tactic ("getting rid of all remaining perms",
2.107 + full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
2.108 +end;
2.109
2.110 fun get_derived_thm ctxt hyp concl orig_thm pi typi =
2.111 let
2.112 val thy = ProofContext.theory_of ctxt;
2.113 val pi' = Var (pi, typi);
2.114 - val lhs = Const ("Nominal.perm", typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
2.115 + val lhs = Const (@{const_name "Nominal.perm"}, typi --> HOLogic.boolT --> HOLogic.boolT) $ pi' $ hyp;
2.116 val ([goal_term, pi''], ctxt') = Variable.import_terms false
2.117 [HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, concl)), pi'] ctxt
2.118 val _ = Display.print_cterm (cterm_of thy goal_term)
2.119 @@ -95,23 +85,25 @@
2.120 end
2.121
2.122 (* replaces every variable x in t with pi o x *)
2.123 -fun apply_pi trm (pi,typi) =
2.124 - let
2.125 - fun only_vars t =
2.126 - (case t of
2.127 - Var (n,ty) => (Const ("Nominal.perm",typi --> ty --> ty) $ (Var (pi,typi)) $ (Var (n,ty)))
2.128 - | _ => t)
2.129 - in
2.130 - map_aterms only_vars trm
2.131 - end;
2.132 +fun apply_pi trm (pi, typi) =
2.133 +let
2.134 + fun only_vars t =
2.135 + (case t of
2.136 + Var (n, ty) =>
2.137 + (Const (@{const_name "Nominal.perm"}, typi --> ty --> ty)
2.138 + $ (Var (pi, typi)) $ (Var (n, ty)))
2.139 + | _ => t)
2.140 +in
2.141 + map_aterms only_vars trm
2.142 +end;
2.143
2.144 (* returns *the* pi which is in front of all variables, provided there *)
2.145 (* exists such a pi; otherwise raises EQVT_FORM *)
2.146 fun get_pi t thy =
2.147 let fun get_pi_aux s =
2.148 (case s of
2.149 - (Const ("Nominal.perm",typrm) $
2.150 - (Var (pi,typi as Type("List.list",[Type ("*",[Type (tyatm,[]),_])]))) $
2.151 + (Const (@{const_name "Nominal.perm"} ,typrm) $
2.152 + (Var (pi,typi as Type("List.list", [Type ("*", [Type (tyatm,[]),_])]))) $
2.153 (Var (n,ty))) =>
2.154 let
2.155 (* FIXME: this should be an operation the library *)
2.156 @@ -130,7 +122,7 @@
2.157 (* to ensure that all pi's must have been the same, i.e. distinct returns *)
2.158 (* a singleton-list *)
2.159 (case (distinct (op =) (get_pi_aux t)) of
2.160 - [(pi,typi)] => (pi,typi)
2.161 + [(pi,typi)] => (pi, typi)
2.162 | _ => raise EQVT_FORM "All permutation should be the same")
2.163 end;
2.164
2.165 @@ -155,8 +147,8 @@
2.166 else raise EQVT_FORM "Type Implication"
2.167 end
2.168 (* case: eqvt-lemma is of the equational form *)
2.169 - | (Const ("Trueprop", _) $ (Const ("op =", _) $
2.170 - (Const ("Nominal.perm",typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
2.171 + | (Const (@{const_name "Trueprop"}, _) $ (Const (@{const_name "op ="}, _) $
2.172 + (Const (@{const_name "Nominal.perm"},typrm) $ Var (pi,typi) $ lhs) $ rhs)) =>
2.173 (if (apply_pi lhs (pi,typi)) = rhs
2.174 then [orig_thm]
2.175 else raise EQVT_FORM "Type Equality")
2.176 @@ -165,38 +157,26 @@
2.177 fold (fn thm => Data.map (flag thm)) thms_to_be_added context
2.178 end
2.179 handle EQVT_FORM s =>
2.180 - error (Display.string_of_thm orig_thm ^ " does not comply with the form of an equivariance lemma ("^s^").")
2.181 + error (Display.string_of_thm orig_thm ^
2.182 + " does not comply with the form of an equivariance lemma (" ^ s ^").")
2.183
2.184 -(* in cases of bij- and freshness, we just add the lemmas to the *)
2.185 -(* data-slot *)
2.186
2.187 -fun eqvt_map f (r:Data.T) = {eqvts = f (#eqvts r), freshs = #freshs r, bijs = #bijs r};
2.188 -fun fresh_map f (r:Data.T) = {eqvts = #eqvts r, freshs = f (#freshs r), bijs = #bijs r};
2.189 -fun bij_map f (r:Data.T) = {eqvts = #eqvts r, freshs = #freshs r, bijs = f (#bijs r)};
2.190 +fun eqvt_map f (r:Data.T) = f r;
2.191
2.192 val eqvt_add = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.add_thm));
2.193 val eqvt_del = Thm.declaration_attribute (eqvt_add_del_aux (eqvt_map o Thm.del_thm));
2.194
2.195 val eqvt_force_add = Thm.declaration_attribute (Data.map o eqvt_map o Thm.add_thm);
2.196 val eqvt_force_del = Thm.declaration_attribute (Data.map o eqvt_map o Thm.del_thm);
2.197 -val bij_add = Thm.declaration_attribute (Data.map o bij_map o Thm.add_thm);
2.198 -val bij_del = Thm.declaration_attribute (Data.map o bij_map o Thm.del_thm);
2.199 -val fresh_add = Thm.declaration_attribute (Data.map o fresh_map o Thm.add_thm);
2.200 -val fresh_del = Thm.declaration_attribute (Data.map o fresh_map o Thm.del_thm);
2.201
2.202 -
2.203 +val get_eqvt_thms = Context.Proof #> Data.get;
2.204
2.205 val setup =
2.206 - Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
2.207 - "equivariance theorem declaration" #>
2.208 - Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
2.209 - "equivariance theorem declaration (without checking the form of the lemma)" #>
2.210 - Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
2.211 - "freshness theorem declaration" #>
2.212 - Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
2.213 - "bijection theorem declaration" #>
2.214 - PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
2.215 - PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
2.216 - PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
2.217 + Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
2.218 + "equivariance theorem declaration"
2.219 + #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
2.220 + "equivariance theorem declaration (without checking the form of the lemma)"
2.221 + #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get)
2.222 +
2.223
2.224 end;