src/Pure/drule.ML
changeset 24241 424cb8b5e5b4
parent 24048 a12b4faff474
child 24426 d89e409cfe4e
     1.1 --- a/src/Pure/drule.ML	Mon Aug 13 12:56:03 2007 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Aug 13 18:10:18 2007 +0200
     1.3 @@ -518,7 +518,7 @@
     1.4  
     1.5  (*** Meta-Rewriting Rules ***)
     1.6  
     1.7 -fun read_prop s = Thm.read_cterm ProtoPure.thy (s, propT);
     1.8 +val read_prop = Thm.cterm_of ProtoPure.thy o SimpleSyntax.read_prop;
     1.9  
    1.10  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    1.11  fun store_standard_thm name thm = store_thm name (standard thm);
    1.12 @@ -530,12 +530,12 @@
    1.13    in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
    1.14  
    1.15  val symmetric_thm =
    1.16 -  let val xy = read_prop "x == y"
    1.17 +  let val xy = read_prop "x::'a == y::'a"
    1.18    in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end;
    1.19  
    1.20  val transitive_thm =
    1.21 -  let val xy = read_prop "x == y"
    1.22 -      val yz = read_prop "y == z"
    1.23 +  let val xy = read_prop "x::'a == y::'a"
    1.24 +      val yz = read_prop "y::'a == z::'a"
    1.25        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    1.26    in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    1.27  
    1.28 @@ -547,14 +547,14 @@
    1.29    in equal_elim (eta_conversion (cprop_of eq')) eq' end;
    1.30  
    1.31  val equals_cong =
    1.32 -  store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x == y"));
    1.33 +  store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a"));
    1.34  
    1.35  val imp_cong =
    1.36    let
    1.37 -    val ABC = read_prop "PROP A ==> PROP B == PROP C"
    1.38 -    val AB = read_prop "PROP A ==> PROP B"
    1.39 -    val AC = read_prop "PROP A ==> PROP C"
    1.40 -    val A = read_prop "PROP A"
    1.41 +    val ABC = read_prop "A ==> B::prop == C::prop"
    1.42 +    val AB = read_prop "A ==> B"
    1.43 +    val AC = read_prop "A ==> C"
    1.44 +    val A = read_prop "A"
    1.45    in
    1.46      store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr
    1.47        (implies_intr AB (implies_intr A
    1.48 @@ -567,10 +567,10 @@
    1.49  
    1.50  val swap_prems_eq =
    1.51    let
    1.52 -    val ABC = read_prop "PROP A ==> PROP B ==> PROP C"
    1.53 -    val BAC = read_prop "PROP B ==> PROP A ==> PROP C"
    1.54 -    val A = read_prop "PROP A"
    1.55 -    val B = read_prop "PROP B"
    1.56 +    val ABC = read_prop "A ==> B ==> C"
    1.57 +    val BAC = read_prop "B ==> A ==> C"
    1.58 +    val A = read_prop "A"
    1.59 +    val B = read_prop "B"
    1.60    in
    1.61      store_standard_thm_open "swap_prems_eq" (equal_intr
    1.62        (implies_intr ABC (implies_intr B (implies_intr A
    1.63 @@ -620,19 +620,19 @@
    1.64  (*** Some useful meta-theorems ***)
    1.65  
    1.66  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.67 -val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    1.68 +val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
    1.69  val _ = store_thm "_" asm_rl;
    1.70  
    1.71  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    1.72  val cut_rl =
    1.73    store_standard_thm_open "cut_rl"
    1.74 -    (Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta"));
    1.75 +    (Thm.trivial (read_prop "?psi ==> ?theta"));
    1.76  
    1.77  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
    1.78       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
    1.79  val revcut_rl =
    1.80 -  let val V = read_prop "PROP V"
    1.81 -      and VW = read_prop "PROP V ==> PROP W";
    1.82 +  let val V = read_prop "V"
    1.83 +      and VW = read_prop "V ==> W";
    1.84    in
    1.85      store_standard_thm_open "revcut_rl"
    1.86        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
    1.87 @@ -640,14 +640,14 @@
    1.88  
    1.89  (*for deleting an unwanted assumption*)
    1.90  val thin_rl =
    1.91 -  let val V = read_prop "PROP V"
    1.92 -      and W = read_prop "PROP W";
    1.93 +  let val V = read_prop "V"
    1.94 +      and W = read_prop "W";
    1.95    in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end;
    1.96  
    1.97  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
    1.98  val triv_forall_equality =
    1.99 -  let val V  = read_prop "PROP V"
   1.100 -      and QV = read_prop "!!x::'a. PROP V"
   1.101 +  let val V  = read_prop "V"
   1.102 +      and QV = read_prop "!!x::'a. V"
   1.103        and x  = cert (Free ("x", Term.aT []));
   1.104    in
   1.105      store_standard_thm_open "triv_forall_equality"
   1.106 @@ -660,8 +660,8 @@
   1.107  *)
   1.108  val distinct_prems_rl =
   1.109    let
   1.110 -    val AAB = read_prop "PROP Phi ==> PROP Phi ==> PROP Psi"
   1.111 -    val A = read_prop "PROP Phi";
   1.112 +    val AAB = read_prop "Phi ==> Phi ==> Psi"
   1.113 +    val A = read_prop "Phi";
   1.114    in
   1.115      store_standard_thm_open "distinct_prems_rl"
   1.116        (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
   1.117 @@ -672,11 +672,11 @@
   1.118     `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   1.119  *)
   1.120  val swap_prems_rl =
   1.121 -  let val cmajor = read_prop "PROP PhiA ==> PROP PhiB ==> PROP Psi";
   1.122 +  let val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
   1.123        val major = assume cmajor;
   1.124 -      val cminor1 = read_prop "PROP PhiA";
   1.125 +      val cminor1 = read_prop "PhiA";
   1.126        val minor1 = assume cminor1;
   1.127 -      val cminor2 = read_prop "PROP PhiB";
   1.128 +      val cminor2 = read_prop "PhiB";
   1.129        val minor2 = assume cminor2;
   1.130    in store_standard_thm_open "swap_prems_rl"
   1.131         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   1.132 @@ -688,8 +688,8 @@
   1.133     Introduction rule for == as a meta-theorem.
   1.134  *)
   1.135  val equal_intr_rule =
   1.136 -  let val PQ = read_prop "PROP phi ==> PROP psi"
   1.137 -      and QP = read_prop "PROP psi ==> PROP phi"
   1.138 +  let val PQ = read_prop "phi ==> psi"
   1.139 +      and QP = read_prop "psi ==> phi"
   1.140    in
   1.141      store_standard_thm_open "equal_intr_rule"
   1.142        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   1.143 @@ -697,8 +697,8 @@
   1.144  
   1.145  (* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
   1.146  val equal_elim_rule1 =
   1.147 -  let val eq = read_prop "PROP phi == PROP psi"
   1.148 -      and P = read_prop "PROP phi"
   1.149 +  let val eq = read_prop "phi::prop == psi::prop"
   1.150 +      and P = read_prop "phi"
   1.151    in store_standard_thm_open "equal_elim_rule1"
   1.152      (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
   1.153    end;
   1.154 @@ -709,7 +709,7 @@
   1.155  
   1.156  (* "[| PROP ?phi; PROP ?phi; PROP ?psi |] ==> PROP ?psi" *)
   1.157  val remdups_rl =
   1.158 -  let val P = read_prop "PROP phi" and Q = read_prop "PROP psi";
   1.159 +  let val P = read_prop "phi" and Q = read_prop "psi";
   1.160    in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
   1.161  
   1.162