author | wenzelm |
Thu, 10 May 2007 00:39:51 +0200 | |
changeset 22905 | dab6a898b47c |
child 22926 | fb6917e426da |
permissions | -rw-r--r-- |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/conv.ML |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
3 |
Author: Amine Chaieb and Makarius |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
4 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
5 |
Conversions: primitive equality reasoning. |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
6 |
*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
7 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
8 |
infix 1 AND; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
9 |
infix 0 OR; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
10 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
11 |
signature CONV = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
12 |
sig |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
13 |
type conv = cterm -> thm |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
14 |
val no_conv: conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
15 |
val all_conv: conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
16 |
val option_conv: conv -> cterm -> thm option |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
17 |
val AND: conv * conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
18 |
val OR: conv * conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
19 |
val forall_conv: int -> conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
20 |
val concl_conv: int -> conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
21 |
val prems_conv: int -> (int -> conv) -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
22 |
val goals_conv: (int -> bool) -> conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
23 |
val fconv_rule: conv -> thm -> thm |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
24 |
end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
25 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
26 |
structure Conv: CONV = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
27 |
struct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
28 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
29 |
(* conversionals *) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
30 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
31 |
type conv = cterm -> thm |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
32 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
33 |
fun no_conv _ = raise CTERM ("no conversion", []); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
34 |
val all_conv = Thm.reflexive; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
35 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
36 |
val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
37 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
38 |
fun option_conv conv ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
39 |
(case try conv ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
40 |
NONE => NONE |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
41 |
| SOME eq => if is_refl eq then NONE else SOME eq); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
42 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
43 |
fun (conv1 AND conv2) ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
44 |
let |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
45 |
val eq1 = conv1 ct; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
46 |
val eq2 = conv2 (Thm.rhs_of eq1); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
47 |
in |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
48 |
if is_refl eq1 then eq2 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
49 |
else if is_refl eq2 then eq1 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
50 |
else Thm.transitive eq1 eq2 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
51 |
end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
52 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
53 |
fun (conv1 OR conv2) ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
54 |
(case try conv1 ct of SOME eq => eq | NONE => conv2 ct); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
55 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
56 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
57 |
(* Pure conversions *) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
58 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
59 |
(*rewrite B in !!x1 ... xn. B*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
60 |
fun forall_conv 0 cv ct = cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
61 |
| forall_conv n cv ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
62 |
(case try Thm.dest_comb ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
63 |
NONE => cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
64 |
| SOME (A, B) => |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
65 |
(case (term_of A, term_of B) of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
66 |
(Const ("all", _), Abs (x, _, _)) => |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
67 |
let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
68 |
Thm.combination (Thm.reflexive A) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
69 |
(Thm.abstract_rule x v (forall_conv (n - 1) cv B')) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
70 |
end |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
71 |
| _ => cv ct)); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
72 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
73 |
(*rewrite B in A1 ==> ... ==> An ==> B*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
74 |
fun concl_conv 0 cv ct = cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
75 |
| concl_conv n cv ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
76 |
(case try Thm.dest_implies ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
77 |
NONE => cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
78 |
| SOME (A, B) => Drule.imp_cong_rule (reflexive A) (concl_conv (n - 1) cv B)); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
79 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
80 |
(*rewrite the A's in A1 ==> ... ==> An ==> B*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
81 |
fun prems_conv 0 _ = reflexive |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
82 |
| prems_conv n cv = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
83 |
let |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
84 |
fun conv i ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
85 |
if i = n + 1 then reflexive ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
86 |
else |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
87 |
(case try Thm.dest_implies ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
88 |
NONE => reflexive ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
89 |
| SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B)); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
90 |
in conv 1 end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
91 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
92 |
fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
93 |
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
94 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
95 |
end; |