equal
deleted
inserted
replaced
10 of the inductive predicate is not a variable but the term @{term"Some s"}: *} |
10 of the inductive predicate is not a variable but the term @{term"Some s"}: *} |
11 |
11 |
12 theorem Sound: |
12 theorem Sound: |
13 "\<lbrakk> (c,Some s) \<Rightarrow> s'; D A c A'; A \<subseteq> dom s \<rbrakk> |
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" |
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) |
15 proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct) |
16 case AssignNone thus ?case |
16 case AssignNone thus ?case |
17 by auto (metis aval_Some option.simps(3) subset_trans) |
17 by auto (metis aval_Some option.simps(3) subset_trans) |
18 next |
18 next |
19 case Semi thus ?case by auto metis |
19 case Semi thus ?case by auto metis |
20 next |
20 next |