deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
authorChristian Urban <urbanc@in.tum.de>
Sun Apr 26 00:42:49 2009 +0200 (2009-04-26)
changeset 30986047fa04a9fe8
parent 30983 e54777ab68bd
child 30987 2bbc22bd6a95
deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
src/HOL/Nominal/Examples/Fsub.thy
src/HOL/Nominal/nominal_thmdecls.ML
     1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Sat Apr 25 21:42:05 2009 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Sun Apr 26 00:42:49 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 21:42:05 2009 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Apr 26 00:42:49 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;