tuned signature;
authorwenzelm
Mon Dec 14 11:20:31 2015 +0100 (2015-12-14)
changeset 61844007d3b34080f
parent 61843 1803599838a6
child 61845 c5c7bc41185c
tuned signature;
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/coinduction.ML
src/Tools/induct.ML
src/Tools/induction.ML
     1.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 14 10:14:19 2015 +0100
     1.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon Dec 14 11:20:31 2015 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4         | SOME (arg, conv) =>
     1.5             let open Conv in
     1.6                if Term.is_open arg then no_tac
     1.7 -              else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
     1.8 +              else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
     1.9                  THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
    1.10                  THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
    1.11                  THEN_ALL_NEW (CONVERSION
     2.1 --- a/src/HOL/Tools/coinduction.ML	Mon Dec 14 10:14:19 2015 +0100
     2.2 +++ b/src/HOL/Tools/coinduction.ML	Mon Dec 14 11:20:31 2015 +0100
     2.3 @@ -8,7 +8,8 @@
     2.4  
     2.5  signature COINDUCTION =
     2.6  sig
     2.7 -  val coinduction_tac: term list -> thm option -> thm list -> int -> context_tactic
     2.8 +  val coinduction_context_tactic: term list -> thm option -> thm list -> int -> context_tactic
     2.9 +  val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> int -> tactic
    2.10  end;
    2.11  
    2.12  structure Coinduction : COINDUCTION =
    2.13 @@ -37,7 +38,7 @@
    2.14      (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
    2.15    end;
    2.16  
    2.17 -fun coinduction_tac raw_vars opt_raw_thm prems =
    2.18 +fun coinduction_context_tactic raw_vars opt_raw_thm prems =
    2.19    CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
    2.20      let
    2.21        val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
    2.22 @@ -117,6 +118,10 @@
    2.23          CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
    2.24      end);
    2.25  
    2.26 +fun coinduction_tac ctxt x1 x2 x3 x4 =
    2.27 +  Method.NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
    2.28 +
    2.29 +
    2.30  local
    2.31  
    2.32  val ruleN = "rule"
    2.33 @@ -153,7 +158,7 @@
    2.34      (Method.setup @{binding coinduction}
    2.35        (arbitrary -- Scan.option coinduct_rule >>
    2.36          (fn (arbitrary, opt_rule) => fn _ => fn facts =>
    2.37 -          Seq.DETERM (coinduction_tac arbitrary opt_rule facts 1)))
    2.38 +          Seq.DETERM (coinduction_context_tactic arbitrary opt_rule facts 1)))
    2.39        "coinduction on types or predicates/sets");
    2.40  
    2.41  end;
     3.1 --- a/src/Tools/induct.ML	Mon Dec 14 10:14:19 2015 +0100
     3.2 +++ b/src/Tools/induct.ML	Mon Dec 14 11:20:31 2015 +0100
     3.3 @@ -71,17 +71,32 @@
     3.4    val rotate_tac: int -> int -> int -> tactic
     3.5    val internalize: Proof.context -> int -> thm -> thm
     3.6    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
     3.7 -  val cases_tac: bool -> term option list list -> thm option -> thm list -> int -> context_tactic
     3.8 +  val cases_context_tactic: bool -> term option list list -> thm option ->
     3.9 +    thm list -> int -> context_tactic
    3.10 +  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    3.11 +    thm list -> int -> tactic
    3.12    val get_inductT: Proof.context -> term option list list -> thm list list
    3.13 -  val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
    3.14 +  val gen_induct_context_tactic: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
    3.15      bool -> (binding option * (term * bool)) option list list ->
    3.16      (string * typ) list list -> term option list -> thm list option ->
    3.17      thm list -> int -> context_tactic
    3.18 -  val induct_tac: bool -> (binding option * (term * bool)) option list list ->
    3.19 +  val gen_induct_tac: Proof.context ->
    3.20 +    ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
    3.21 +    bool -> (binding option * (term * bool)) option list list ->
    3.22 +    (string * typ) list list -> term option list -> thm list option ->
    3.23 +    thm list -> int -> tactic
    3.24 +  val induct_context_tactic: bool ->
    3.25 +    (binding option * (term * bool)) option list list ->
    3.26      (string * typ) list list -> term option list -> thm list option ->
    3.27      thm list -> int -> context_tactic
    3.28 -  val coinduct_tac: term option list -> term option list -> thm option ->
    3.29 +  val induct_tac: Proof.context -> bool ->
    3.30 +    (binding option * (term * bool)) option list list ->
    3.31 +    (string * typ) list list -> term option list -> thm list option ->
    3.32 +    thm list -> int -> tactic
    3.33 +  val coinduct_context_tactic: term option list -> term option list -> thm option ->
    3.34      thm list -> int -> context_tactic
    3.35 +  val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    3.36 +    thm list -> int -> tactic
    3.37    val gen_induct_setup: binding ->
    3.38     (bool -> (binding option * (term * bool)) option list list ->
    3.39      (string * typ) list list -> term option list -> thm list option ->
    3.40 @@ -477,7 +492,7 @@
    3.41  
    3.42  in
    3.43  
    3.44 -fun cases_tac simp insts opt_rule facts i : context_tactic =
    3.45 +fun cases_context_tactic simp insts opt_rule facts i : context_tactic =
    3.46    fn (ctxt, st) =>
    3.47      let
    3.48        fun inst_rule r =
    3.49 @@ -518,6 +533,9 @@
    3.50          end)
    3.51      end;
    3.52  
    3.53 +fun cases_tac ctxt x1 x2 x3 x4 x5 =
    3.54 +  Method.NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
    3.55 +
    3.56  end;
    3.57  
    3.58  
    3.59 @@ -739,7 +757,7 @@
    3.60  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
    3.61    | get_inductP _ _ = [];
    3.62  
    3.63 -fun gen_induct_tac mod_cases simp def_insts arbitrary taking opt_rule facts =
    3.64 +fun gen_induct_context_tactic mod_cases simp def_insts arbitrary taking opt_rule facts =
    3.65    CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) =>
    3.66      let
    3.67        val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    3.68 @@ -806,7 +824,13 @@
    3.69           THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st)
    3.70      end)
    3.71  
    3.72 -val induct_tac = gen_induct_tac I;
    3.73 +val induct_context_tactic = gen_induct_context_tactic I;
    3.74 +
    3.75 +fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 =
    3.76 +  Method.NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
    3.77 +
    3.78 +fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
    3.79 +  Method.NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
    3.80  
    3.81  
    3.82  
    3.83 @@ -831,7 +855,7 @@
    3.84  
    3.85  in
    3.86  
    3.87 -fun coinduct_tac inst taking opt_rule facts =
    3.88 +fun coinduct_context_tactic inst taking opt_rule facts =
    3.89    CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
    3.90      let
    3.91        fun inst_rule r =
    3.92 @@ -856,6 +880,9 @@
    3.93              (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st)))
    3.94      end);
    3.95  
    3.96 +fun coinduct_tac ctxt x1 x2 x3 x4 x5 =
    3.97 +  Method.NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
    3.98 +
    3.99  end;
   3.100  
   3.101  
   3.102 @@ -930,13 +957,13 @@
   3.103          (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   3.104          (fn (no_simp, (insts, opt_rule)) => fn _ =>
   3.105            CONTEXT_METHOD (fn facts =>
   3.106 -            Seq.DETERM (cases_tac (not no_simp) insts opt_rule facts 1))))
   3.107 +            Seq.DETERM (cases_context_tactic (not no_simp) insts opt_rule facts 1))))
   3.108        "case analysis on types or predicates/sets" #>
   3.109 -    gen_induct_setup @{binding induct} induct_tac #>
   3.110 +    gen_induct_setup @{binding induct} induct_context_tactic #>
   3.111       Method.local_setup @{binding coinduct}
   3.112        (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   3.113          (fn ((insts, taking), opt_rule) => fn _ => fn facts =>
   3.114 -          Seq.DETERM (coinduct_tac insts taking opt_rule facts 1)))
   3.115 +          Seq.DETERM (coinduct_context_tactic insts taking opt_rule facts 1)))
   3.116        "coinduction on types or predicates/sets");
   3.117  
   3.118  end;
     4.1 --- a/src/Tools/induction.ML	Mon Dec 14 10:14:19 2015 +0100
     4.2 +++ b/src/Tools/induction.ML	Mon Dec 14 11:20:31 2015 +0100
     4.3 @@ -7,9 +7,12 @@
     4.4  
     4.5  signature INDUCTION =
     4.6  sig
     4.7 -  val induction_tac: bool -> (binding option * (term * bool)) option list list ->
     4.8 +  val induction_context_tactic: bool -> (binding option * (term * bool)) option list list ->
     4.9      (string * typ) list list -> term option list -> thm list option ->
    4.10      thm list -> int -> context_tactic
    4.11 +  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    4.12 +    (string * typ) list list -> term option list -> thm list option ->
    4.13 +    thm list -> int -> tactic
    4.14  end
    4.15  
    4.16  structure Induction: INDUCTION =
    4.17 @@ -23,27 +26,30 @@
    4.18    | (p as Free _, _) => [p]
    4.19    | (_, ts) => maps preds_of ts);
    4.20  
    4.21 -fun name_hyps (arg as ((cases, consumes), th)) =
    4.22 -  if not (forall (null o #2 o #1) cases) then arg
    4.23 -  else
    4.24 -    let
    4.25 -      val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
    4.26 -      val prems' = drop consumes prems;
    4.27 -      val ps = preds_of concl;
    4.28 +val induction_context_tactic =
    4.29 +  Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) =>
    4.30 +    if not (forall (null o #2 o #1) cases) then arg
    4.31 +    else
    4.32 +      let
    4.33 +        val (prems, concl) = Logic.strip_horn (Thm.prop_of th);
    4.34 +        val prems' = drop consumes prems;
    4.35 +        val ps = preds_of concl;
    4.36 +  
    4.37 +        fun hname_of t =
    4.38 +          if exists_subterm (member (op aconv) ps) t
    4.39 +          then ind_hypsN else Rule_Cases.case_hypsN;
    4.40 +  
    4.41 +        val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
    4.42 +        val n = Int.min (length hnamess, length cases);
    4.43 +        val cases' =
    4.44 +          map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
    4.45 +            (take n cases ~~ take n hnamess);
    4.46 +      in ((cases', consumes), th) end);
    4.47  
    4.48 -      fun hname_of t =
    4.49 -        if exists_subterm (member (op aconv) ps) t
    4.50 -        then ind_hypsN else Rule_Cases.case_hypsN;
    4.51 +fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
    4.52 +  Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
    4.53  
    4.54 -      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems';
    4.55 -      val n = Int.min (length hnamess, length cases);
    4.56 -      val cases' =
    4.57 -        map (fn (((cn, _), concls), hns) => ((cn, hns), concls))
    4.58 -          (take n cases ~~ take n hnamess);
    4.59 -    in ((cases', consumes), th) end;
    4.60 -
    4.61 -val induction_tac = Induct.gen_induct_tac name_hyps;
    4.62 -
    4.63 -val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
    4.64 +val _ =
    4.65 +  Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic);
    4.66  
    4.67  end