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

src/HOL/Bali/DefiniteAssignment.thy

changeset 32960 | 69916a850301 |

parent 24019 | 67bde7cfcf10 |

child 35416 | d8d7d1b785af |

--- a/src/HOL/Bali/DefiniteAssignment.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/HOL/Bali/DefiniteAssignment.thy Sat Oct 17 14:43:18 2009 +0200 @@ -260,11 +260,11 @@ proof (cases "the_Bool bv") case True with Cond show ?thesis using v bv - by (auto intro: hyp_CondL) + by (auto intro: hyp_CondL) next case False with Cond show ?thesis using v bv - by (auto intro: hyp_CondR) + by (auto intro: hyp_CondR) qed qed (simp_all) with const @@ -364,7 +364,7 @@ hence "?Ass b e1" by (rule hyp_e1) with emptyC bv True show ?thesis - by simp + by simp next case False with const bv @@ -372,7 +372,7 @@ hence "?Ass b e2" by (rule hyp_e2) with emptyC bv False show ?thesis - by simp + by simp qed qed (simp_all) with boolConst @@ -411,7 +411,7 @@ hence "?Ass b e1" by (rule hyp_e1) with bv True show ?thesis - by simp + by simp next case False with const bv @@ -419,7 +419,7 @@ hence "?Ass b e2" by (rule hyp_e2) with bv False show ?thesis - by simp + by simp qed qed (simp_all) with boolConst @@ -959,14 +959,14 @@ from `E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)` obtain Te where "E\<turnstile>e\<Colon>-Te" "prg E\<turnstile>Te\<preceq>? PrimT Boolean" - by cases simp + by cases simp thus ?thesis - by - (drule cast_Boolean2,simp) + by - (drule cast_Boolean2,simp) qed with Cast.hyps show ?case by simp - next + next case (Lit val) thus ?case by - (erule wt_elim_cases, cases "val", auto simp add: empty_dt_def) @@ -1000,17 +1000,17 @@ case None with boolean_e1 boolean_e2 show ?thesis - using hyp_e1 hyp_e2 - by (auto) + using hyp_e1 hyp_e2 + by (auto) next case (Some bv) show ?thesis proof (cases "the_Bool bv") - case True - with Some show ?thesis using hyp_e1 boolean_e1 by auto + case True + with Some show ?thesis using hyp_e1 boolean_e1 by auto next - case False - with Some show ?thesis using hyp_e2 boolean_e2 by auto + case False + with Some show ?thesis using hyp_e2 boolean_e2 by auto qed qed qed simp_all @@ -1085,7 +1085,7 @@ fix l' from hyp_brk have "rmlab l (brk C) l' \<subseteq> rmlab l (brk C') l'" - by (cases "l=l'") simp_all + by (cases "l=l'") simp_all } moreover note A A' ultimately show ?case @@ -1154,15 +1154,15 @@ { fix l' have "brk A l' \<subseteq> brk A' l'" proof (cases "constVal e") - case None - with A A' C' - show ?thesis - by (cases "l=l'") auto + case None + with A A' C' + show ?thesis + by (cases "l=l'") auto next - case (Some bv) - with A A' C' - show ?thesis - by (cases "the_Bool bv", cases "l=l'") auto + case (Some bv) + with A A' C' + show ?thesis + by (cases "the_Bool bv", cases "l=l'") auto qed } ultimately show ?case @@ -1381,7 +1381,7 @@ proof - from B' have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps) ultimately @@ -1391,7 +1391,7 @@ obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" proof - from B' have "(B \<union> assigns_if False e) \<subseteq> (B' \<union> assigns_if False e)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps) ultimately @@ -1415,7 +1415,7 @@ proof - from B' have "(B \<union> assigns_if True e) \<subseteq> (B' \<union> assigns_if True e)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps) ultimately @@ -1461,7 +1461,7 @@ moreover have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) (B \<union> {VName vn}) \<langle>c2\<rangle>" - by (rule Try.hyps) + by (rule Try.hyps) ultimately show ?thesis using that by iprover qed @@ -1516,7 +1516,7 @@ obtain E2' where "Env\<turnstile> B' \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" proof - from B' have "B \<union> assigns_if True e1 \<subseteq> B' \<union> assigns_if True e1" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps) ultimately show ?thesis using that by iprover @@ -1538,7 +1538,7 @@ obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" proof - from B' have "B \<union> assigns_if False e1 \<subseteq> B' \<union> assigns_if False e1" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps) ultimately show ?thesis using that by iprover @@ -1562,7 +1562,7 @@ have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule BinOp.hyps) from this B' E1' have "nrm E1 \<subseteq> nrm E1'" - by (rule da_monotone [THEN conjE]) + by (rule da_monotone [THEN conjE]) moreover have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps) ultimately show ?thesis using that by iprover @@ -1612,7 +1612,7 @@ have "Env\<turnstile> B \<guillemotright>\<langle>v\<rangle>\<guillemotright> V" by (rule Ass.hyps) from this B' V' have "nrm V \<subseteq> nrm V'" - by (rule da_monotone [THEN conjE]) + by (rule da_monotone [THEN conjE]) moreover have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps) ultimately show ?thesis using that by iprover @@ -1636,7 +1636,7 @@ proof - from B' have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps) ultimately @@ -1647,7 +1647,7 @@ proof - from B' have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps) ultimately @@ -1672,7 +1672,7 @@ proof - from B' have "(B \<union> assigns_if True c) \<subseteq> (B' \<union> assigns_if True c)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps) ultimately @@ -1683,7 +1683,7 @@ proof - from B' have "(B \<union> assigns_if False c) \<subseteq> (B' \<union> assigns_if False c)" - by blast + by blast moreover have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps) ultimately @@ -1708,7 +1708,7 @@ have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Call.hyps) from this B' E' have "nrm E \<subseteq> nrm E'" - by (rule da_monotone [THEN conjE]) + by (rule da_monotone [THEN conjE]) moreover have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps) ultimately show ?thesis using that by iprover @@ -1728,10 +1728,10 @@ moreover note B' moreover from B' obtain C' where da_c: "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" - by (rule Body.hyps [elim_format]) blast + by (rule Body.hyps [elim_format]) blast ultimately have "nrm C \<subseteq> nrm C'" - by (rule da_monotone [THEN conjE]) + by (rule da_monotone [THEN conjE]) with da_c that show ?thesis by iprover qed moreover @@ -1762,7 +1762,7 @@ have "Env\<turnstile> B \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" by (rule AVar.hyps) from this B' E1' have "nrm E1 \<subseteq> nrm E1'" - by (rule da_monotone [THEN conjE]) + by (rule da_monotone [THEN conjE]) moreover have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps) ultimately show ?thesis using that by iprover @@ -1788,7 +1788,7 @@ have "Env\<turnstile> B \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" by (rule Cons.hyps) from this B' E' have "nrm E \<subseteq> nrm E'" - by (rule da_monotone [THEN conjE]) + by (rule da_monotone [THEN conjE]) moreover have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps) ultimately show ?thesis using that by iprover