author | wenzelm |
Mon, 22 Jun 1998 17:26:46 +0200 | |
changeset 5069 | 3ea049f7979d |
parent 4477 | b3e5857d8d99 |
child 5143 | b94cd208f073 |
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 |
|
5069 | 23 |
Goal "(X x, s[n/x]) -|-> (n, s[n/x])"; |
3145 | 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 |
|
5069 | 33 |
Goal "{((e,s),(n,s')). P e s n s'} = \ |
3120
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); |
4089 | 56 |
by (blast_tac (claset() addIs prems) 1); |
57 |
by (blast_tac (claset() addIs prems) 1); |
|
58 |
by (blast_tac (claset() addIs prems) 1); |
|
3145 | 59 |
by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1); |
4264 | 60 |
by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma])); |
3120
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 |
*) |
5069 | 70 |
Goal |
3120
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); |
4089 | 81 |
by (blast_tac (claset() addEs [exec_WHILE_case]) 1); |
3120
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*) |
5069 | 90 |
Goalw [Function_def] "Function eval"; |
4264 | 91 |
by (strip_tac 1); |
92 |
by (split_all_tac 1); |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
93 |
by (etac eval_induct 1); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
94 |
by (dtac com_Unique 4); |
4089 | 95 |
by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def]))); |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
96 |
by (ALLGOALS Blast_tac); |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
97 |
qed "Function_eval"; |
3144 | 98 |
|
99 |
||
5069 | 100 |
Goal "!!x. (e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"; |
3145 | 101 |
by (etac eval_induct 1); |
3144 | 102 |
by (ALLGOALS Asm_simp_tac); |
103 |
val lemma = result(); |
|
104 |
bind_thm ("eval_N_E", refl RSN (2, lemma RS mp)); |
|
105 |
||
106 |
AddSEs [eval_N_E]; |
|
107 |
||
108 |
||
109 |
(*This theorem says that "WHILE TRUE DO c" cannot terminate*) |
|
5069 | 110 |
Goal "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"; |
3144 | 111 |
by (etac exec.induct 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4264
diff
changeset
|
112 |
by Auto_tac; |
3144 | 113 |
bind_thm ("while_true_E", refl RSN (2, result() RS mp)); |
114 |
||
115 |
||
116 |
(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and WHILE e DO c **) |
|
117 |
||
5069 | 118 |
Goal "!!x. (c',s) -[eval]-> t ==> \ |
3144 | 119 |
\ (c' = WHILE e DO c) --> \ |
120 |
\ (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"; |
|
121 |
by (etac exec.induct 1); |
|
3145 | 122 |
by (ALLGOALS Asm_simp_tac); |
3144 | 123 |
by (ALLGOALS Blast_tac); |
124 |
bind_thm ("while_if1", refl RSN (2, result() RS mp)); |
|
125 |
||
126 |
||
5069 | 127 |
Goal "!!x. (c',s) -[eval]-> t ==> \ |
3144 | 128 |
\ (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \ |
129 |
\ (WHILE e DO c, s) -[eval]-> t"; |
|
130 |
by (etac exec.induct 1); |
|
3145 | 131 |
by (ALLGOALS Asm_simp_tac); |
3144 | 132 |
by (ALLGOALS Blast_tac); |
133 |
bind_thm ("while_if2", refl RSN (2, result() RS mp)); |
|
134 |
||
135 |
||
5069 | 136 |
Goal "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) = \ |
3144 | 137 |
\ ((WHILE e DO c, s) -[eval]-> t)"; |
4089 | 138 |
by (blast_tac (claset() addIs [while_if1, while_if2]) 1); |
3144 | 139 |
qed "while_if"; |
140 |
||
141 |
||
142 |
||
3145 | 143 |
(** Equivalence of (IF e THEN c1 ELSE c2);;c |
144 |
and IF e THEN (c1;;c) ELSE (c2;;c) **) |
|
145 |
||
5069 | 146 |
Goal "!!x. (c',s) -[eval]-> t ==> \ |
3145 | 147 |
\ (c' = (IF e THEN c1 ELSE c2);;c) --> \ |
148 |
\ (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"; |
|
149 |
by (etac exec.induct 1); |
|
150 |
by (ALLGOALS Asm_simp_tac); |
|
151 |
by (Blast_tac 1); |
|
152 |
bind_thm ("if_semi1", refl RSN (2, result() RS mp)); |
|
153 |
||
154 |
||
5069 | 155 |
Goal "!!x. (c',s) -[eval]-> t ==> \ |
3145 | 156 |
\ (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \ |
157 |
\ ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"; |
|
158 |
by (etac exec.induct 1); |
|
159 |
by (ALLGOALS Asm_simp_tac); |
|
160 |
by (ALLGOALS Blast_tac); |
|
161 |
bind_thm ("if_semi2", refl RSN (2, result() RS mp)); |
|
162 |
||
163 |
||
5069 | 164 |
Goal "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) = \ |
3145 | 165 |
\ ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"; |
4089 | 166 |
by (blast_tac (claset() addIs [if_semi1, if_semi2]) 1); |
3145 | 167 |
qed "if_semi"; |
168 |
||
169 |
||
170 |
||
3144 | 171 |
(** Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e) |
172 |
and VALOF c1;;c2 RESULTIS e |
|
173 |
**) |
|
174 |
||
5069 | 175 |
Goal "!!x. (e',s) -|-> (v,s') ==> \ |
3144 | 176 |
\ (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \ |
177 |
\ (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"; |
|
3145 | 178 |
by (etac eval_induct 1); |
179 |
by (ALLGOALS Asm_simp_tac); |
|
180 |
by (Blast_tac 1); |
|
3144 | 181 |
bind_thm ("valof_valof1", refl RSN (2, result() RS mp)); |
182 |
||
183 |
||
5069 | 184 |
Goal "!!x. (e',s) -|-> (v,s') ==> \ |
3144 | 185 |
\ (e' = VALOF c1;;c2 RESULTIS e) --> \ |
186 |
\ (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"; |
|
3145 | 187 |
by (etac eval_induct 1); |
188 |
by (ALLGOALS Asm_simp_tac); |
|
189 |
by (Blast_tac 1); |
|
3144 | 190 |
bind_thm ("valof_valof2", refl RSN (2, result() RS mp)); |
191 |
||
192 |
||
5069 | 193 |
Goal "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = \ |
3144 | 194 |
\ ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"; |
4089 | 195 |
by (blast_tac (claset() addIs [valof_valof1, valof_valof2]) 1); |
3144 | 196 |
qed "valof_valof"; |
197 |
||
3145 | 198 |
|
199 |
(** Equivalence of VALOF SKIP RESULTIS e and e **) |
|
200 |
||
5069 | 201 |
Goal "!!x. (e',s) -|-> (v,s') ==> \ |
3145 | 202 |
\ (e' = VALOF SKIP RESULTIS e) --> \ |
203 |
\ (e, s) -|-> (v,s')"; |
|
204 |
by (etac eval_induct 1); |
|
205 |
by (ALLGOALS Asm_simp_tac); |
|
206 |
by (Blast_tac 1); |
|
207 |
bind_thm ("valof_skip1", refl RSN (2, result() RS mp)); |
|
208 |
||
5069 | 209 |
Goal "!!x. (e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"; |
3145 | 210 |
by (Blast_tac 1); |
211 |
qed "valof_skip2"; |
|
212 |
||
5069 | 213 |
Goal "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))"; |
4089 | 214 |
by (blast_tac (claset() addIs [valof_skip1, valof_skip2]) 1); |
3145 | 215 |
qed "valof_skip"; |
216 |
||
217 |
||
218 |
(** Equivalence of VALOF x:=e RESULTIS x and e **) |
|
219 |
||
5069 | 220 |
Goal "!!x. (e',s) -|-> (v,s'') ==> \ |
3145 | 221 |
\ (e' = VALOF x:=e RESULTIS X x) --> \ |
222 |
\ (EX s'. (e, s) -|-> (v,s') & (s'' = s'[v/x]))"; |
|
223 |
by (etac eval_induct 1); |
|
224 |
by (ALLGOALS Asm_simp_tac); |
|
225 |
by (thin_tac "?PP-->?QQ" 1); |
|
3718 | 226 |
by (Clarify_tac 1); |
3145 | 227 |
by (Simp_tac 1); |
228 |
by (Blast_tac 1); |
|
229 |
bind_thm ("valof_assign1", refl RSN (2, result() RS mp)); |
|
230 |
||
231 |
||
5069 | 232 |
Goal "!!x. (e,s) -|-> (v,s') ==> \ |
3145 | 233 |
\ (VALOF x:=e RESULTIS X x, s) -|-> (v,s'[v/x])"; |
234 |
by (Blast_tac 1); |
|
235 |
qed "valof_assign2"; |