equal
deleted
inserted
replaced
319 adm_not_eq_tr adm_conj adm_disj adm_imp adm_all |
319 adm_not_eq_tr adm_conj adm_disj adm_imp adm_all |
320 |
320 |
321 method_setup induct = {* |
321 method_setup induct = {* |
322 Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt => |
322 Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt => |
323 SIMPLE_METHOD' (fn i => |
323 SIMPLE_METHOD' (fn i => |
324 res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN |
324 Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN |
325 REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) |
325 REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) |
326 *} |
326 *} |
327 |
327 |
328 lemma least_FIX: "f(p) = p \<Longrightarrow> FIX(f) << p" |
328 lemma least_FIX: "f(p) = p \<Longrightarrow> FIX(f) << p" |
329 apply (induct f) |
329 apply (induct f) |
378 apply (rule 3) |
378 apply (rule 3) |
379 done |
379 done |
380 |
380 |
381 ML {* |
381 ML {* |
382 fun induct2_tac ctxt (f, g) i = |
382 fun induct2_tac ctxt (f, g) i = |
383 res_inst_tac ctxt |
383 Rule_Insts.res_inst_tac ctxt |
384 [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN |
384 [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN |
385 REPEAT(resolve_tac ctxt @{thms adm_lemmas} i) |
385 REPEAT(resolve_tac ctxt @{thms adm_lemmas} i) |
386 *} |
386 *} |
387 |
387 |
388 end |
388 end |