src/HOL/IMP/Def_Ass_Sound_Big.thy
 changeset 43158 686fa0a0696e child 45015 fdac1e9880eb
equal inserted replaced
43157:b505be6f029a 43158:686fa0a0696e

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