# HG changeset patch # User wenzelm # Date 1450088431 -3600 # Node ID 007d3b34080f9fe82832c7c219f92f376954ed2b # Parent 1803599838a66ebbfedb3f0c3e59812f9014ede5 tuned signature; diff -r 1803599838a6 -r 007d3b34080f src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Mon Dec 14 10:14:19 2015 +0100 +++ b/src/HOL/Tools/Function/partial_function.ML Mon Dec 14 11:20:31 2015 +0100 @@ -93,7 +93,7 @@ | SOME (arg, conv) => let open Conv in if Term.is_open arg then no_tac - else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE []) + else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE []) THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0) THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl} THEN_ALL_NEW (CONVERSION diff -r 1803599838a6 -r 007d3b34080f src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Mon Dec 14 10:14:19 2015 +0100 +++ b/src/HOL/Tools/coinduction.ML Mon Dec 14 11:20:31 2015 +0100 @@ -8,7 +8,8 @@ signature COINDUCTION = sig - val coinduction_tac: term list -> thm option -> thm list -> int -> context_tactic + val coinduction_context_tactic: term list -> thm option -> thm list -> int -> context_tactic + val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> int -> tactic end; structure Coinduction : COINDUCTION = @@ -37,7 +38,7 @@ (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st end; -fun coinduction_tac raw_vars opt_raw_thm prems = +fun coinduction_context_tactic raw_vars opt_raw_thm prems = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => let val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst; @@ -117,6 +118,10 @@ CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st')) end); +fun coinduction_tac ctxt x1 x2 x3 x4 = + Method.NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4); + + local val ruleN = "rule" @@ -153,7 +158,7 @@ (Method.setup @{binding coinduction} (arbitrary -- Scan.option coinduct_rule >> (fn (arbitrary, opt_rule) => fn _ => fn facts => - Seq.DETERM (coinduction_tac arbitrary opt_rule facts 1))) + Seq.DETERM (coinduction_context_tactic arbitrary opt_rule facts 1))) "coinduction on types or predicates/sets"); end; diff -r 1803599838a6 -r 007d3b34080f src/Tools/induct.ML --- a/src/Tools/induct.ML Mon Dec 14 10:14:19 2015 +0100 +++ b/src/Tools/induct.ML Mon Dec 14 11:20:31 2015 +0100 @@ -71,17 +71,32 @@ val rotate_tac: int -> int -> int -> tactic val internalize: Proof.context -> int -> thm -> thm val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq - val cases_tac: bool -> term option list list -> thm option -> thm list -> int -> context_tactic + val cases_context_tactic: bool -> term option list list -> thm option -> + thm list -> int -> context_tactic + val cases_tac: Proof.context -> bool -> term option list list -> thm option -> + thm list -> int -> tactic val get_inductT: Proof.context -> term option list list -> thm list list - val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) -> + val gen_induct_context_tactic: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) -> bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> context_tactic - val induct_tac: bool -> (binding option * (term * bool)) option list list -> + val gen_induct_tac: Proof.context -> + ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) -> + bool -> (binding option * (term * bool)) option list list -> + (string * typ) list list -> term option list -> thm list option -> + thm list -> int -> tactic + val induct_context_tactic: bool -> + (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> context_tactic - val coinduct_tac: term option list -> term option list -> thm option -> + val induct_tac: Proof.context -> bool -> + (binding option * (term * bool)) option list list -> + (string * typ) list list -> term option list -> thm list option -> + thm list -> int -> tactic + val coinduct_context_tactic: term option list -> term option list -> thm option -> thm list -> int -> context_tactic + val coinduct_tac: Proof.context -> term option list -> term option list -> thm option -> + thm list -> int -> tactic val gen_induct_setup: binding -> (bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> @@ -477,7 +492,7 @@ in -fun cases_tac simp insts opt_rule facts i : context_tactic = +fun cases_context_tactic simp insts opt_rule facts i : context_tactic = fn (ctxt, st) => let fun inst_rule r = @@ -518,6 +533,9 @@ end) end; +fun cases_tac ctxt x1 x2 x3 x4 x5 = + Method.NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5); + end; @@ -739,7 +757,7 @@ fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) | get_inductP _ _ = []; -fun gen_induct_tac mod_cases simp def_insts arbitrary taking opt_rule facts = +fun gen_induct_context_tactic mod_cases simp def_insts arbitrary taking opt_rule facts = CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) => let val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; @@ -806,7 +824,13 @@ THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st) end) -val induct_tac = gen_induct_tac I; +val induct_context_tactic = gen_induct_context_tactic I; + +fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 = + Method.NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8); + +fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 = + Method.NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7); @@ -831,7 +855,7 @@ in -fun coinduct_tac inst taking opt_rule facts = +fun coinduct_context_tactic inst taking opt_rule facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) => let fun inst_rule r = @@ -856,6 +880,9 @@ (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st))) end); +fun coinduct_tac ctxt x1 x2 x3 x4 x5 = + Method.NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5); + end; @@ -930,13 +957,13 @@ (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >> (fn (no_simp, (insts, opt_rule)) => fn _ => CONTEXT_METHOD (fn facts => - Seq.DETERM (cases_tac (not no_simp) insts opt_rule facts 1)))) + Seq.DETERM (cases_context_tactic (not no_simp) insts opt_rule facts 1)))) "case analysis on types or predicates/sets" #> - gen_induct_setup @{binding induct} induct_tac #> + gen_induct_setup @{binding induct} induct_context_tactic #> Method.local_setup @{binding coinduct} (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >> (fn ((insts, taking), opt_rule) => fn _ => fn facts => - Seq.DETERM (coinduct_tac insts taking opt_rule facts 1))) + Seq.DETERM (coinduct_context_tactic insts taking opt_rule facts 1))) "coinduction on types or predicates/sets"); end; diff -r 1803599838a6 -r 007d3b34080f src/Tools/induction.ML --- a/src/Tools/induction.ML Mon Dec 14 10:14:19 2015 +0100 +++ b/src/Tools/induction.ML Mon Dec 14 11:20:31 2015 +0100 @@ -7,9 +7,12 @@ signature INDUCTION = sig - val induction_tac: bool -> (binding option * (term * bool)) option list list -> + val induction_context_tactic: bool -> (binding option * (term * bool)) option list list -> (string * typ) list list -> term option list -> thm list option -> thm list -> int -> context_tactic + val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list -> + (string * typ) list list -> term option list -> thm list option -> + thm list -> int -> tactic end structure Induction: INDUCTION = @@ -23,27 +26,30 @@ | (p as Free _, _) => [p] | (_, ts) => maps preds_of ts); -fun name_hyps (arg as ((cases, consumes), th)) = - if not (forall (null o #2 o #1) cases) then arg - else - let - val (prems, concl) = Logic.strip_horn (Thm.prop_of th); - val prems' = drop consumes prems; - val ps = preds_of concl; +val induction_context_tactic = + Induct.gen_induct_context_tactic (fn arg as ((cases, consumes), th) => + if not (forall (null o #2 o #1) cases) then arg + else + let + val (prems, concl) = Logic.strip_horn (Thm.prop_of th); + val prems' = drop consumes prems; + val ps = preds_of concl; + + fun hname_of t = + if exists_subterm (member (op aconv) ps) t + then ind_hypsN else Rule_Cases.case_hypsN; + + val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'; + val n = Int.min (length hnamess, length cases); + val cases' = + map (fn (((cn, _), concls), hns) => ((cn, hns), concls)) + (take n cases ~~ take n hnamess); + in ((cases', consumes), th) end); - fun hname_of t = - if exists_subterm (member (op aconv) ps) t - then ind_hypsN else Rule_Cases.case_hypsN; +fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 = + Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7); - val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'; - val n = Int.min (length hnamess, length cases); - val cases' = - map (fn (((cn, _), concls), hns) => ((cn, hns), concls)) - (take n cases ~~ take n hnamess); - in ((cases', consumes), th) end; - -val induction_tac = Induct.gen_induct_tac name_hyps; - -val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac); +val _ = + Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_context_tactic); end