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