equal
deleted
inserted
replaced
8 |
8 |
9 (* ------------------------------------------------------------------------ *) |
9 (* ------------------------------------------------------------------------ *) |
10 (* Exhaustion and Elimination for type one *) |
10 (* Exhaustion and Elimination for type one *) |
11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |
12 |
12 |
13 val prems = goalw thy [ONE_def] "t=UU | t = ONE"; |
13 Goalw [ONE_def] "t=UU | t = ONE"; |
14 by (lift.induct_tac "t" 1); |
14 by (lift.induct_tac "t" 1); |
15 by (Simp_tac 1); |
15 by (Simp_tac 1); |
16 by (Simp_tac 1); |
16 by (Simp_tac 1); |
17 qed "Exh_one"; |
17 qed "Exh_one"; |
18 |
18 |
19 val prems = goal thy |
19 val prems = Goal "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"; |
20 "[| p=UU ==> Q; p = ONE ==>Q|] ==>Q"; |
|
21 by (rtac (Exh_one RS disjE) 1); |
20 by (rtac (Exh_one RS disjE) 1); |
22 by (eresolve_tac prems 1); |
21 by (eresolve_tac prems 1); |
23 by (eresolve_tac prems 1); |
22 by (eresolve_tac prems 1); |
24 qed "oneE"; |
23 qed "oneE"; |
25 |
24 |