author  paulson 
Wed, 07 Apr 2004 14:25:48 +0200  
changeset 14527  bc9e5587d05a 
parent 13075  d3e1d554cd6d 
child 16417  9bc16273c2d4 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/Induct/Com 
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: Commands 
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 

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

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

11 
theory Com = Main: 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 

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

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

14 

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

15 
types state = "loc => nat" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

16 
n2n2n = "nat => nat => nat" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11701
diff
changeset

18 
arities loc :: type 
3120
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 
datatype 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

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

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

23 
 Op n2n2n exp exp 
10759  24 
 valOf com exp ("VALOF _ RESULTIS _" 60) 
25 
and 

26 
com = SKIP 

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

27 
 ":=" loc exp (infixl 60) 
10759  28 
 Semi com com ("_;;_" [60, 60] 60) 
29 
 Cond exp com com ("IF _ THEN _ ELSE _" 60) 

30 
 While exp com ("WHILE _ DO _" 60) 

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

31 

14527  32 

33 
subsection {* Commands *} 

34 

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

35 
text{* Execution of commands *} 
10759  36 
consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

37 
"@exec" :: "((exp*state) * (nat*state)) set => 
10759  38 
[com*state,state] => bool" ("_/ [_]> _" [50,0,50] 50) 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

39 

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

40 
translations "csig [eval]> s" == "(csig,s) \<in> exec eval" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

41 

4264  42 
syntax eval' :: "[exp*state,nat*state] => 
43 
((exp*state) * (nat*state)) set => bool" 

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

44 
("_/ [_]> _" [50,0,50] 50) 
4264  45 

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

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

47 
"esig [eval]> ns" => "(esig,ns) \<in> eval" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

48 

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

49 
text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

50 
inductive "exec eval" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

52 
Skip: "(SKIP,s) [eval]> s" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

53 

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

54 
Assign: "(e,s) [eval]> (v,s') ==> (x := e, s) [eval]> s'(x:=v)" 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

55 

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

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

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

58 

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

59 
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

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

61 

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

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

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

64 

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

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

66 
==> (WHILE e DO c, s) [eval]> s1" 
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 
WhileTrue: "[ (e,s) [eval]> (0,s1); 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

69 
(c,s1) [eval]> s2; (WHILE e DO c, s2) [eval]> s3 ] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

71 

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

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

73 

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

74 

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

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

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

77 
and [elim!]: "(x:=a,s) [eval]> t" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

78 
and [elim!]: "(c1;;c2, s) [eval]> t" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

79 
and [elim!]: "(IF e THEN c1 ELSE c2, s) [eval]> t" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

81 

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

82 

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

83 
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

84 
lemma exec_mono: "A<=B ==> exec(A) <= exec(B)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

85 
apply (unfold exec.defs ) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

87 
apply (assumption  rule basic_monos)+ 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

89 

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

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

91 
Unify.trace_bound := 30; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

92 
Unify.search_bound := 60; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

94 

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) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

98 
apply (intro allI) 
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 *} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

108 
consts eval :: "((exp*state) * (nat*state)) set" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

109 
">" :: "[exp*state,nat*state] => bool" (infixl 50) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

110 

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

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

112 
"esig > (n,s)" <= "(esig,n,s) \<in> eval" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

113 
"esig > ns" == "(esig,ns ) \<in> eval" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

114 

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

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

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

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

118 

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

119 
X [intro!]: "(X(x),s) > (s(x),s)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

120 

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

121 
Op [intro]: "[ (e0,s) > (n0,s0); (e1,s0) > (n1,s1) ] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

123 

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

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

125 
==> (VALOF c RESULTIS e, s) > (n, s1)" 
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 
monos exec_mono 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

128 

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

129 

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

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

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

132 
and [elim!]: "(X(x),sigma) > (n,s')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

133 
and [elim!]: "(Op f a1 a2,sigma) > (n,s')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

134 
and [elim!]: "(VALOF c RESULTIS e, s) > (n, s1)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

135 

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

136 

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

137 
lemma var_assign_eval [intro!]: "(X x, s(x:=n)) > (n, s(x:=n))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

138 
by (rule fun_upd_same [THEN subst], fast) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

139 

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

