src/HOL/IMP/Live_True.thy
changeset 47818 151d137f1095
parent 46365 547d1a1dcaf6
child 48256 5fa4fc4d721a
equal deleted inserted replaced
47817:5d2d63f4363e 47818:151d137f1095
    47   case Skip then show ?case by auto
    47   case Skip then show ?case by auto
    48 next
    48 next
    49   case Assign then show ?case
    49   case Assign then show ?case
    50     by (auto simp: ball_Un)
    50     by (auto simp: ball_Un)
    51 next
    51 next
    52   case (Semi c1 s1 s2 c2 s3 X t1)
    52   case (Seq c1 s1 s2 c2 s3 X t1)
    53   from Semi.IH(1) Semi.prems obtain t2 where
    53   from Seq.IH(1) Seq.prems obtain t2 where
    54     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
    54     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
    55     by simp blast
    55     by simp blast
    56   from Semi.IH(2)[OF s2t2] obtain t3 where
    56   from Seq.IH(2)[OF s2t2] obtain t3 where
    57     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
    57     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
    58     by auto
    58     by auto
    59   show ?case using t12 t23 s3t3 by auto
    59   show ?case using t12 t23 s3t3 by auto
    60 next
    60 next
    61   case (IfTrue b s c1 s' c2)
    61   case (IfTrue b s c1 s' c2)