src/HOL/IMP/Def_Ass_Sound_Big.thy
author nipkow
Tue Sep 20 05:48:23 2011 +0200 (2011-09-20)
changeset 45015 fdac1e9880eb
parent 43158 686fa0a0696e
child 47818 151d137f1095
permissions -rw-r--r--
Updated IMP to use new induction method
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@43158
     3
theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big
kleing@43158
     4
begin
kleing@43158
     5
kleing@43158
     6
kleing@43158
     7
subsection "Soundness wrt Big Steps"
kleing@43158
     8
kleing@43158
     9
text{* Note the special form of the induction because one of the arguments
kleing@43158
    10
of the inductive predicate is not a variable but the term @{term"Some s"}: *}
kleing@43158
    11
kleing@43158
    12
theorem Sound:
kleing@43158
    13
  "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
kleing@43158
    14
  \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
nipkow@45015
    15
proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
kleing@43158
    16
  case AssignNone thus ?case
kleing@43158
    17
    by auto (metis aval_Some option.simps(3) subset_trans)
kleing@43158
    18
next
kleing@43158
    19
  case Semi thus ?case by auto metis
kleing@43158
    20
next
kleing@43158
    21
  case IfTrue thus ?case by auto blast
kleing@43158
    22
next
kleing@43158
    23
  case IfFalse thus ?case by auto blast
kleing@43158
    24
next
kleing@43158
    25
  case IfNone thus ?case
kleing@43158
    26
    by auto (metis bval_Some option.simps(3) order_trans)
kleing@43158
    27
next
kleing@43158
    28
  case WhileNone thus ?case
kleing@43158
    29
    by auto (metis bval_Some option.simps(3) order_trans)
kleing@43158
    30
next
kleing@43158
    31
  case (WhileTrue b s c s' s'')
kleing@43158
    32
  from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast
kleing@43158
    33
  then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"
kleing@43158
    34
    by (metis D_incr WhileTrue(3,7) subset_trans)
kleing@43158
    35
  from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
kleing@43158
    36
qed auto
kleing@43158
    37
kleing@43158
    38
corollary sound: "\<lbrakk>  D (dom s) c A';  (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"
kleing@43158
    39
by (metis Sound not_Some_eq subset_refl)
kleing@43158
    40
kleing@43158
    41
end