Some basic rules are now stored with "open" derivations, to facilitate
authorberghofe
Fri Aug 31 16:07:56 2001 +0200 (2001-08-31)
changeset 11512da3a96ab5630
parent 11511 ec89f5cff390
child 11513 2f6fe5b01521
Some basic rules are now stored with "open" derivations, to facilitate
simplification of proof terms.
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Aug 31 16:06:21 2001 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri Aug 31 16:07:56 2001 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4      (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
     1.5    val zero_var_indexes  : thm -> thm
     1.6    val standard          : thm -> thm
     1.7 +  val standard'         : thm -> thm
     1.8    val rotate_prems      : int -> thm -> thm
     1.9    val rearrange_prems   : int list -> thm -> thm
    1.10    val assume_ax         : theory -> string -> thm
    1.11 @@ -62,6 +63,7 @@
    1.12    val transitive_thm    : thm
    1.13    val refl_implies      : thm
    1.14    val symmetric_fun     : thm -> thm
    1.15 +  val extensional       : thm -> thm
    1.16    val imp_cong          : thm
    1.17    val swap_prems_eq     : thm
    1.18    val equal_abs_elim    : cterm  -> thm -> thm
    1.19 @@ -88,7 +90,6 @@
    1.20    val tag               : tag -> 'a attribute
    1.21    val untag             : string -> 'a attribute
    1.22    val tag_lemma         : 'a attribute
    1.23 -  val tag_assumption    : 'a attribute
    1.24    val tag_internal      : 'a attribute
    1.25    val has_internal	: tag list -> bool
    1.26    val close_derivation  : thm -> thm
    1.27 @@ -249,7 +250,6 @@
    1.28  fun simple_tag name x = tag (name, []) x;
    1.29  
    1.30  fun tag_lemma x = simple_tag "lemma" x;
    1.31 -fun tag_assumption x = simple_tag "assumption" x;
    1.32  
    1.33  val internal_tag = ("internal", []);
    1.34  fun tag_internal x = tag internal_tag x;
    1.35 @@ -329,15 +329,17 @@
    1.36    if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm)
    1.37    else thm;
    1.38  
    1.39 -fun standard th =
    1.40 +fun standard' th =
    1.41    let val {maxidx,...} = rep_thm th in
    1.42      th
    1.43      |> implies_intr_hyps
    1.44      |> forall_intr_frees |> forall_elim_vars (maxidx + 1)
    1.45      |> strip_shyps_warning
    1.46 -    |> zero_var_indexes |> Thm.varifyT |> Thm.compress |> close_derivation
    1.47 +    |> zero_var_indexes |> Thm.varifyT |> Thm.compress
    1.48    end;
    1.49  
    1.50 +val standard = close_derivation o standard';
    1.51 +
    1.52  
    1.53  (*Convert all Vars in a theorem to Frees.  Also return a function for
    1.54    reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
    1.55 @@ -480,6 +482,8 @@
    1.56  
    1.57  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    1.58  fun store_standard_thm name thm = store_thm name (standard thm);
    1.59 +fun open_store_thm name thm = hd (PureThy.open_smart_store_thms (name, [thm]));
    1.60 +fun open_store_standard_thm name thm = open_store_thm name (standard' thm);
    1.61  
    1.62  val reflexive_thm =
    1.63    let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
    1.64 @@ -497,6 +501,11 @@
    1.65  
    1.66  fun symmetric_fun thm = thm RS symmetric_thm;
    1.67  
    1.68 +fun extensional eq =
    1.69 +  let val eq' =
    1.70 +    abstract_rule "x" (snd (Thm.dest_comb (fst (dest_equals (cprop_of eq))))) eq
    1.71 +  in equal_elim (eta_conversion (cprop_of eq')) eq' end;
    1.72 +
    1.73  val imp_cong =
    1.74    let
    1.75      val ABC = read_prop "PROP A ==> PROP B == PROP C"
    1.76 @@ -504,7 +513,7 @@
    1.77      val AC = read_prop "PROP A ==> PROP C"
    1.78      val A = read_prop "PROP A"
    1.79    in
    1.80 -    store_standard_thm "imp_cong" (implies_intr ABC (equal_intr
    1.81 +    open_store_standard_thm "imp_cong" (implies_intr ABC (equal_intr
    1.82        (implies_intr AB (implies_intr A
    1.83          (equal_elim (implies_elim (assume ABC) (assume A))
    1.84            (implies_elim (assume AB) (assume A)))))
    1.85 @@ -520,7 +529,7 @@
    1.86      val A = read_prop "PROP A"
    1.87      val B = read_prop "PROP B"
    1.88    in
    1.89 -    store_standard_thm "swap_prems_eq" (equal_intr
    1.90 +    open_store_standard_thm "swap_prems_eq" (equal_intr
    1.91        (implies_intr ABC (implies_intr B (implies_intr A
    1.92          (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
    1.93        (implies_intr BAC (implies_intr A (implies_intr B
    1.94 @@ -533,12 +542,12 @@
    1.95  (*** Some useful meta-theorems ***)
    1.96  
    1.97  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.98 -val asm_rl = store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    1.99 +val asm_rl = open_store_standard_thm "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
   1.100  val _ = store_thm "_" asm_rl;
   1.101  
   1.102  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
   1.103  val cut_rl =
   1.104 -  store_standard_thm "cut_rl"
   1.105 +  open_store_standard_thm "cut_rl"
   1.106      (Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta"));
   1.107  
   1.108  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
   1.109 @@ -547,7 +556,7 @@
   1.110    let val V = read_prop "PROP V"
   1.111        and VW = read_prop "PROP V ==> PROP W";
   1.112    in
   1.113 -    store_standard_thm "revcut_rl"
   1.114 +    open_store_standard_thm "revcut_rl"
   1.115        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   1.116    end;
   1.117  
   1.118 @@ -555,7 +564,7 @@
   1.119  val thin_rl =
   1.120    let val V = read_prop "PROP V"
   1.121        and W = read_prop "PROP W";
   1.122 -  in  store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   1.123 +  in  open_store_standard_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   1.124    end;
   1.125  
   1.126  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
   1.127 @@ -564,9 +573,9 @@
   1.128        and QV = read_prop "!!x::'a. PROP V"
   1.129        and x  = read_cterm proto_sign ("x", TypeInfer.logicT);
   1.130    in
   1.131 -    store_standard_thm "triv_forall_equality"
   1.132 -      (standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.133 -        (implies_intr V  (forall_intr x (assume V)))))
   1.134 +    open_store_standard_thm "triv_forall_equality"
   1.135 +      (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   1.136 +        (implies_intr V  (forall_intr x (assume V))))
   1.137    end;
   1.138  
   1.139  (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
   1.140 @@ -580,7 +589,7 @@
   1.141        val minor1 = assume cminor1;
   1.142        val cminor2 = read_prop "PROP PhiB";
   1.143        val minor2 = assume cminor2;
   1.144 -  in store_standard_thm "swap_prems_rl"
   1.145 +  in open_store_standard_thm "swap_prems_rl"
   1.146         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.147           (implies_elim (implies_elim major minor1) minor2))))
   1.148    end;
   1.149 @@ -593,7 +602,7 @@
   1.150    let val PQ = read_prop "PROP phi ==> PROP psi"
   1.151        and QP = read_prop "PROP psi ==> PROP phi"
   1.152    in
   1.153 -    store_standard_thm "equal_intr_rule"
   1.154 +    open_store_standard_thm "equal_intr_rule"
   1.155        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   1.156    end;
   1.157