140 

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

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

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

143 

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

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

145 
"{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

147 

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

148 
text{*New induction rule. Note the form of the VALOF induction hypothesis*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

150 
"[ (e,s) > (n,s'); 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

151 
!!n s. P (N n) s n s; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

152 
!!s x. P (X x) s (s x) s; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

153 
!!e0 e1 f n0 n1 s s0 s1. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

154 
[ (e0,s) > (n0,s0); P e0 s n0 s0; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

155 
(e1,s0) > (n1,s1); P e1 s0 n1 s1 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

157 
!!c e n s s0 s1. 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

158 
[ (c,s) [eval Int {((e,s),(n,s')). P e s n s'}]> s0; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

159 
(c,s) [eval]> s0; 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

160 
(e,s0) > (n,s1); P e s0 n s1 ] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

162 
] ==> P e s n s'" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

163 
apply (erule eval.induct, blast) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

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

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

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

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

169 

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

170 

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

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

172 
using eval restricted to its functional part. Note that the execution 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

173 
(c,s) [eval]> s2 can use unrestricted eval! The reason is that 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

174 
the execution (c,s) [eval Int {...}]> s1 assures us that execution is 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

175 
functional on the argument (c,s). 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

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

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

179 
==> \<forall>s2. (c,s) [eval]> s2 > s2=s1" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

180 
apply (erule exec.induct, simp_all) 
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 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

189 
apply (erule exec_WHILE_case, blast+) 
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) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

196 
apply (intro allI, rule impI) 
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 

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

204 

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

205 
lemma eval_N_E_lemma: "(e,s) > (v,s') ==> (e = N n) > (v=n & s'=s)" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

206 
by (erule eval_induct, simp_all) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

207 

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

208 
lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl] 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

209 

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

210 

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

211 
text{*This theorem says that "WHILE TRUE DO c" cannot terminate*} 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

212 
lemma while_true_E [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

213 
"(c', s) [eval]> t ==> (c' = WHILE (N 0) DO c) > False" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

214 
by (erule exec.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

215 

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

216 

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

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

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

219 

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

220 
lemma while_if1 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

222 
==> (c' = WHILE e DO c) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

224 
by (erule exec.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

225 

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

226 
lemma while_if2 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

228 
==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

230 
by (erule exec.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

231 

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

232 

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

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

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

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

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

237 

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

238 

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

239 

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

240 
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

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

242 

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

243 
lemma if_semi1 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

245 
==> (c' = (IF e THEN c1 ELSE c2);;c) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

247 
by (erule exec.induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

248 

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

249 
lemma if_semi2 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

251 
==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

253 
by (erule exec.induct, auto) 
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 
theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) [eval]> t) = 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

257 
by (blast intro: if_semi1 if_semi2) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

258 

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 

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

261 
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

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

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

264 

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

265 
lemma valof_valof1 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

266 
"(e',s) > (v,s') 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

267 
==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

269 
by (erule eval_induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

270 

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

271 

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

272 
lemma valof_valof2 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

273 
"(e',s) > (v,s') 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

274 
==> (e' = VALOF c1;;c2 RESULTIS e) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

276 
by (erule eval_induct, auto) 
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 
theorem valof_valof: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

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

281 
by (blast intro: valof_valof1 valof_valof2) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

282 

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

283 

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

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

285 

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

286 
lemma valof_skip1 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

287 
"(e',s) > (v,s') 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

288 
==> (e' = VALOF SKIP RESULTIS e) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

289 
(e, s) > (v,s')" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

290 
by (erule eval_induct, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

291 

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

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

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

294 
by blast 
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 
theorem valof_skip: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

298 
by (blast intro: valof_skip1 valof_skip2) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

299 

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

300 

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

301 
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

302 

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

303 
lemma valof_assign1 [rule_format]: 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

304 
"(e',s) > (v,s'') 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

305 
==> (e' = VALOF x:=e RESULTIS X x) > 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

306 
(\<exists>s'. (e, s) > (v,s') & (s'' = s'(x:=v)))" 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

308 
apply (simp_all del: fun_upd_apply, clarify, auto) 
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
12338
diff
changeset

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

310 

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

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

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

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

314 

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

315 

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

316 
end 