author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44965  9e17d632a9ed 
child 58305  57752a91eec4 
permissions  rwrr 
36862  1 
(* Title: HOL/Induct/Com.thy 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Copyright 1997 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 

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

5 
Example of Mutual Induction via Iteratived Inductive Definitions: Commands 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

7 

14527  8 
header{*Mutual Induction via Iteratived Inductive Definitions*} 
9 

16417  10 
theory Com imports Main begin 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

12 
typedecl loc 
41818  13 
type_synonym state = "loc => nat" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 

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

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

16 
exp = N nat 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
 X loc 
24824  18 
 Op "nat => nat => nat" exp exp 
10759  19 
 valOf com exp ("VALOF _ RESULTIS _" 60) 
20 
and 

21 
com = SKIP 

24824  22 
 Assign loc exp (infixl ":=" 60) 
23 
 Semi com com ("_;;_" [60, 60] 60) 

24 
 Cond exp com com ("IF _ THEN _ ELSE _" 60) 

10759  25 
 While exp com ("WHILE _ DO _" 60) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

26 

14527  27 

28 
subsection {* Commands *} 

29 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

30 
text{* Execution of commands *} 
4264  31 

19736  32 
abbreviation (input) 
23746  33 
generic_rel ("_/ [_]> _" [50,0,50] 50) where 
19736  34 
"esig [eval]> ns == (esig,ns) \<in> eval" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

35 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

36 
text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*} 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 

23746  38 
inductive_set 
39 
exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" 

40 
and exec_rel :: "com * state => ((exp*state) * (nat*state)) set => state => bool" 

41 
("_/ [_]> _" [50,0,50] 50) 

42 
for eval :: "((exp*state) * (nat*state)) set" 

43 
where 

44 
"csig [eval]> s == (csig,s) \<in> exec eval" 

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

45 

23746  46 
 Skip: "(SKIP,s) [eval]> s" 
47 

48 
 Assign: "(e,s) [eval]> (v,s') ==> (x := e, s) [eval]> s'(x:=v)" 

49 

50 
 Semi: "[ (c0,s) [eval]> s2; (c1,s2) [eval]> s1 ] 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

51 
==> (c0 ;; c1, s) [eval]> s1" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

52 

23746  53 
 IfTrue: "[ (e,s) [eval]> (0,s'); (c0,s') [eval]> s1 ] 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

54 
==> (IF e THEN c0 ELSE c1, s) [eval]> s1" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 

23746  56 
 IfFalse: "[ (e,s) [eval]> (Suc 0, s'); (c1,s') [eval]> s1 ] 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

57 
==> (IF e THEN c0 ELSE c1, s) [eval]> s1" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

58 

23746  59 
 WhileFalse: "(e,s) [eval]> (Suc 0, s1) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

60 
==> (WHILE e DO c, s) [eval]> s1" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

61 

23746  62 
 WhileTrue: "[ (e,s) [eval]> (0,s1); 
18260  63 
(c,s1) [eval]> s2; (WHILE e DO c, s2) [eval]> s3 ] 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

64 
==> (WHILE e DO c, s) [eval]> s3" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

65 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

66 
declare exec.intros [intro] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

67 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

68 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

69 
inductive_cases 
18260  70 
[elim!]: "(SKIP,s) [eval]> t" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

71 
and [elim!]: "(x:=a,s) [eval]> t" 
18260  72 
and [elim!]: "(c1;;c2, s) [eval]> t" 
73 
and [elim!]: "(IF e THEN c1 ELSE c2, s) [eval]> t" 

74 
and exec_WHILE_case: "(WHILE b DO c,s) [eval]> t" 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

75 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

76 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

77 
text{*Justifies using "exec" in the inductive definition of "eval"*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

78 
lemma exec_mono: "A<=B ==> exec(A) <= exec(B)" 
23746  79 
apply (rule subsetI) 
80 
apply (simp add: split_paired_all) 

81 
apply (erule exec.induct) 

82 
apply blast+ 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

83 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

84 

23746  85 
lemma [pred_set_conv]: 
86 
"((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)" 

44174
d1d79f0e1ea6
make more HOL theories work with separate set type
huffman
parents:
41818
diff
changeset

87 
unfolding subset_eq 
44965  88 
by (auto simp add: le_fun_def) 
23746  89 

90 
lemma [pred_set_conv]: 

91 
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)" 

44174
d1d79f0e1ea6
make more HOL theories work with separate set type
huffman
parents:
41818
diff
changeset

92 
unfolding subset_eq 
44965  93 
by (auto simp add: le_fun_def) 
23746  94 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

