SimpleSyntax.read_prop;
authorwenzelm
Mon Aug 13 18:10:18 2007 +0200 (2007-08-13)
changeset 24241424cb8b5e5b4
parent 24240 3831fc5598ab
child 24242 e52ef498c0ba
SimpleSyntax.read_prop;
src/Pure/conjunction.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/conjunction.ML	Mon Aug 13 12:56:03 2007 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Mon Aug 13 18:10:18 2007 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  
     1.5  (** abstract syntax **)
     1.6  
     1.7 -fun read s = Thm.read_cterm ProtoPure.thy (s, propT);
     1.8  val cert = Thm.cterm_of ProtoPure.thy;
     1.9 +val read_prop = cert o SimpleSyntax.read_prop;
    1.10  
    1.11  val true_prop = cert Logic.true_prop;
    1.12  val conjunction = cert Logic.conjunction;
    1.13 @@ -63,11 +63,11 @@
    1.14  
    1.15  local
    1.16  
    1.17 -val A = read "PROP A" and vA = read "PROP ?A";
    1.18 -val B = read "PROP B" and vB = read "PROP ?B";
    1.19 -val C = read "PROP C";
    1.20 -val ABC = read "PROP A ==> PROP B ==> PROP C";
    1.21 -val A_B = read "PROP ProtoPure.conjunction(A, B)"
    1.22 +val A = read_prop "A" and vA = read_prop "?A";
    1.23 +val B = read_prop "B" and vB = read_prop "?B";
    1.24 +val C = read_prop "C";
    1.25 +val ABC = read_prop "A ==> B ==> C";
    1.26 +val A_B = read_prop "A && B";
    1.27  
    1.28  val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
    1.29  
    1.30 @@ -125,7 +125,7 @@
    1.31    let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
    1.32    in (As, mk_conjunction_balanced As) end;
    1.33  
    1.34 -val B = cert (Free ("B", propT));
    1.35 +val B = read_prop "B";
    1.36  
    1.37  fun comp_rule th rule =
    1.38    Thm.adjust_maxidx_thm ~1 (th COMP
     2.1 --- a/src/Pure/drule.ML	Mon Aug 13 12:56:03 2007 +0200
     2.2 +++ b/src/Pure/drule.ML	Mon Aug 13 18:10:18 2007 +0200
     2.3 @@ -518,7 +518,7 @@
     2.4  
     2.5  (*** Meta-Rewriting Rules ***)
     2.6  
     2.7 -fun read_prop s = Thm.read_cterm ProtoPure.thy (s, propT);
     2.8 +val read_prop = Thm.cterm_of ProtoPure.thy o SimpleSyntax.read_prop;
     2.9  
    2.10  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    2.11  fun store_standard_thm name thm = store_thm name (standard thm);
    2.12 @@ -530,12 +530,12 @@
    2.13    in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
    2.14  
    2.15  val symmetric_thm =
    2.16 -  let val xy = read_prop "x == y"
    2.17 +  let val xy = read_prop "x::'a == y::'a"
    2.18    in store_standard_thm_open "symmetric" (Thm.implies_intr xy (Thm.symmetric (Thm.assume xy))) end;
    2.19  
    2.20  val transitive_thm =
    2.21 -  let val xy = read_prop "x == y"
    2.22 -      val yz = read_prop "y == z"
    2.23 +  let val xy = read_prop "x::'a == y::'a"
    2.24 +      val yz = read_prop "y::'a == z::'a"
    2.25        val xythm = Thm.assume xy and yzthm = Thm.assume yz
    2.26    in store_standard_thm_open "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
    2.27  
    2.28 @@ -547,14 +547,14 @@
    2.29    in equal_elim (eta_conversion (cprop_of eq')) eq' end;
    2.30  
    2.31  val equals_cong =
    2.32 -  store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x == y"));
    2.33 +  store_standard_thm_open "equals_cong" (Thm.reflexive (read_prop "x::'a == y::'a"));
    2.34  
    2.35  val imp_cong =
    2.36    let
    2.37 -    val ABC = read_prop "PROP A ==> PROP B == PROP C"
    2.38 -    val AB = read_prop "PROP A ==> PROP B"
    2.39 -    val AC = read_prop "PROP A ==> PROP C"
    2.40 -    val A = read_prop "PROP A"
    2.41 +    val ABC = read_prop "A ==> B::prop == C::prop"
    2.42 +    val AB = read_prop "A ==> B"
    2.43 +    val AC = read_prop "A ==> C"
    2.44 +    val A = read_prop "A"
    2.45    in
    2.46      store_standard_thm_open "imp_cong" (implies_intr ABC (equal_intr
    2.47        (implies_intr AB (implies_intr A
    2.48 @@ -567,10 +567,10 @@
    2.49  
    2.50  val swap_prems_eq =
    2.51    let
    2.52 -    val ABC = read_prop "PROP A ==> PROP B ==> PROP C"
    2.53 -    val BAC = read_prop "PROP B ==> PROP A ==> PROP C"
    2.54 -    val A = read_prop "PROP A"
    2.55 -    val B = read_prop "PROP B"
    2.56 +    val ABC = read_prop "A ==> B ==> C"
    2.57 +    val BAC = read_prop "B ==> A ==> C"
    2.58 +    val A = read_prop "A"
    2.59 +    val B = read_prop "B"
    2.60    in
    2.61      store_standard_thm_open "swap_prems_eq" (equal_intr
    2.62        (implies_intr ABC (implies_intr B (implies_intr A
    2.63 @@ -620,19 +620,19 @@
    2.64  (*** Some useful meta-theorems ***)
    2.65  
    2.66  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    2.67 -val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    2.68 +val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "?psi"));
    2.69  val _ = store_thm "_" asm_rl;
    2.70  
    2.71  (*Meta-level cut rule: [| V==>W; V |] ==> W *)
    2.72  val cut_rl =
    2.73    store_standard_thm_open "cut_rl"
    2.74 -    (Thm.trivial (read_prop "PROP ?psi ==> PROP ?theta"));
    2.75 +    (Thm.trivial (read_prop "?psi ==> ?theta"));
    2.76  
    2.77  (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
    2.78       [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
    2.79  val revcut_rl =
    2.80 -  let val V = read_prop "PROP V"
    2.81 -      and VW = read_prop "PROP V ==> PROP W";
    2.82 +  let val V = read_prop "V"
    2.83 +      and VW = read_prop "V ==> W";
    2.84    in
    2.85      store_standard_thm_open "revcut_rl"
    2.86        (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
    2.87 @@ -640,14 +640,14 @@
    2.88  
    2.89  (*for deleting an unwanted assumption*)
    2.90  val thin_rl =
    2.91 -  let val V = read_prop "PROP V"
    2.92 -      and W = read_prop "PROP W";
    2.93 +  let val V = read_prop "V"
    2.94 +      and W = read_prop "W";
    2.95    in store_standard_thm_open "thin_rl" (implies_intr V (implies_intr W (assume W))) end;
    2.96  
    2.97  (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
    2.98  val triv_forall_equality =
    2.99 -  let val V  = read_prop "PROP V"
   2.100 -      and QV = read_prop "!!x::'a. PROP V"
   2.101 +  let val V  = read_prop "V"
   2.102 +      and QV = read_prop "!!x::'a. V"
   2.103        and x  = cert (Free ("x", Term.aT []));
   2.104    in
   2.105      store_standard_thm_open "triv_forall_equality"
   2.106 @@ -660,8 +660,8 @@
   2.107  *)
   2.108  val distinct_prems_rl =
   2.109    let
   2.110 -    val AAB = read_prop "PROP Phi ==> PROP Phi ==> PROP Psi"
   2.111 -    val A = read_prop "PROP Phi";
   2.112 +    val AAB = read_prop "Phi ==> Phi ==> Psi"
   2.113 +    val A = read_prop "Phi";
   2.114    in
   2.115      store_standard_thm_open "distinct_prems_rl"
   2.116        (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
   2.117 @@ -672,11 +672,11 @@
   2.118     `thm COMP swap_prems_rl' swaps the first two premises of `thm'
   2.119  *)
   2.120  val swap_prems_rl =
   2.121 -  let val cmajor = read_prop "PROP PhiA ==> PROP PhiB ==> PROP Psi";
   2.122 +  let val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
   2.123        val major = assume cmajor;
   2.124 -      val cminor1 = read_prop "PROP PhiA";
   2.125 +      val cminor1 = read_prop "PhiA";
   2.126        val minor1 = assume cminor1;
   2.127 -      val cminor2 = read_prop "PROP PhiB";
   2.128 +      val cminor2 = read_prop "PhiB";
   2.129        val minor2 = assume cminor2;
   2.130    in store_standard_thm_open "swap_prems_rl"
   2.131         (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
   2.132 @@ -688,8 +688,8 @@
   2.133     Introduction rule for == as a meta-theorem.
   2.134  *)
   2.135  val equal_intr_rule =
   2.136 -  let val PQ = read_prop "PROP phi ==> PROP psi"
   2.137 -      and QP = read_prop "PROP psi ==> PROP phi"
   2.138 +  let val PQ = read_prop "phi ==> psi"
   2.139 +      and QP = read_prop "psi ==> phi"
   2.140    in
   2.141      store_standard_thm_open "equal_intr_rule"
   2.142        (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   2.143 @@ -697,8 +697,8 @@
   2.144  
   2.145  (* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
   2.146  val equal_elim_rule1 =
   2.147 -  let val eq = read_prop "PROP phi == PROP psi"
   2.148 -      and P = read_prop "PROP phi"
   2.149 +  let val eq = read_prop "phi::prop == psi::prop"
   2.150 +      and P = read_prop "phi"
   2.151    in store_standard_thm_open "equal_elim_rule1"
   2.152      (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
   2.153    end;
   2.154 @@ -709,7 +709,7 @@
   2.155  
   2.156  (* "[| PROP ?phi; PROP ?phi; PROP ?psi |] ==> PROP ?psi" *)
   2.157  val remdups_rl =
   2.158 -  let val P = read_prop "PROP phi" and Q = read_prop "PROP psi";
   2.159 +  let val P = read_prop "phi" and Q = read_prop "psi";
   2.160    in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
   2.161  
   2.162