equal
deleted
inserted
replaced
77 goal OrderArith.thy |
77 goal OrderArith.thy |
78 "!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"; |
78 "!!r s. [| wf[A](r); wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"; |
79 by (rtac wf_onI2 1); |
79 by (rtac wf_onI2 1); |
80 by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); |
80 by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); |
81 (*Proving the lemma, which is needed twice!*) |
81 (*Proving the lemma, which is needed twice!*) |
82 by (eres_inst_tac [("V", "y : A + B")] thin_rl 2); |
82 by (thin_tac "y : A + B" 2); |
83 by (rtac ballI 2); |
83 by (rtac ballI 2); |
84 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); |
84 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); |
85 by (etac (bspec RS mp) 2); |
85 by (etac (bspec RS mp) 2); |
86 by (fast_tac sum_cs 2); |
86 by (fast_tac sum_cs 2); |
87 by (best_tac (sum_cs addSEs [raddE]) 2); |
87 by (best_tac (sum_cs addSEs [raddE]) 2); |