95 
text{*Command execution is functional (deterministic) provided evaluation is*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

96 
theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

97 
apply (simp add: single_valued_def) 
18260  98 
apply (intro allI) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

99 
apply (rule impI) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

100 
apply (erule exec.induct) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

101 
apply (blast elim: exec_WHILE_case)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

102 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

103 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

104 

14527  105 
subsection {* Expressions *} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

106 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

107 
text{* Evaluation of arithmetic expressions *} 
18260  108 

23746  109 
inductive_set 
110 
eval :: "((exp*state) * (nat*state)) set" 

111 
and eval_rel :: "[exp*state,nat*state] => bool" (infixl ">" 50) 

112 
where 

113 
"esig > ns == (esig, ns) \<in> eval" 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

114 

23746  115 
 N [intro!]: "(N(n),s) > (n,s)" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

116 

23746  117 
 X [intro!]: "(X(x),s) > (s(x),s)" 
118 

119 
 Op [intro]: "[ (e0,s) > (n0,s0); (e1,s0) > (n1,s1) ] 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

120 
==> (Op f e0 e1, s) > (f n0 n1, s1)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

121 

23746  122 
 valOf [intro]: "[ (c,s) [eval]> s0; (e,s0) > (n,s1) ] 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

123 
==> (VALOF c RESULTIS e, s) > (n, s1)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

124 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

125 
monos exec_mono 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

126 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

127 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

128 
inductive_cases 
18260  129 
[elim!]: "(N(n),sigma) > (n',s')" 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

130 
and [elim!]: "(X(x),sigma) > (n,s')" 
18260  131 
and [elim!]: "(Op f a1 a2,sigma) > (n,s')" 
132 
and [elim!]: "(VALOF c RESULTIS e, s) > (n, s1)" 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

133 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

134 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

135 
lemma var_assign_eval [intro!]: "(X x, s(x:=n)) > (n, s(x:=n))" 
44965  136 
by (rule fun_upd_same [THEN subst]) fast 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

137 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

138 

23746  139 
text{* Make the induction rule look nicer  though @{text eta_contract} makes the new 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

140 
version look worse than it is...*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

141 

44965  142 
lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))" 
143 
by auto 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

144 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

145 
text{*New induction rule. Note the form of the VALOF induction hypothesis*} 
18260  146 
lemma eval_induct 
147 
[case_names N X Op valOf, consumes 1, induct set: eval]: 

148 
"[ (e,s) > (n,s'); 

149 
!!n s. P (N n) s n s; 

150 
!!s x. P (X x) s (s x) s; 

151 
!!e0 e1 f n0 n1 s s0 s1. 

152 
[ (e0,s) > (n0,s0); P e0 s n0 s0; 

153 
(e1,s0) > (n1,s1); P e1 s0 n1 s1 

154 
] ==> P (Op f e0 e1) s (f n0 n1) s1; 

155 
!!c e n s s0 s1. 

