author  wenzelm 
Mon, 22 Jun 1998 17:26:46 +0200  
changeset 5069  3ea049f7979d 
parent 4477  b3e5857d8d99 
child 5143  b94cd208f073 
permissions  rwrr 
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"; 