8 inductive |
8 inductive |
9 small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
9 small_step :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>" 55) |
10 where |
10 where |
11 Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" | |
11 Assign: "(x ::= a, s) \<rightarrow> (SKIP, s(x := aval a s))" | |
12 |
12 |
13 Semi1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
13 Seq1: "(SKIP;c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
14 Semi2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" | |
14 Seq2: "(c\<^isub>1,s) \<rightarrow> (c\<^isub>1',s') \<Longrightarrow> (c\<^isub>1;c\<^isub>2,s) \<rightarrow> (c\<^isub>1';c\<^isub>2,s')" | |
15 |
15 |
16 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
16 IfTrue: "bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>1,s)" | |
17 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
17 IfFalse: "\<not>bval b s \<Longrightarrow> (IF b THEN c\<^isub>1 ELSE c\<^isub>2,s) \<rightarrow> (c\<^isub>2,s)" | |
18 |
18 |
19 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
19 While: "(WHILE b DO c,s) \<rightarrow> (IF b THEN c; WHILE b DO c ELSE SKIP,s)" |
52 |
52 |
53 inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct" |
53 inductive_cases SkipE[elim!]: "(SKIP,s) \<rightarrow> ct" |
54 thm SkipE |
54 thm SkipE |
55 inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct" |
55 inductive_cases AssignE[elim!]: "(x::=a,s) \<rightarrow> ct" |
56 thm AssignE |
56 thm AssignE |
57 inductive_cases SemiE[elim]: "(c1;c2,s) \<rightarrow> ct" |
57 inductive_cases SeqE[elim]: "(c1;c2,s) \<rightarrow> ct" |
58 thm SemiE |
58 thm SeqE |
59 inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct" |
59 inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<rightarrow> ct" |
60 inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct" |
60 inductive_cases WhileE[elim]: "(WHILE b DO c, s) \<rightarrow> ct" |
61 |
61 |
62 |
62 |
63 text{* A simple property: *} |
63 text{* A simple property: *} |
68 done |
68 done |
69 |
69 |
70 |
70 |
71 subsection "Equivalence with big-step semantics" |
71 subsection "Equivalence with big-step semantics" |
72 |
72 |
73 lemma star_semi2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')" |
73 lemma star_seq2: "(c1,s) \<rightarrow>* (c1',s') \<Longrightarrow> (c1;c2,s) \<rightarrow>* (c1';c2,s')" |
74 proof(induction rule: star_induct) |
74 proof(induction rule: star_induct) |
75 case refl thus ?case by simp |
75 case refl thus ?case by simp |
76 next |
76 next |
77 case step |
77 case step |
78 thus ?case by (metis Semi2 star.step) |
78 thus ?case by (metis Seq2 star.step) |
79 qed |
79 qed |
80 |
80 |
81 lemma semi_comp: |
81 lemma seq_comp: |
82 "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk> |
82 "\<lbrakk> (c1,s1) \<rightarrow>* (SKIP,s2); (c2,s2) \<rightarrow>* (SKIP,s3) \<rbrakk> |
83 \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)" |
83 \<Longrightarrow> (c1;c2, s1) \<rightarrow>* (SKIP,s3)" |
84 by(blast intro: star.step star_semi2 star_trans) |
84 by(blast intro: star.step star_seq2 star_trans) |
85 |
85 |
86 text{* The following proof corresponds to one on the board where one would |
86 text{* The following proof corresponds to one on the board where one would |
87 show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *} |
87 show chains of @{text "\<rightarrow>"} and @{text "\<rightarrow>*"} steps. *} |
88 |
88 |
89 lemma big_to_small: |
89 lemma big_to_small: |
93 next |
93 next |
94 fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto |
94 fix x a s show "(x ::= a,s) \<rightarrow>* (SKIP, s(x := aval a s))" by auto |
95 next |
95 next |
96 fix c1 c2 s1 s2 s3 |
96 fix c1 c2 s1 s2 s3 |
97 assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)" |
97 assume "(c1,s1) \<rightarrow>* (SKIP,s2)" and "(c2,s2) \<rightarrow>* (SKIP,s3)" |
98 thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule semi_comp) |
98 thus "(c1;c2, s1) \<rightarrow>* (SKIP,s3)" by (rule seq_comp) |
99 next |
99 next |
100 fix s::state and b c0 c1 t |
100 fix s::state and b c0 c1 t |
101 assume "bval b s" |
101 assume "bval b s" |
102 hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp |
102 hence "(IF b THEN c0 ELSE c1,s) \<rightarrow> (c0,s)" by simp |
103 moreover assume "(c0,s) \<rightarrow>* (SKIP,t)" |
103 moreover assume "(c0,s) \<rightarrow>* (SKIP,t)" |
124 assume w: "(?w,s') \<rightarrow>* (SKIP,t)" |
124 assume w: "(?w,s') \<rightarrow>* (SKIP,t)" |
125 assume c: "(c,s) \<rightarrow>* (SKIP,s')" |
125 assume c: "(c,s) \<rightarrow>* (SKIP,s')" |
126 assume b: "bval b s" |
126 assume b: "bval b s" |
127 have "(?w,s) \<rightarrow> (?if, s)" by blast |
127 have "(?w,s) \<rightarrow> (?if, s)" by blast |
128 moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b) |
128 moreover have "(?if, s) \<rightarrow> (c; ?w, s)" by (simp add: b) |
129 moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule semi_comp[OF c w]) |
129 moreover have "(c; ?w,s) \<rightarrow>* (SKIP,t)" by(rule seq_comp[OF c w]) |
130 ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps) |
130 ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,t)" by (metis star.simps) |
131 qed |
131 qed |
132 |
132 |
133 text{* Each case of the induction can be proved automatically: *} |
133 text{* Each case of the induction can be proved automatically: *} |
134 lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)" |
134 lemma "cs \<Rightarrow> t \<Longrightarrow> cs \<rightarrow>* (SKIP,t)" |
135 proof (induction rule: big_step.induct) |
135 proof (induction rule: big_step.induct) |
136 case Skip show ?case by blast |
136 case Skip show ?case by blast |
137 next |
137 next |
138 case Assign show ?case by blast |
138 case Assign show ?case by blast |
139 next |
139 next |
140 case Semi thus ?case by (blast intro: semi_comp) |
140 case Seq thus ?case by (blast intro: seq_comp) |
141 next |
141 next |
142 case IfTrue thus ?case by (blast intro: star.step) |
142 case IfTrue thus ?case by (blast intro: star.step) |
143 next |
143 next |
144 case IfFalse thus ?case by (blast intro: star.step) |
144 case IfFalse thus ?case by (blast intro: star.step) |
145 next |
145 next |
146 case WhileFalse thus ?case |
146 case WhileFalse thus ?case |
147 by (metis star.step star_step1 small_step.IfFalse small_step.While) |
147 by (metis star.step star_step1 small_step.IfFalse small_step.While) |
148 next |
148 next |
149 case WhileTrue |
149 case WhileTrue |
150 thus ?case |
150 thus ?case |
151 by(metis While semi_comp small_step.IfTrue star.step[of small_step]) |
151 by(metis While seq_comp small_step.IfTrue star.step[of small_step]) |
152 qed |
152 qed |
153 |
153 |
154 lemma small1_big_continue: |
154 lemma small1_big_continue: |
155 "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" |
155 "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" |
156 apply (induction arbitrary: t rule: small_step.induct) |
156 apply (induction arbitrary: t rule: small_step.induct) |