equal
deleted
inserted
replaced
34 Goal "<c,s> -n-> t ==> <c,s> -c-> t"; |
34 Goal "<c,s> -n-> t ==> <c,s> -c-> t"; |
35 by (etac evaln.induct 1); |
35 by (etac evaln.induct 1); |
36 by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac)); |
36 by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac)); |
37 qed "evaln_evalc"; |
37 qed "evaln_evalc"; |
38 |
38 |
39 goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)"; |
|
40 by (induct_tac "m'" 1); |
|
41 by (CLASIMPSET auto_tac); |
|
42 qed_spec_mp "Suc_le_D"; |
|
43 |
|
44 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; |
39 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; |
45 by (cut_facts_tac (premises()) 1); |
40 by (cut_facts_tac (premises()) 1); |
46 by (ftac Suc_le_D 1); |
41 by (ftac Suc_le_D 1); |
47 by (Clarify_tac 1); |
42 by (Clarify_tac 1); |
48 by (eresolve_tac (premises()) 1); |
43 by (eresolve_tac (premises()) 1); |