equal
deleted
inserted
replaced
|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big |
|
4 begin |
|
5 |
|
6 |
|
7 subsection "Soundness wrt Big Steps" |
|
8 |
|
9 text{* Note the special form of the induction because one of the arguments |
|
10 of the inductive predicate is not a variable but the term @{term"Some s"}: *} |
|
11 |
|
12 theorem Sound: |
|
13 "\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk> |
|
14 \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t" |
|
15 proof (induct c "Some s" s' arbitrary: s A A' rule:big_step_induct) |
|
16 case AssignNone thus ?case |
|
17 by auto (metis aval_Some option.simps(3) subset_trans) |
|
18 next |
|
19 case Semi thus ?case by auto metis |
|
20 next |
|
21 case IfTrue thus ?case by auto blast |
|
22 next |
|
23 case IfFalse thus ?case by auto blast |
|
24 next |
|
25 case IfNone thus ?case |
|
26 by auto (metis bval_Some option.simps(3) order_trans) |
|
27 next |
|
28 case WhileNone thus ?case |
|
29 by auto (metis bval_Some option.simps(3) order_trans) |
|
30 next |
|
31 case (WhileTrue b s c s' s'') |
|
32 from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast |
|
33 then obtain t' where "s' = Some t'" "A \<subseteq> dom t'" |
|
34 by (metis D_incr WhileTrue(3,7) subset_trans) |
|
35 from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case . |
|
36 qed auto |
|
37 |
|
38 corollary sound: "\<lbrakk> D (dom s) c A'; (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None" |
|
39 by (metis Sound not_Some_eq subset_refl) |
|
40 |
|
41 end |