export has_internal;
authorwenzelm
Thu Jul 27 18:27:09 2000 +0200 (2000-07-27)
changeset 9455f23722b4fbe7
parent 9454 ea80449107cc
child 9456 880794f48ce6
export has_internal;
tag some rules as internal;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Thu Jul 27 18:25:55 2000 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Jul 27 18:27:09 2000 +0200
     1.3 @@ -86,6 +86,15 @@
     1.4  signature DRULE =
     1.5  sig
     1.6    include BASIC_DRULE
     1.7 +  val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
     1.8 +  val tag_rule          : tag -> thm -> thm
     1.9 +  val untag_rule        : string -> thm -> thm
    1.10 +  val tag               : tag -> 'a attribute
    1.11 +  val untag             : string -> 'a attribute
    1.12 +  val tag_lemma         : 'a attribute
    1.13 +  val tag_assumption    : 'a attribute
    1.14 +  val tag_internal      : 'a attribute
    1.15 +  val has_internal	: tag list -> bool
    1.16    val compose_single    : thm * int * thm -> thm
    1.17    val merge_rules	: thm list * thm list -> thm list
    1.18    val triv_goal         : thm
    1.19 @@ -101,14 +110,6 @@
    1.20    val unvarifyT         : thm -> thm
    1.21    val unvarify          : thm -> thm
    1.22    val tvars_intr_list	: string list -> thm -> thm
    1.23 -  val rule_attribute    : ('a -> thm -> thm) -> 'a attribute
    1.24 -  val tag_rule          : tag -> thm -> thm
    1.25 -  val untag_rule        : string -> thm -> thm
    1.26 -  val tag               : tag -> 'a attribute
    1.27 -  val untag             : string -> 'a attribute
    1.28 -  val tag_lemma         : 'a attribute
    1.29 -  val tag_assumption    : 'a attribute
    1.30 -  val tag_internal      : 'a attribute
    1.31  end;
    1.32  
    1.33  structure Drule: DRULE =
    1.34 @@ -208,6 +209,36 @@
    1.35      in (typ,sort) end;
    1.36  
    1.37  
    1.38 +
    1.39 +(** basic attributes **)
    1.40 +
    1.41 +(* dependent rules *)
    1.42 +
    1.43 +fun rule_attribute f (x, thm) = (x, (f x thm));
    1.44 +
    1.45 +
    1.46 +(* add / delete tags *)
    1.47 +
    1.48 +fun map_tags f thm =
    1.49 +  Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
    1.50 +
    1.51 +fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
    1.52 +fun untag_rule s = map_tags (filter_out (equal s o #1));
    1.53 +
    1.54 +fun tag tg x = rule_attribute (K (tag_rule tg)) x;
    1.55 +fun untag s x = rule_attribute (K (untag_rule s)) x;
    1.56 +
    1.57 +fun simple_tag name x = tag (name, []) x;
    1.58 +
    1.59 +fun tag_lemma x = simple_tag "lemma" x;
    1.60 +fun tag_assumption x = simple_tag "assumption" x;
    1.61 +
    1.62 +val internal_tag = ("internal", []);
    1.63 +fun tag_internal x = tag internal_tag x;
    1.64 +fun has_internal tags = exists (equal internal_tag) tags;
    1.65 +
    1.66 +
    1.67 +
    1.68  (** Standardization of rules **)
    1.69  
    1.70  (*Strip extraneous shyps as far as possible*)
    1.71 @@ -408,24 +439,22 @@
    1.72  
    1.73  fun read_prop s = read_cterm proto_sign (s, propT);
    1.74  
    1.75 -fun store_thm name thm = hd (PureThy.smart_store_thms (name, [standard thm]));
    1.76 +fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    1.77 +fun store_standard_thm name thm = store_thm name (standard thm);
    1.78  
    1.79  val reflexive_thm =
    1.80    let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
    1.81 -  in store_thm "reflexive" (Thm.reflexive cx) end;
    1.82 +  in store_standard_thm "reflexive" (Thm.reflexive cx) end;
    1.83  
    1.84  val symmetric_thm =
    1.85    let val xy = read_prop "x::'a::logic == y"
    1.86 -  in store_thm "symmetric"
    1.87 -      (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy)))
    1.88 -   end;
    1.89 +  in store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
    1.90  
    1.91  val transitive_thm =
    1.92    let val xy = read_prop "x::'a::logic == y"
    1.93        val yz = read_prop "y::'a::logic == z"
    1.94        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.95 -  in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm))
    1.96 -  end;
    1.97 +  in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.98  
    1.99  fun symmetric_fun thm = thm RS symmetric_thm;
   1.100  
   1.101 @@ -475,13 +504,13 @@
   1.102  (*** Some useful meta-theorems ***)
   1.103  
   1.104  (*The rule V/V, obtains assumption solving for eresolve_tac*)
   1.105 -val asm_rl = store_thm "asm_rl" (trivial(read_prop "PROP ?psi"));
   1.106 +val asm_rl = store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
   1.107  val _ = store_thm "_" asm_rl;
   1.108  
   1.109  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   1.110  val cut_rl =
   1.111 -  store_thm "cut_rl"
   1.112 -    (trivial(read_prop "PROP ?psi ==> PROP ?theta"));
   1.113 +  store_standard_thm "cut_rl"
   1.114 +    (Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta"));
   1.115  
   1.116  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   1.117       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
   1.118 @@ -489,7 +518,7 @@
   1.119    let val V = read_prop "PROP V"
   1.120        and VW = read_prop "PROP V ==> PROP W";
   1.121    in
   1.122 -    store_thm "revcut_rl"
   1.123 +    store_standard_thm "revcut_rl"
   1.124        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   1.125    end;
   1.126  
   1.127 @@ -497,7 +526,7 @@
   1.128  val thin_rl =
   1.129    let val V = read_prop "PROP V"
   1.130        and W = read_prop "PROP W";
   1.131 -  in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   1.132 +  in  store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   1.133    end;
   1.134  
   1.135  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   1.136 @@ -506,9 +535,9 @@
   1.137        and QV = read_prop "!!x::'a. PROP V"
   1.138        and x  = read_cterm proto_sign ("x", TypeInfer.logicT);
   1.139    in
   1.140 -    store_thm "triv_forall_equality"
   1.141 -      (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.142 -        (implies_intr V  (forall_intr x (assume V))))
   1.143 +    store_standard_thm "triv_forall_equality"
   1.144 +      (standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.145 +        (implies_intr V  (forall_intr x (assume V)))))
   1.146    end;
   1.147  
   1.148  (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   1.149 @@ -522,7 +551,7 @@
   1.150        val minor1 = assume cminor1;
   1.151        val cminor2 = read_prop "PROP PhiB";
   1.152        val minor2 = assume cminor2;
   1.153 -  in store_thm "swap_prems_rl"
   1.154 +  in store_standard_thm "swap_prems_rl"
   1.155         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.156           (implies_elim (implies_elim major minor1) minor2))))
   1.157    end;
   1.158 @@ -535,7 +564,7 @@
   1.159    let val PQ = read_prop "PROP phi ==> PROP psi"
   1.160        and QP = read_prop "PROP psi ==> PROP phi"
   1.161    in
   1.162 -    store_thm "equal_intr_rule"
   1.163 +    store_standard_thm "equal_intr_rule"
   1.164        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   1.165    end;
   1.166  
   1.167 @@ -626,8 +655,10 @@
   1.168    val G = read_prop "GOAL (PROP A)";
   1.169    val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
   1.170  in
   1.171 -  val triv_goal = store_thm "triv_goal" (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A));
   1.172 -  val rev_triv_goal = store_thm "rev_triv_goal" (Thm.equal_elim G_def (Thm.assume G));
   1.173 +  val triv_goal = store_thm "triv_goal"
   1.174 +    (tag_rule internal_tag (standard (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A))));
   1.175 +  val rev_triv_goal = store_thm "rev_triv_goal"
   1.176 +    (tag_rule internal_tag (standard (Thm.equal_elim G_def (Thm.assume G))));
   1.177  end;
   1.178  
   1.179  val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign (Const ("Goal", propT --> propT)));
   1.180 @@ -760,32 +791,6 @@
   1.181  fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
   1.182  
   1.183  
   1.184 -
   1.185 -(** basic attributes **)
   1.186 -
   1.187 -(* dependent rules *)
   1.188 -
   1.189 -fun rule_attribute f (x, thm) = (x, (f x thm));
   1.190 -
   1.191 -
   1.192 -(* add / delete tags *)
   1.193 -
   1.194 -fun map_tags f thm =
   1.195 -  Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
   1.196 -
   1.197 -fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
   1.198 -fun untag_rule s = map_tags (filter_out (equal s o #1));
   1.199 -
   1.200 -fun tag tg x = rule_attribute (K (tag_rule tg)) x;
   1.201 -fun untag s x = rule_attribute (K (untag_rule s)) x;
   1.202 -
   1.203 -fun simple_tag name x = tag (name, []) x;
   1.204 -
   1.205 -fun tag_lemma x = simple_tag "lemma" x;
   1.206 -fun tag_assumption x = simple_tag "assumption" x;
   1.207 -fun tag_internal x = simple_tag "internal" x;
   1.208 -
   1.209 -
   1.210  end;
   1.211  
   1.212