# HG changeset patch # User wenzelm # Date 1214227613 -7200 # Node ID 385c0ce331737ad568cda34e5f1d2797230321bb # Parent a12978a1126a469c0ea43e9cb45f4771ce4df4d1 tuned get_inductT: *all* rules for missing instantiation; exported get_inductT; diff -r a12978a1126a -r 385c0ce33173 src/Tools/induct.ML --- a/src/Tools/induct.ML Mon Jun 23 15:26:52 2008 +0200 +++ b/src/Tools/induct.ML Mon Jun 23 15:26:53 2008 +0200 @@ -62,6 +62,7 @@ val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq val cases_tac: Proof.context -> term option list list -> thm option -> thm list -> int -> cases_tactic + val get_inductT: Proof.context -> term option list list -> thm list list val induct_tac: Proof.context -> (string option * term) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> cases_tactic @@ -567,18 +568,16 @@ ... induct ... r - explicit rule *) -local - fun get_inductT ctxt insts = - fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts) - |> map (find_inductT ctxt o Term.fastype_of)) [[]] + fold_rev multiply (insts |> map + ((fn [] => NONE | ts => List.last ts) #> + (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #> + find_inductT ctxt)) [[]] |> filter_out (forall PureThy.is_internal); fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) | get_inductP _ _ = []; -in - fun induct_tac ctxt def_insts arbitrary taking opt_rule facts = let val thy = ProofContext.theory_of ctxt; @@ -629,8 +628,6 @@ THEN_ALL_NEW_CASES rulify_tac end; -end; - (** coinduct method **)