src/Tools/induct.ML
changeset 27323 385c0ce33173
parent 27140 327a73f02d5f
child 27370 8e8f96dfaf63
equal deleted inserted replaced
27322:a12978a1126a 27323:385c0ce33173
    60   val rulify_tac: int -> tactic
    60   val rulify_tac: int -> tactic
    61   val internalize: int -> thm -> thm
    61   val internalize: int -> thm -> thm
    62   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    62   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
    63   val cases_tac: Proof.context -> term option list list -> thm option ->
    63   val cases_tac: Proof.context -> term option list list -> thm option ->
    64     thm list -> int -> cases_tactic
    64     thm list -> int -> cases_tactic
       
    65   val get_inductT: Proof.context -> term option list list -> thm list list
    65   val induct_tac: Proof.context -> (string option * term) option list list ->
    66   val induct_tac: Proof.context -> (string option * term) option list list ->
    66     (string * typ) list list -> term option list -> thm list option ->
    67     (string * typ) list list -> term option list -> thm list option ->
    67     thm list -> int -> cases_tactic
    68     thm list -> int -> cases_tactic
    68   val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    69   val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    69     thm list -> int -> cases_tactic
    70     thm list -> int -> cases_tactic
   565     `A x` induct ...     - predicate/set induction
   566     `A x` induct ...     - predicate/set induction
   566           induct x       - type induction
   567           induct x       - type induction
   567     ...   induct ... r   - explicit rule
   568     ...   induct ... r   - explicit rule
   568 *)
   569 *)
   569 
   570 
   570 local
       
   571 
       
   572 fun get_inductT ctxt insts =
   571 fun get_inductT ctxt insts =
   573   fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
   572   fold_rev multiply (insts |> map
   574     |> map (find_inductT ctxt o Term.fastype_of)) [[]]
   573       ((fn [] => NONE | ts => List.last ts) #>
       
   574         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
       
   575         find_inductT ctxt)) [[]]
   575   |> filter_out (forall PureThy.is_internal);
   576   |> filter_out (forall PureThy.is_internal);
   576 
   577 
   577 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   578 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   578   | get_inductP _ _ = [];
   579   | get_inductP _ _ = [];
   579 
       
   580 in
       
   581 
   580 
   582 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
   581 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
   583   let
   582   let
   584     val thy = ProofContext.theory_of ctxt;
   583     val thy = ProofContext.theory_of ctxt;
   585     val cert = Thm.cterm_of thy;
   584     val cert = Thm.cterm_of thy;
   627                 (Tactic.rtac rule' i THEN
   626                 (Tactic.rtac rule' i THEN
   628                   PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
   627                   PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))
   629     THEN_ALL_NEW_CASES rulify_tac
   628     THEN_ALL_NEW_CASES rulify_tac
   630   end;
   629   end;
   631 
   630 
   632 end;
       
   633 
       
   634 
   631 
   635 
   632 
   636 (** coinduct method **)
   633 (** coinduct method **)
   637 
   634 
   638 (*
   635 (*