src/HOL/IMP/Def_Ass_Sound_Big.thy
author nipkow
Sat, 28 Apr 2012 07:38:22 +0200
changeset 47818 151d137f1095
parent 45015 fdac1e9880eb
permissions -rw-r--r--
renamed Semi to Seq

(* Author: Tobias Nipkow *)

theory Def_Ass_Sound_Big imports Def_Ass Def_Ass_Big
begin


subsection "Soundness wrt Big Steps"

text{* Note the special form of the induction because one of the arguments
of the inductive predicate is not a variable but the term @{term"Some s"}: *}

theorem Sound:
  "\<lbrakk> (c,Some s) \<Rightarrow> s';  D A c A';  A \<subseteq> dom s \<rbrakk>
  \<Longrightarrow> \<exists> t. s' = Some t \<and> A' \<subseteq> dom t"
proof (induction c "Some s" s' arbitrary: s A A' rule:big_step_induct)
  case AssignNone thus ?case
    by auto (metis aval_Some option.simps(3) subset_trans)
next
  case Seq thus ?case by auto metis
next
  case IfTrue thus ?case by auto blast
next
  case IfFalse thus ?case by auto blast
next
  case IfNone thus ?case
    by auto (metis bval_Some option.simps(3) order_trans)
next
  case WhileNone thus ?case
    by auto (metis bval_Some option.simps(3) order_trans)
next
  case (WhileTrue b s c s' s'')
  from `D A (WHILE b DO c) A'` obtain A' where "D A c A'" by blast
  then obtain t' where "s' = Some t'" "A \<subseteq> dom t'"
    by (metis D_incr WhileTrue(3,7) subset_trans)
  from WhileTrue(5)[OF this(1) WhileTrue(6) this(2)] show ?case .
qed auto

corollary sound: "\<lbrakk>  D (dom s) c A';  (c,Some s) \<Rightarrow> s' \<rbrakk> \<Longrightarrow> s' \<noteq> None"
by (metis Sound not_Some_eq subset_refl)

end