author | wenzelm |
Thu, 05 Jul 2007 00:15:44 +0200 | |
changeset 23587 | 46d01f5e1e5b |
parent 23583 | 00751df1f98c |
child 23596 | f8381a95c49c |
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 |
|
22937 | 8 |
infix 1 then_conv; |
9 |
infix 0 else_conv; |
|
23169 | 10 |
|
23490 | 11 |
type conv = cterm -> thm; |
12 |
||
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
13 |
signature CONV = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
14 |
sig |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
15 |
val no_conv: conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
16 |
val all_conv: conv |
23490 | 17 |
val is_refl: thm -> bool |
22937 | 18 |
val then_conv: conv * conv -> conv |
19 |
val else_conv: conv * conv -> conv |
|
22926 | 20 |
val first_conv: conv list -> conv |
21 |
val every_conv: conv list -> conv |
|
22937 | 22 |
val try_conv: conv -> conv |
23 |
val repeat_conv: conv -> conv |
|
22926 | 24 |
val cache_conv: conv -> conv |
25 |
val abs_conv: conv -> conv |
|
26 |
val combination_conv: conv -> conv -> conv |
|
27 |
val comb_conv: conv -> conv |
|
28 |
val arg_conv: conv -> conv |
|
29 |
val fun_conv: conv -> conv |
|
30 |
val arg1_conv: conv -> conv |
|
31 |
val fun2_conv: conv -> conv |
|
23034 | 32 |
val binop_conv: conv -> conv |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
33 |
val forall_conv: int -> conv -> conv |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
34 |
val concl_conv: int -> conv -> conv |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
35 |
val prems_conv: int -> conv -> conv |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
36 |
val fconv_rule: conv -> thm -> thm |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
37 |
val gconv_rule: conv -> int -> thm -> thm |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
38 |
end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
39 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
40 |
structure Conv: CONV = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
41 |
struct |
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 |
(* conversionals *) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
44 |
|
22926 | 45 |
type conv = cterm -> thm; |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
46 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
47 |
fun no_conv _ = raise CTERM ("no conversion", []); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
48 |
val all_conv = Thm.reflexive; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
49 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
50 |
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
|
51 |
|
22937 | 52 |
fun (cv1 then_conv cv2) ct = |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
53 |
let |
22926 | 54 |
val eq1 = cv1 ct; |
55 |
val eq2 = cv2 (Thm.rhs_of eq1); |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
56 |
in |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
57 |
if is_refl eq1 then eq2 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
58 |
else if is_refl eq2 then eq1 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
59 |
else Thm.transitive eq1 eq2 |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
60 |
end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
61 |
|
22937 | 62 |
fun (cv1 else_conv cv2) ct = |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
63 |
(cv1 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
64 |
handle THM _ => cv2 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
65 |
| CTERM _ => cv2 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
66 |
| TERM _ => cv2 ct |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
67 |
| TYPE _ => cv2 ct); |
22926 | 68 |
|
22937 | 69 |
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv; |
70 |
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; |
|
22926 | 71 |
|
22937 | 72 |
fun try_conv cv = cv else_conv all_conv; |
73 |
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; |
|
22926 | 74 |
|
75 |
fun cache_conv cv = |
|
76 |
let |
|
77 |
val cache = ref Termtab.empty; |
|
78 |
fun conv ct = |
|
23587 | 79 |
(case Termtab.lookup (! cache) (Thm.term_of ct) of |
22926 | 80 |
SOME th => th |
81 |
| NONE => |
|
82 |
let val th = cv ct |
|
23587 | 83 |
in change cache (Termtab.update (Thm.term_of ct, th)); th end); |
22926 | 84 |
in conv end; |
85 |
||
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
86 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
87 |
|
22926 | 88 |
(** Pure conversions **) |
89 |
||
90 |
(* lambda terms *) |
|
91 |
||
92 |
fun abs_conv cv ct = |
|
23587 | 93 |
(case Thm.term_of ct of |
22926 | 94 |
Abs (x, _, _) => |
95 |
let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct |
|
96 |
in Thm.abstract_rule x v (cv ct') end |
|
97 |
| _ => raise CTERM ("abs_conv", [ct])); |
|
98 |
||
99 |
fun combination_conv cv1 cv2 ct = |
|
100 |
let val (ct1, ct2) = Thm.dest_comb ct |
|
101 |
in Thm.combination (cv1 ct1) (cv2 ct2) end; |
|
102 |
||
103 |
fun comb_conv cv = combination_conv cv cv; |
|
104 |
fun arg_conv cv = combination_conv all_conv cv; |
|
105 |
fun fun_conv cv = combination_conv cv all_conv; |
|
106 |
||
107 |
val arg1_conv = fun_conv o arg_conv; |
|
108 |
val fun2_conv = fun_conv o fun_conv; |
|
109 |
||
23034 | 110 |
fun binop_conv cv = combination_conv (arg_conv cv) cv; |
22926 | 111 |
|
23169 | 112 |
|
22926 | 113 |
(* logic *) |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
114 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
115 |
(*rewrite B in !!x1 ... xn. B*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
116 |
fun forall_conv 0 cv ct = cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
117 |
| forall_conv n cv ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
118 |
(case try Thm.dest_comb ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
119 |
NONE => cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
120 |
| SOME (A, B) => |
23587 | 121 |
(case (Thm.term_of A, Thm.term_of B) of |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
122 |
(Const ("all", _), Abs (x, _, _)) => |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
123 |
let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in |
22926 | 124 |
Thm.combination (all_conv A) |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
125 |
(Thm.abstract_rule x v (forall_conv (n - 1) cv B')) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
126 |
end |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
127 |
| _ => cv ct)); |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
128 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
129 |
(*rewrite B in A1 ==> ... ==> An ==> B*) |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
130 |
fun concl_conv 0 cv ct = cv ct |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
131 |
| concl_conv n cv ct = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
132 |
(case try Thm.dest_implies ct of |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
133 |
NONE => cv ct |
22926 | 134 |
| SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B)); |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
135 |
|
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
136 |
(*rewrite the A's in A1 ==> ... ==> An ==> B*) |
22926 | 137 |
fun prems_conv 0 _ = all_conv |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
138 |
| prems_conv n cv = |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
139 |
let |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
140 |
fun conv i ct = |
22926 | 141 |
if i = n + 1 then all_conv ct |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
142 |
else |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
143 |
(case try Thm.dest_implies ct of |
22926 | 144 |
NONE => all_conv ct |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
145 |
| SOME (A, B) => Drule.imp_cong_rule (cv A) (conv (i + 1) B)); |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
146 |
in conv 1 end; |
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
147 |
|
23534 | 148 |
fun fconv_rule cv th = Thm.equal_elim (cv (Thm.cprop_of th)) th; (*FCONV_RULE in LCF*) |
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
149 |
|
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
150 |
fun gconv_rule cv i = Drule.with_subgoal i (fn th => |
23534 | 151 |
(case try (Thm.dest_implies o Thm.cprop_of) th of |
23583
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
152 |
SOME (A, B) => Thm.equal_elim (Drule.imp_cong_rule (cv A) (all_conv B)) th |
00751df1f98c
else_conv: only handle THM | CTERM | TERM | TYPE;
wenzelm
parents:
23534
diff
changeset
|
153 |
| NONE => raise THM ("gconv_rule", i, [th]))); |
23411
c524900454f3
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
chaieb
parents:
23169
diff
changeset
|
154 |
|
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset
|
155 |
end; |