src/HOL/IMP/Def_Ass_Sound_Big.thy
changeset 45015 fdac1e9880eb
parent 43158 686fa0a0696e
child 47818 151d137f1095
equal deleted inserted replaced
45014:0e847655b2d8 45015:fdac1e9880eb
    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