summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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) |