tuned;
authorwenzelm
Fri Jul 27 16:21:09 2018 +0200 (11 months ago)
changeset 68691206966cbc2fc
parent 68690 354c04092cd0
child 68692 0c568ec56f37
tuned;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Jul 26 15:19:56 2018 +0200
     1.2 +++ b/src/Pure/thm.ML	Fri Jul 27 16:21:09 2018 +0200
     1.3 @@ -772,15 +772,15 @@
     1.4    A \<Longrightarrow> B
     1.5  *)
     1.6  fun implies_intr
     1.7 -    (ct as Cterm {t = A, T, maxidx = maxidxA, sorts, ...})
     1.8 -    (th as Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...})) =
     1.9 +    (ct as Cterm {t = A, T, maxidx = maxidx1, sorts, ...})
    1.10 +    (th as Thm (der, {maxidx = maxidx2, hyps, shyps, tpairs, prop, ...})) =
    1.11    if T <> propT then
    1.12      raise THM ("implies_intr: assumptions must have type prop", 0, [th])
    1.13    else
    1.14      Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
    1.15       {cert = join_certificate1 (ct, th),
    1.16        tags = [],
    1.17 -      maxidx = Int.max (maxidxA, maxidx),
    1.18 +      maxidx = Int.max (maxidx1, maxidx2),
    1.19        shyps = Sorts.union sorts shyps,
    1.20        hyps = remove_hyps A hyps,
    1.21        tpairs = tpairs,
    1.22 @@ -794,9 +794,9 @@
    1.23  *)
    1.24  fun implies_elim thAB thA =
    1.25    let
    1.26 -    val Thm (derA, {maxidx = maxA, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,
    1.27 +    val Thm (derA, {maxidx = maxidx1, hyps = hypsA, shyps = shypsA, tpairs = tpairsA,
    1.28        prop = propA, ...}) = thA
    1.29 -    and Thm (der, {maxidx, hyps, shyps, tpairs, prop, ...}) = thAB;
    1.30 +    and Thm (der, {maxidx = maxidx2, hyps, shyps, tpairs, prop, ...}) = thAB;
    1.31      fun err () = raise THM ("implies_elim: major premise", 0, [thAB, thA]);
    1.32    in
    1.33      case prop of
    1.34 @@ -805,7 +805,7 @@
    1.35            Thm (deriv_rule2 (curry Proofterm.%%) der derA,
    1.36             {cert = join_certificate2 (thAB, thA),
    1.37              tags = [],
    1.38 -            maxidx = Int.max (maxA, maxidx),
    1.39 +            maxidx = Int.max (maxidx1, maxidx2),
    1.40              shyps = Sorts.union shypsA shyps,
    1.41              hyps = union_hyps hypsA hyps,
    1.42              tpairs = union_tpairs tpairsA tpairs,
    1.43 @@ -851,8 +851,8 @@
    1.44    A[t/x]
    1.45  *)
    1.46  fun forall_elim
    1.47 -    (ct as Cterm {t, T, maxidx = maxt, sorts, ...})
    1.48 -    (th as Thm (der, {maxidx, shyps, hyps, tpairs, prop, ...})) =
    1.49 +    (ct as Cterm {t, T, maxidx = maxidx1, sorts, ...})
    1.50 +    (th as Thm (der, {maxidx = maxidx2, shyps, hyps, tpairs, prop, ...})) =
    1.51    (case prop of
    1.52      Const ("Pure.all", Type ("fun", [Type ("fun", [qary, _]), _])) $ A =>
    1.53        if T <> qary then
    1.54 @@ -861,7 +861,7 @@
    1.55          Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
    1.56           {cert = join_certificate1 (ct, th),
    1.57            tags = [],
    1.58 -          maxidx = Int.max (maxidx, maxt),
    1.59 +          maxidx = Int.max (maxidx1, maxidx2),
    1.60            shyps = Sorts.union sorts shyps,
    1.61            hyps = hyps,
    1.62            tpairs = tpairs,
    1.63 @@ -909,9 +909,9 @@
    1.64  *)
    1.65  fun transitive th1 th2 =
    1.66    let
    1.67 -    val Thm (der1, {maxidx = max1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,
    1.68 +    val Thm (der1, {maxidx = maxidx1, hyps = hyps1, shyps = shyps1, tpairs = tpairs1,
    1.69        prop = prop1, ...}) = th1
    1.70 -    and Thm (der2, {maxidx = max2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
    1.71 +    and Thm (der2, {maxidx = maxidx2, hyps = hyps2, shyps = shyps2, tpairs = tpairs2,
    1.72        prop = prop2, ...}) = th2;
    1.73      fun err msg = raise THM ("transitive: " ^ msg, 0, [th1, th2]);
    1.74    in
    1.75 @@ -922,7 +922,7 @@
    1.76            Thm (deriv_rule2 (Proofterm.transitive u T) der1 der2,
    1.77             {cert = join_certificate2 (th1, th2),
    1.78              tags = [],
    1.79 -            maxidx = Int.max (max1, max2),
    1.80 +            maxidx = Int.max (maxidx1, maxidx2),
    1.81              shyps = Sorts.union shyps1 shyps2,
    1.82              hyps = union_hyps hyps1 hyps2,
    1.83              tpairs = union_tpairs tpairs1 tpairs2,
    1.84 @@ -1011,9 +1011,9 @@
    1.85  *)
    1.86  fun combination th1 th2 =
    1.87    let
    1.88 -    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
    1.89 +    val Thm (der1, {maxidx = maxidx1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
    1.90        prop = prop1, ...}) = th1
    1.91 -    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
    1.92 +    and Thm (der2, {maxidx = maxidx2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
    1.93        prop = prop2, ...}) = th2;
    1.94      fun chktypes fT tT =
    1.95        (case fT of
    1.96 @@ -1030,7 +1030,7 @@
    1.97            Thm (deriv_rule2 (Proofterm.combination f g t u fT) der1 der2,
    1.98             {cert = join_certificate2 (th1, th2),
    1.99              tags = [],
   1.100 -            maxidx = Int.max (max1, max2),
   1.101 +            maxidx = Int.max (maxidx1, maxidx2),
   1.102              shyps = Sorts.union shyps1 shyps2,
   1.103              hyps = union_hyps hyps1 hyps2,
   1.104              tpairs = union_tpairs tpairs1 tpairs2,
   1.105 @@ -1045,9 +1045,9 @@
   1.106  *)
   1.107  fun equal_intr th1 th2 =
   1.108    let
   1.109 -    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
   1.110 +    val Thm (der1, {maxidx = maxidx1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1,
   1.111        prop = prop1, ...}) = th1
   1.112 -    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
   1.113 +    and Thm (der2, {maxidx = maxidx2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2,
   1.114        prop = prop2, ...}) = th2;
   1.115      fun err msg = raise THM ("equal_intr: " ^ msg, 0, [th1, th2]);
   1.116    in
   1.117 @@ -1057,7 +1057,7 @@
   1.118            Thm (deriv_rule2 (Proofterm.equal_intr A B) der1 der2,
   1.119             {cert = join_certificate2 (th1, th2),
   1.120              tags = [],
   1.121 -            maxidx = Int.max (max1, max2),
   1.122 +            maxidx = Int.max (maxidx1, maxidx2),
   1.123              shyps = Sorts.union shyps1 shyps2,
   1.124              hyps = union_hyps hyps1 hyps2,
   1.125              tpairs = union_tpairs tpairs1 tpairs2,
   1.126 @@ -1073,9 +1073,9 @@
   1.127  *)
   1.128  fun equal_elim th1 th2 =
   1.129    let
   1.130 -    val Thm (der1, {maxidx = max1, shyps = shyps1, hyps = hyps1,
   1.131 +    val Thm (der1, {maxidx = maxidx1, shyps = shyps1, hyps = hyps1,
   1.132        tpairs = tpairs1, prop = prop1, ...}) = th1
   1.133 -    and Thm (der2, {maxidx = max2, shyps = shyps2, hyps = hyps2,
   1.134 +    and Thm (der2, {maxidx = maxidx2, shyps = shyps2, hyps = hyps2,
   1.135        tpairs = tpairs2, prop = prop2, ...}) = th2;
   1.136      fun err msg = raise THM ("equal_elim: " ^ msg, 0, [th1, th2]);
   1.137    in
   1.138 @@ -1085,7 +1085,7 @@
   1.139            Thm (deriv_rule2 (Proofterm.equal_elim A B) der1 der2,
   1.140             {cert = join_certificate2 (th1, th2),
   1.141              tags = [],
   1.142 -            maxidx = Int.max (max1, max2),
   1.143 +            maxidx = Int.max (maxidx1, maxidx2),
   1.144              shyps = Sorts.union shyps1 shyps2,
   1.145              hyps = union_hyps hyps1 hyps2,
   1.146              tpairs = union_tpairs tpairs1 tpairs2,