src/HOL/IMP/Def_Ass_Sound_Big.thy
changeset 47818 151d137f1095
parent 45015 fdac1e9880eb
equal deleted inserted replaced
47817:5d2d63f4363e 47818:151d137f1095
    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 (induction 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 Seq thus ?case by auto metis
    20 next
    20 next
    21   case IfTrue thus ?case by auto blast
    21   case IfTrue thus ?case by auto blast
    22 next
    22 next
    23   case IfFalse thus ?case by auto blast
    23   case IfFalse thus ?case by auto blast
    24 next
    24 next