author | paulson |
Fri, 26 Sep 1997 10:21:14 +0200 | |
changeset 3718 | d78cf498a88c |
parent 3145 | 809a2c9902f7 |
child 4089 | 96fba19bcbe2 |
permissions | -rw-r--r-- |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Induct/Exp |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
Copyright 1997 University of Cambridge |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
6 |
Example of Mutual Induction via Iteratived Inductive Definitions: Expressions |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
8 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
9 |
open Exp; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
|
3145 | 11 |
AddSIs [eval.N, eval.X]; |
12 |
AddIs [eval.Op, eval.valOf]; |
|
3144 | 13 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
val eval_elim_cases = map (eval.mk_cases exp.simps) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')", |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
"(Op f a1 a2,sigma) -|-> (n,s')", |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
"(VALOF c RESULTIS e, s) -|-> (n, s1)" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
]; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
19 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
20 |
AddSEs eval_elim_cases; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
21 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
|
3145 | 23 |
goal thy "(X x, s[n/x]) -|-> (n, s[n/x])"; |
24 |
by (rtac (assign_same RS subst) 1 THEN resolve_tac eval.intrs 1); |
|
25 |
qed "var_assign_eval"; |
|
26 |
||
27 |
AddSIs [var_assign_eval]; |
|
28 |
||
29 |
||
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
30 |
(** Make the induction rule look nicer -- though eta_contract makes the new |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
31 |
version look worse than it is...**) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
32 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
33 |
goal thy "{((e,s),(n,s')). P e s n s'} = \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
34 |
\ Collect (split (%v. split (split P v)))"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
35 |
by (rtac Collect_cong 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
36 |
by (split_all_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
37 |
by (Simp_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
38 |
val split_lemma = result(); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
39 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
40 |
(*New induction rule. Note the form of the VALOF induction hypothesis*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
41 |
val major::prems = goal thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
42 |
"[| (e,s) -|-> (n,s'); \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
43 |
\ !!n s. P (N n) s n s; \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
44 |
\ !!s x. P (X x) s (s x) s; \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
45 |
\ !!e0 e1 f n0 n1 s s0 s1. \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
46 |
\ [| (e0,s) -|-> (n0,s0); P e0 s n0 s0; \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
47 |
\ (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1 \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
48 |
\ |] ==> P (Op f e0 e1) s (f n0 n1) s1; \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
49 |
\ !!c e n s s0 s1. \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
50 |
\ [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \ |
3145 | 51 |
\ (c,s) -[eval]-> s0; \ |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
52 |
\ (e,s0) -|-> (n,s1); P e s0 n s1 |] \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
53 |
\ ==> P (VALOF c RESULTIS e) s n s1 \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
54 |
\ |] ==> P e s n s'"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
55 |
by (rtac (major RS eval.induct) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
56 |
by (blast_tac (!claset addIs prems) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
57 |
by (blast_tac (!claset addIs prems) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
58 |
by (blast_tac (!claset addIs prems) 1); |
3145 | 59 |
by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
60 |
by (fast_tac (!claset addIs prems addss (!simpset addsimps [split_lemma])) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
61 |
qed "eval_induct"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
62 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
63 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
64 |
(*Lemma for Function_eval. The major premise is that (c,s) executes to s1 |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
65 |
using eval restricted to its functional part. Note that the execution |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
66 |
(c,s) -[eval]-> s2 can use unrestricted eval! The reason is that |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
67 |
the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
68 |
functional on the argument (c,s). |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
69 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
70 |
goal thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
71 |
"!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
72 |
\ ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
73 |
by (etac exec.induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
74 |
by (ALLGOALS Full_simp_tac); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
75 |
by (Blast_tac 3); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
76 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
77 |
by (rewtac Unique_def); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
78 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
79 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
80 |
by (Blast_tac 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
81 |
by (blast_tac (!claset addEs [exec_WHILE_case]) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
82 |
by (thin_tac "(?c,s2) -[?ev]-> s3" 1); |
3718 | 83 |
by (Clarify_tac 1); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
84 |
by (etac exec_WHILE_case 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
85 |
by (ALLGOALS Fast_tac); (*Blast_tac: proof fails*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
86 |
qed "com_Unique"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
87 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
88 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
89 |
(*Expression evaluation is functional, or deterministic*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
90 |
goal thy "Function eval"; |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
91 |
by (simp_tac (!simpset addsimps [Function_def]) 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
92 |
by (REPEAT (rtac allI 1)); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
93 |
by (rtac impI 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
94 |
by (etac eval_induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
95 |
by (dtac com_Unique 4); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
96 |
by (ALLGOALS (full_simp_tac (!simpset addsimps [Unique_def]))); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
97 |
by (ALLGOALS Blast_tac); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
98 |
qed "Function_eval"; |
3144 | 99 |
|
100 |
||
101 |
goal thy "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"; |
|
3145 | 102 |
by (etac eval_induct 1); |
3144 | 103 |
by (ALLGOALS Asm_simp_tac); |
104 |
val lemma = result(); |
|
105 |
bind_thm ("eval_N_E", refl RSN (2, lemma RS mp)); |
|
106 |
||
107 |
AddSEs [eval_N_E]; |
|
108 |
||
109 |
||
110 |
(*This theorem says that "WHILE TRUE DO c" cannot terminate*) |
|
111 |
goal thy "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"; |
|
112 |
by (etac exec.induct 1); |
|
113 |
by (Auto_tac()); |
|
114 |
bind_thm ("while_true_E", refl RSN (2, result() RS mp)); |
|
115 |
||
116 |
||
117 |
(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and WHILE e DO c **) |
|
118 |
||
119 |
goal thy "!!x. (c',s) -[eval]-> t ==> \ |
|
120 |
\ (c' = WHILE e DO c) --> \ |
|
121 |
\ (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"; |
|
122 |
by (etac exec.induct 1); |
|
3145 | 123 |
by (ALLGOALS Asm_simp_tac); |
3144 | 124 |
by (ALLGOALS Blast_tac); |
125 |
bind_thm ("while_if1", refl RSN (2, result() RS mp)); |
|
126 |
||
127 |
||
128 |
goal thy "!!x. (c',s) -[eval]-> t ==> \ |
|
129 |
\ (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \ |
|
130 |
\ (WHILE e DO c, s) -[eval]-> t"; |
|
131 |
by (etac exec.induct 1); |
|
3145 | 132 |
by (ALLGOALS Asm_simp_tac); |
3144 | 133 |
by (ALLGOALS Blast_tac); |
134 |
bind_thm ("while_if2", refl RSN (2, result() RS mp)); |
|
135 |
||
136 |
||
137 |
goal thy "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) = \ |
|
138 |
\ ((WHILE e DO c, s) -[eval]-> t)"; |
|
139 |
by (blast_tac (!claset addIs [while_if1, while_if2]) 1); |
|
140 |
qed "while_if"; |
|
141 |
||
142 |
||
143 |
||
3145 | 144 |
(** Equivalence of (IF e THEN c1 ELSE c2);;c |
145 |
and IF e THEN (c1;;c) ELSE (c2;;c) **) |
|
146 |
||
147 |
goal thy "!!x. (c',s) -[eval]-> t ==> \ |
|
148 |
\ (c' = (IF e THEN c1 ELSE c2);;c) --> \ |
|
149 |
\ (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"; |
|
150 |
by (etac exec.induct 1); |
|
151 |
by (ALLGOALS Asm_simp_tac); |
|
152 |
by (Blast_tac 1); |
|
153 |
bind_thm ("if_semi1", refl RSN (2, result() RS mp)); |
|
154 |
||
155 |
||
156 |
goal thy "!!x. (c',s) -[eval]-> t ==> \ |
|
157 |
\ (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \ |
|
158 |
\ ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"; |
|
159 |
by (etac exec.induct 1); |
|
160 |
by (ALLGOALS Asm_simp_tac); |
|
161 |
by (ALLGOALS Blast_tac); |
|
162 |
bind_thm ("if_semi2", refl RSN (2, result() RS mp)); |
|
163 |
||
164 |
||
165 |
goal thy "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) = \ |
|
166 |
\ ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"; |
|
167 |
by (blast_tac (!claset addIs [if_semi1, if_semi2]) 1); |
|
168 |
qed "if_semi"; |
|
169 |
||
170 |
||
171 |
||
3144 | 172 |
(** Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e) |
173 |
and VALOF c1;;c2 RESULTIS e |
|
174 |
**) |
|
175 |
||
176 |
goal thy "!!x. (e',s) -|-> (v,s') ==> \ |
|
177 |
\ (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \ |
|
178 |
\ (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"; |
|
3145 | 179 |
by (etac eval_induct 1); |
180 |
by (ALLGOALS Asm_simp_tac); |
|
181 |
by (Blast_tac 1); |
|
3144 | 182 |
bind_thm ("valof_valof1", refl RSN (2, result() RS mp)); |
183 |
||
184 |
||
185 |
goal thy "!!x. (e',s) -|-> (v,s') ==> \ |
|
186 |
\ (e' = VALOF c1;;c2 RESULTIS e) --> \ |
|
187 |
\ (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"; |
|
3145 | 188 |
by (etac eval_induct 1); |
189 |
by (ALLGOALS Asm_simp_tac); |
|
190 |
by (Blast_tac 1); |
|
3144 | 191 |
bind_thm ("valof_valof2", refl RSN (2, result() RS mp)); |
192 |
||
193 |
||
194 |
goal thy "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = \ |
|
195 |
\ ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"; |
|
196 |
by (blast_tac (!claset addIs [valof_valof1, valof_valof2]) 1); |
|
197 |
qed "valof_valof"; |
|
198 |
||
3145 | 199 |
|
200 |
(** Equivalence of VALOF SKIP RESULTIS e and e **) |
|
201 |
||
202 |
goal thy "!!x. (e',s) -|-> (v,s') ==> \ |
|
203 |
\ (e' = VALOF SKIP RESULTIS e) --> \ |
|
204 |
\ (e, s) -|-> (v,s')"; |
|
205 |
by (etac eval_induct 1); |
|
206 |
by (ALLGOALS Asm_simp_tac); |
|
207 |
by (Blast_tac 1); |
|
208 |
bind_thm ("valof_skip1", refl RSN (2, result() RS mp)); |
|
209 |
||
210 |
goal thy "!!x. (e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"; |
|
211 |
by (Blast_tac 1); |
|
212 |
qed "valof_skip2"; |
|
213 |
||
214 |
goal thy "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))"; |
|
215 |
by (blast_tac (!claset addIs [valof_skip1, valof_skip2]) 1); |
|
216 |
qed "valof_skip"; |
|
217 |
||
218 |
||
219 |
(** Equivalence of VALOF x:=e RESULTIS x and e **) |
|
220 |
||
221 |
goal thy "!!x. (e',s) -|-> (v,s'') ==> \ |
|
222 |
\ (e' = VALOF x:=e RESULTIS X x) --> \ |
|
223 |
\ (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))"; |
|
224 |
by (etac eval_induct 1); |
|
225 |
by (ALLGOALS Asm_simp_tac); |
|
226 |
by (thin_tac "?PP-->?QQ" 1); |
|
3718 | 227 |
by (Clarify_tac 1); |
3145 | 228 |
by (Simp_tac 1); |
229 |
by (Blast_tac 1); |
|
230 |
bind_thm ("valof_assign1", refl RSN (2, result() RS mp)); |
|
231 |
||
232 |
||
233 |
goal thy "!!x. (e,s) -|-> (v,s') ==> \ |
|
234 |
\ (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])"; |
|
235 |
by (Blast_tac 1); |
|
236 |
qed "valof_assign2"; |