author  berghofe 
Fri, 24 Jul 1998 13:39:47 +0200  
changeset 5191  8ceaa19f7717 
parent 5148  74919e8f221c 
child 5223  4cb05273f764 
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 
*) 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

70 
Goal "(c,s) [eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]> s1 \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

71 
\ ==> (ALL s2. (c,s) [eval]> s2 > s2=s1)"; 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

72 
by (etac exec.induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

73 
by (ALLGOALS Full_simp_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

74 
by (Blast_tac 3); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

75 
by (Blast_tac 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

76 
by (rewtac Unique_def); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

77 
by (Blast_tac 1); 
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); 
4089  80 
by (blast_tac (claset() addEs [exec_WHILE_case]) 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

81 
by (thin_tac "(?c,s2) [?ev]> s3" 1); 
3718  82 
by (Clarify_tac 1); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

83 
by (etac exec_WHILE_case 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

84 
by (ALLGOALS Fast_tac); (*Blast_tac: proof fails*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

85 
qed "com_Unique"; 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

86 

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 
(*Expression evaluation is functional, or deterministic*) 
5069  89 
Goalw [Function_def] "Function eval"; 
4264  90 
by (strip_tac 1); 
91 
by (split_all_tac 1); 

3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

92 
by (etac eval_induct 1); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

93 
by (dtac com_Unique 4); 
4089  94 
by (ALLGOALS (full_simp_tac (simpset() addsimps [Unique_def]))); 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

95 
by (ALLGOALS Blast_tac); 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

96 
qed "Function_eval"; 
3144  97 

98 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

99 
Goal "(e,s) > (v,s') ==> (e = N n) > (v=n & s'=s)"; 
3145  100 
by (etac eval_induct 1); 
3144  101 
by (ALLGOALS Asm_simp_tac); 
102 
val lemma = result(); 

103 
bind_thm ("eval_N_E", refl RSN (2, lemma RS mp)); 

104 

105 
AddSEs [eval_N_E]; 

106 

107 

108 
(*This theorem says that "WHILE TRUE DO c" cannot terminate*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

109 
Goal "(c', s) [eval]> t ==> (c' = WHILE (N 0) DO c) > False"; 
3144  110 
by (etac exec.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4264
diff
changeset

111 
by Auto_tac; 
3144  112 
bind_thm ("while_true_E", refl RSN (2, result() RS mp)); 
113 

114 

115 
(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and WHILE e DO c **) 

116 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

117 
Goal "(c',s) [eval]> t ==> \ 
3144  118 
\ (c' = WHILE e DO c) > \ 
119 
\ (IF e THEN c;;c' ELSE SKIP, s) [eval]> t"; 

120 
by (etac exec.induct 1); 

3145  121 
by (ALLGOALS Asm_simp_tac); 
3144  122 
by (ALLGOALS Blast_tac); 
123 
bind_thm ("while_if1", refl RSN (2, result() RS mp)); 

124 

125 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

126 
Goal "(c',s) [eval]> t ==> \ 
3144  127 
\ (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) > \ 
128 
\ (WHILE e DO c, s) [eval]> t"; 

129 
by (etac exec.induct 1); 

3145  130 
by (ALLGOALS Asm_simp_tac); 
3144  131 
by (ALLGOALS Blast_tac); 
132 
bind_thm ("while_if2", refl RSN (2, result() RS mp)); 

133 

134 

5069  135 
Goal "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) [eval]> t) = \ 
3144  136 
\ ((WHILE e DO c, s) [eval]> t)"; 
4089  137 
by (blast_tac (claset() addIs [while_if1, while_if2]) 1); 
3144  138 
qed "while_if"; 
139 

140 

141 

3145  142 
(** Equivalence of (IF e THEN c1 ELSE c2);;c 
143 
and IF e THEN (c1;;c) ELSE (c2;;c) **) 

144 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

145 
Goal "(c',s) [eval]> t ==> \ 
3145  146 
\ (c' = (IF e THEN c1 ELSE c2);;c) > \ 
147 
\ (IF e THEN (c1;;c) ELSE (c2;;c), s) [eval]> t"; 

148 
by (etac exec.induct 1); 

149 
by (ALLGOALS Asm_simp_tac); 

150 
by (Blast_tac 1); 

151 
bind_thm ("if_semi1", refl RSN (2, result() RS mp)); 

152 

153 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

154 
Goal "(c',s) [eval]> t ==> \ 
3145  155 
\ (c' = IF e THEN (c1;;c) ELSE (c2;;c)) > \ 
156 
\ ((IF e THEN c1 ELSE c2);;c, s) [eval]> t"; 

157 
by (etac exec.induct 1); 

158 
by (ALLGOALS Asm_simp_tac); 

159 
by (ALLGOALS Blast_tac); 

160 
bind_thm ("if_semi2", refl RSN (2, result() RS mp)); 

161 

162 

5069  163 
Goal "(((IF e THEN c1 ELSE c2);;c, s) [eval]> t) = \ 
3145  164 
\ ((IF e THEN (c1;;c) ELSE (c2;;c), s) [eval]> t)"; 
4089  165 
by (blast_tac (claset() addIs [if_semi1, if_semi2]) 1); 
3145  166 
qed "if_semi"; 
167 

168 

169 

3144  170 
(** Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e) 
171 
and VALOF c1;;c2 RESULTIS e 

172 
**) 

173 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

174 
Goal "(e',s) > (v,s') ==> \ 
3144  175 
\ (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) > \ 
176 
\ (VALOF c1;;c2 RESULTIS e, s) > (v,s')"; 

3145  177 
by (etac eval_induct 1); 
178 
by (ALLGOALS Asm_simp_tac); 

179 
by (Blast_tac 1); 

3144  180 
bind_thm ("valof_valof1", refl RSN (2, result() RS mp)); 
181 

182 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

183 
Goal "(e',s) > (v,s') ==> \ 
3144  184 
\ (e' = VALOF c1;;c2 RESULTIS e) > \ 
185 
\ (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) > (v,s')"; 

3145  186 
by (etac eval_induct 1); 
187 
by (ALLGOALS Asm_simp_tac); 

188 
by (Blast_tac 1); 

3144  189 
bind_thm ("valof_valof2", refl RSN (2, result() RS mp)); 
190 

191 

5069  192 
Goal "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) > (v,s')) = \ 
3144  193 
\ ((VALOF c1;;c2 RESULTIS e, s) > (v,s'))"; 
4089  194 
by (blast_tac (claset() addIs [valof_valof1, valof_valof2]) 1); 
3144  195 
qed "valof_valof"; 
196 

3145  197 

198 
(** Equivalence of VALOF SKIP RESULTIS e and e **) 

199 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

200 
Goal "(e',s) > (v,s') ==> \ 
3145  201 
\ (e' = VALOF SKIP RESULTIS e) > \ 
202 
\ (e, s) > (v,s')"; 

203 
by (etac eval_induct 1); 

204 
by (ALLGOALS Asm_simp_tac); 

205 
by (Blast_tac 1); 

206 
bind_thm ("valof_skip1", refl RSN (2, result() RS mp)); 

207 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

208 
Goal "(e,s) > (v,s') ==> (VALOF SKIP RESULTIS e, s) > (v,s')"; 
3145  209 
by (Blast_tac 1); 
210 
qed "valof_skip2"; 

211 

5069  212 
Goal "((VALOF SKIP RESULTIS e, s) > (v,s')) = ((e, s) > (v,s'))"; 
4089  213 
by (blast_tac (claset() addIs [valof_skip1, valof_skip2]) 1); 
3145  214 
qed "valof_skip"; 
215 

216 

217 
(** Equivalence of VALOF x:=e RESULTIS x and e **) 

218 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

219 
Goal "(e',s) > (v,s'') ==> \ 
3145  220 
\ (e' = VALOF x:=e RESULTIS X x) > \ 
221 
\ (EX s'. (e, s) > (v,s') & (s'' = s'[v/x]))"; 

222 
by (etac eval_induct 1); 

223 
by (ALLGOALS Asm_simp_tac); 

224 
by (thin_tac "?PP>?QQ" 1); 

3718  225 
by (Clarify_tac 1); 
3145  226 
by (Simp_tac 1); 
227 
by (Blast_tac 1); 

228 
bind_thm ("valof_assign1", refl RSN (2, result() RS mp)); 

229 

230 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

231 
Goal "(e,s) > (v,s') ==> \ 
3145  232 
\ (VALOF x:=e RESULTIS X x, s) > (v,s'[v/x])"; 
233 
by (Blast_tac 1); 

234 
qed "valof_assign2"; 