156 
[ (c,s) [eval Int {((e,s),(n,s')). P e s n s'}]> s0; 

157 
(c,s) [eval]> s0; 

158 
(e,s0) > (n,s1); P e s0 n s1 ] 

159 
==> P (VALOF c RESULTIS e) s n s1 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

160 
] ==> P e s n s'" 
18260  161 
apply (induct set: eval) 
162 
apply blast 

163 
apply blast 

164 
apply blast 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

165 
apply (frule Int_lower1 [THEN exec_mono, THEN subsetD]) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

166 
apply (auto simp add: split_lemma) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

167 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

168 

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

169 

23746  170 
text{*Lemma for @{text Function_eval}. The major premise is that @{text "(c,s)"} executes to @{text "s1"} 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

171 
using eval restricted to its functional part. Note that the execution 
23746  172 
@{text "(c,s) [eval]> s2"} can use unrestricted @{text eval}! The reason is that 
173 
the execution @{text "(c,s) [eval Int {...}]> s1"} assures us that execution is 

174 
functional on the argument @{text "(c,s)"}. 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

175 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

176 
lemma com_Unique: 
18260  177 
"(c,s) [eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) > nt' > (n,t)=nt'}]> s1 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

178 
==> \<forall>s2. (c,s) [eval]> s2 > s2=s1" 
18260  179 
apply (induct set: exec) 
180 
apply simp_all 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

181 
apply blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

182 
apply force 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

183 
apply blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

184 
apply blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

185 
apply blast 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

186 
apply (blast elim: exec_WHILE_case) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

187 
apply (erule_tac V = "(?c,s2) [?ev]> s3" in thin_rl) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

188 
apply clarify 
18260  189 
apply (erule exec_WHILE_case, blast+) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

190 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

191 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

192 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

193 
text{*Expression evaluation is functional, or deterministic*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

194 
theorem single_valued_eval: "single_valued eval" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

195 
apply (unfold single_valued_def) 
18260  196 
apply (intro allI, rule impI) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

197 
apply (simp (no_asm_simp) only: split_tupled_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

198 
apply (erule eval_induct) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

199 
apply (drule_tac [4] com_Unique) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

200 
apply (simp_all (no_asm_use)) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

201 
apply blast+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

202 
done 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

203 

18260  204 
lemma eval_N_E [dest!]: "(N n, s) > (v, s') ==> (v = n & s' = s)" 
205 
by (induct e == "N n" s v s' set: eval) simp_all 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

206 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

207 
text{*This theorem says that "WHILE TRUE DO c" cannot terminate*} 
18260  208 
lemma while_true_E: 
209 
"(c', s) [eval]> t ==> c' = WHILE (N 0) DO c ==> False" 

210 
by (induct set: exec) auto 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

211 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

212 

18260  213 
subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

214 
WHILE e DO c *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

215 

18260  216 
lemma while_if1: 
217 
"(c',s) [eval]> t 

218 
==> c' = WHILE e DO c ==> 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

219 
(IF e THEN c;;c' ELSE SKIP, s) [eval]> t" 
18260  220 
by (induct set: exec) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

221 

18260  222 
lemma while_if2: 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

223 
"(c',s) [eval]> t 
18260  224 
==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==> 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

225 
(WHILE e DO c, s) [eval]> t" 
18260  226 
by (induct set: exec) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

227 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

228 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

229 
theorem while_if: 
18260  230 
"((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) [eval]> t) = 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

231 
((WHILE e DO c, s) [eval]> t)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

232 
by (blast intro: while_if1 while_if2) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

233 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

234 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

235 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

236 
subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

237 
and IF e THEN (c1;;c) ELSE (c2;;c) *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

238 

18260  239 
lemma if_semi1: 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

240 
"(c',s) [eval]> t 
18260  241 
==> c' = (IF e THEN c1 ELSE c2);;c ==> 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

242 
(IF e THEN (c1;;c) ELSE (c2;;c), s) [eval]> t" 
18260  243 
by (induct set: exec) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

244 

18260  245 
lemma if_semi2: 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

246 
"(c',s) [eval]> t 
18260  247 
==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==> 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

248 
((IF e THEN c1 ELSE c2);;c, s) [eval]> t" 
18260  249 
by (induct set: exec) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

250 

18260  251 
theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) [eval]> t) = 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

252 
((IF e THEN (c1;;c) ELSE (c2;;c), s) [eval]> t)" 
18260  253 
by (blast intro: if_semi1 if_semi2) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

254 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

255 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

256 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

257 
subsection{* Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

258 
and VALOF c1;;c2 RESULTIS e 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

259 
*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

260 

18260  261 
lemma valof_valof1: 
262 
"(e',s) > (v,s') 

263 
==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==> 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

264 
(VALOF c1;;c2 RESULTIS e, s) > (v,s')" 
18260  265 
by (induct set: eval) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

266 

18260  267 
lemma valof_valof2: 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

268 
"(e',s) > (v,s') 
18260  269 
==> e' = VALOF c1;;c2 RESULTIS e ==> 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

270 
(VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) > (v,s')" 
18260  271 
by (induct set: eval) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

272 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

273 
theorem valof_valof: 
18260  274 
"((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) > (v,s')) = 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

275 
((VALOF c1;;c2 RESULTIS e, s) > (v,s'))" 
18260  276 
by (blast intro: valof_valof1 valof_valof2) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

277 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

278 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

279 
subsection{* Equivalence of VALOF SKIP RESULTIS e and e *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

280 

18260  281 
lemma valof_skip1: 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

282 
"(e',s) > (v,s') 
18260  283 
==> e' = VALOF SKIP RESULTIS e ==> 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

284 
(e, s) > (v,s')" 
18260  285 
by (induct set: eval) auto 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

286 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

287 
lemma valof_skip2: 
18260  288 
"(e,s) > (v,s') ==> (VALOF SKIP RESULTIS e, s) > (v,s')" 
289 
by blast 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

290 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

291 
theorem valof_skip: 
18260  292 
"((VALOF SKIP RESULTIS e, s) > (v,s')) = ((e, s) > (v,s'))" 
293 
by (blast intro: valof_skip1 valof_skip2) 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

294 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

295 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

296 
subsection{* Equivalence of VALOF x:=e RESULTIS x and e *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

297 

18260  298 
lemma valof_assign1: 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

299 
"(e',s) > (v,s'') 
18260  300 
==> e' = VALOF x:=e RESULTIS X x ==> 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

301 
(\<exists>s'. (e, s) > (v,s') & (s'' = s'(x:=v)))" 
18260  302 
by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto) 
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

303 

d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

304 
lemma valof_assign2: 
18260  305 
"(e,s) > (v,s') ==> (VALOF x:=e RESULTIS X x, s) > (v,s'(x:=v))" 
306 
by blast 

13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

307 

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

308 
end 