651 apply (safe del: disjE) |
651 apply (safe del: disjE) |
652 apply (simp_all (no_asm_use) split del: split_if_asm) |
652 apply (simp_all (no_asm_use) split del: split_if_asm) |
653 apply (safe del: disjE) |
653 apply (safe del: disjE) |
654 (* 17 subgoals *) |
654 (* 17 subgoals *) |
655 apply (tactic {* ALLGOALS (fn i => |
655 apply (tactic {* ALLGOALS (fn i => |
656 if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", |
656 if i = 11 then EVERY' |
657 RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1", |
657 [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", |
658 RuleInsts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i |
658 thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1", |
659 else RuleInsts.thin_tac @{context} "All ?P" i) *}) |
659 thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i |
|
660 else thin_tac @{context} "All ?P" i) *}) |
660 (*apply (safe del: disjE elim!: wt_elim_cases)*) |
661 (*apply (safe del: disjE elim!: wt_elim_cases)*) |
661 apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*}) |
662 apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*}) |
662 apply (simp_all (no_asm_use) split del: split_if_asm) |
663 apply (simp_all (no_asm_use) split del: split_if_asm) |
663 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) |
664 apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) |
664 apply ((blast del: equalityCE dest: sym [THEN trans])+) |
665 apply ((blast del: equalityCE dest: sym [THEN trans])+) |