equal
deleted
inserted
replaced
84 \ P(b); \ |
84 \ P(b); \ |
85 \ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
85 \ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
86 \ |] ==> c<=b --> P(b-c)"; |
86 \ |] ==> c<=b --> P(b-c)"; |
87 by (rtac (major RS Fin_induct) 1); |
87 by (rtac (major RS Fin_induct) 1); |
88 by (rtac (Diff_insert RS ssubst) 2); |
88 by (rtac (Diff_insert RS ssubst) 2); |
89 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[insert_subset_iff, |
89 by (ALLGOALS (asm_simp_tac |
90 Diff_subset RS Fin_subset])))); |
90 (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset])))); |
91 val Fin_empty_induct_lemma = result(); |
91 val Fin_empty_induct_lemma = result(); |
92 |
92 |
93 val prems = goal Finite.thy |
93 val prems = goal Finite.thy |
94 "[| b: Fin(A); \ |
94 "[| b: Fin(A); \ |
95 \ P(b); \ |
95 \ P(b); \ |