--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 27 15:08:31 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Mar 28 21:05:02 2015 +0100
@@ -176,7 +176,7 @@
val tacs1 = [
quant_tac ctxt 1,
simp_tac (put_simpset HOL_ss ctxt) 1,
- Induct_Tacs.induct_tac ctxt [[SOME "n"]] 1,
+ Induct_Tacs.induct_tac ctxt [[SOME "n"]] NONE 1,
simp_tac (put_simpset take_ss ctxt addsimps prems) 1,
TRY (safe_tac (put_claset HOL_cs ctxt))]
fun con_tac _ =
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Fri Mar 27 15:08:31 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Mar 28 21:05:02 2015 +0100
@@ -244,7 +244,7 @@
THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
-- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
(asm_full_simp_tac @{context})) 7*})
apply (tactic "forward_hyp_tac @{context}")
--- a/src/HOL/Nominal/nominal_atoms.ML Fri Mar 27 15:08:31 2015 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Mar 28 21:05:02 2015 +0100
@@ -131,7 +131,7 @@
(HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
val proof2 = fn {prems, context = ctxt} =>
- Induct_Tacs.case_tac ctxt "y" [] 1 THEN
+ Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN
asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
rtac @{thm exI} 1 THEN
rtac @{thm refl} 1
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Fri Mar 27 15:08:31 2015 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Mar 28 21:05:02 2015 +0100
@@ -798,7 +798,7 @@
fun split_idle_tac ctxt =
SELECT_GOAL
(TRY (rtac @{thm actionI} 1) THEN
- Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] 1 THEN
+ Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
rewrite_goals_tac ctxt @{thms action_rews} THEN
forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
asm_full_simp_tac ctxt 1);
--- a/src/Pure/Tools/rule_insts.ML Fri Mar 27 15:08:31 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sat Mar 28 21:05:02 2015 +0100
@@ -13,7 +13,9 @@
(binding * string option * mixfix) list -> thm -> thm
val read_instantiate: Proof.context ->
((indexname * Position.T) * string) list -> string list -> thm -> thm
+ val read_term: string -> Proof.context -> term * Proof.context
val schematic: bool Config.T
+ val goal_context: term -> Proof.context -> (string * typ) list * Proof.context
val res_inst_tac: Proof.context ->
((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
int -> tactic
@@ -69,6 +71,18 @@
else error_var "Bad sort for instantiation of type variable: " (xi, pos)
end;
+fun make_instT f v =
+ let
+ val T = TVar v;
+ val T' = f T;
+ in if T = T' then NONE else SOME (v, T') end;
+
+fun make_inst f v =
+ let
+ val t = Var v;
+ val t' = f t;
+ in if t aconv t' then NONE else SOME (v, t') end;
+
fun read_terms ss Ts ctxt =
let
fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
@@ -82,36 +96,32 @@
val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
in ((ts', tyenv'), ctxt') end;
-fun make_instT f v =
- let
- val T = TVar v;
- val T' = f T;
- in if T = T' then NONE else SOME (v, T') end;
+in
-fun make_inst f v =
+fun read_term s ctxt =
let
- val t = Var v;
- val t' = f t;
- in if t aconv t' then NONE else SOME (v, t') end;
-
-in
+ val (t, ctxt') = Variable.fix_dummy_patterns (Syntax.parse_term ctxt s) ctxt;
+ val t' = Syntax.check_term ctxt' t;
+ in (t', ctxt') end;
fun read_insts thm mixed_insts ctxt =
let
val (type_insts, term_insts) =
List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
+ (*thm context*)
+ val ctxt1 = Variable.declare_thm thm ctxt;
val tvars = Thm.fold_terms Term.add_tvars thm [];
val vars = Thm.fold_terms Term.add_vars thm [];
(*explicit type instantiations*)
- val instT1 = Term_Subst.instantiateT (map (read_type ctxt tvars) type_insts);
+ val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);
val vars1 = map (apsnd instT1) vars;
(*term instantiations*)
val (xs, ss) = split_list term_insts;
val Ts = map (the_type vars1) xs;
- val ((ts, inferred), ctxt') = read_terms ss Ts ctxt;
+ val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
(*implicit type instantiations*)
val instT2 = Term_Subst.instantiateT inferred;
@@ -122,7 +132,7 @@
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
val inst_vars = map_filter (make_inst inst2) vars2;
- in ((inst_tvars, inst_vars), ctxt') end;
+ in ((inst_tvars, inst_vars), ctxt2) end;
end;
@@ -132,9 +142,7 @@
fun where_rule ctxt mixed_insts fixes thm =
let
- val ctxt' = ctxt
- |> Variable.declare_thm thm
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+ val ctxt' = ctxt |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
val ((inst_tvars, inst_vars), ctxt'') = read_insts thm mixed_insts ctxt';
in
thm
@@ -199,27 +207,28 @@
(** tactics **)
+(* goal context *)
+
val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
+fun goal_context goal ctxt =
+ let
+ val ((_, params), ctxt') = ctxt
+ |> Variable.declare_constraints goal
+ |> Variable.improper_fixes
+ |> Variable.focus_params goal
+ ||> Variable.restore_proper_fixes ctxt
+ ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
+ in (params, ctxt') end;
+
+
(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
let
- (* goal parameters *)
+ (* goal context *)
- val goal = Thm.term_of cgoal;
- val params =
- Logic.strip_params goal
- (*as they are printed: bound variables with the same name are renamed*)
- |> Term.rename_wrt_term goal
- |> rev;
- val (param_names, param_ctxt) = ctxt
- |> Variable.declare_thm thm
- |> Thm.fold_terms Variable.declare_constraints st
- |> Variable.improper_fixes
- |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params)
- ||> Variable.restore_proper_fixes ctxt
- ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic;
+ val (params, param_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
val paramTs = map #2 params;
@@ -240,20 +249,17 @@
(* lift and instantiate rule *)
val inc = Thm.maxidx_of st + 1;
- fun lift_var ((a, j), T) =
- Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
- fun lift_term t =
- fold_rev Term.absfree (param_names ~~ paramTs)
- (Logic.incr_indexes (fixed, paramTs, inc) t);
+ val lift_type = Logic.incr_tvar inc;
+ fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
+ fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
val inst_tvars' = inst_tvars
- |> map (apply2 (Thm.ctyp_of inst_ctxt o Logic.incr_tvar inc) o apfst TVar);
+ |> map (apply2 (Thm.ctyp_of inst_ctxt o lift_type) o apfst TVar);
val inst_vars' = inst_vars
|> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
- val thm' =
- Drule.instantiate_normalize (inst_tvars', inst_vars')
- (Thm.lift_rule cgoal thm)
+ val thm' = Thm.lift_rule cgoal thm
+ |> Drule.instantiate_normalize (inst_tvars', inst_vars')
|> singleton (Variable.export inst_ctxt param_ctxt);
in
compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
--- a/src/Pure/variable.ML Fri Mar 27 15:08:31 2015 +0100
+++ b/src/Pure/variable.ML Sat Mar 28 21:05:02 2015 +0100
@@ -73,6 +73,7 @@
(((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
+ val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context
val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context
val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
--- a/src/Tools/induct_tacs.ML Fri Mar 27 15:08:31 2015 +0100
+++ b/src/Tools/induct_tacs.ML Sat Mar 28 21:05:02 2015 +0100
@@ -7,11 +7,9 @@
signature INDUCT_TACS =
sig
val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
- int -> tactic
- val case_rule_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
- thm -> int -> tactic
- val induct_tac: Proof.context -> string option list list -> int -> tactic
- val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
+ thm option -> int -> tactic
+ val induct_tac: Proof.context -> string option list list ->
+ thm list option -> int -> tactic
end
structure Induct_Tacs: INDUCT_TACS =
@@ -28,35 +26,29 @@
quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
in (u, U) end;
-fun gen_case_tac ctxt s fixes opt_rule i st =
+fun case_tac ctxt s fixes opt_rule = SUBGOAL (fn (goal, i) =>
let
val rule =
(case opt_rule of
SOME rule => rule
| NONE =>
let
- val ctxt' = ctxt
- |> Variable.focus_subgoal i st |> #2
- |> Config.get ctxt Rule_Insts.schematic ?
- Proof_Context.set_mode Proof_Context.mode_schematic
- |> Context_Position.set_visible false;
- val t = Syntax.read_term ctxt' s;
+ val (t, ctxt') = ctxt
+ |> Rule_Insts.goal_context goal |> #2
+ |> Context_Position.set_visible false
+ |> Rule_Insts.read_term s;
+ val pos = Syntax.read_input_pos s;
in
- (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, Syntax.read_input_pos s))) of
+ (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, pos))) of
rule :: _ => rule
| [] => @{thm case_split})
end);
val _ = Method.trace ctxt [rule];
-
- val xi =
- (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
- Var (xi, _) :: _ => xi
- | _ => raise THM ("Malformed cases rule", 0, [rule]));
- in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i st end
- handle THM _ => Seq.empty;
-
-fun case_tac ctxt s xs = gen_case_tac ctxt s xs NONE;
-fun case_rule_tac ctxt s xs rule = gen_case_tac ctxt s xs (SOME rule);
+ in
+ (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) handle THM _ => [] of
+ Var (xi, _) :: _ => Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i
+ | _ => no_tac)
+ end);
(* induction *)
@@ -72,32 +64,34 @@
in
-fun gen_induct_tac ctxt0 varss opt_rules i st =
+fun induct_tac ctxt varss opt_rules i st =
let
- val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
- val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
+ val goal = Thm.cprem_of st i;
+ val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
+ and ((_, goal'), _) = Variable.focus_cterm goal ctxt;
+ val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
fun induct_var name =
let
- val t = Syntax.read_term ctxt name;
+ val t = Syntax.read_term goal_ctxt name;
val pos = Syntax.read_input_pos name;
val (x, _) = Term.dest_Free t handle TERM _ =>
error ("Induction argument not a variable: " ^
- quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
+ quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
val eq_x = fn Free (y, _) => x = y | _ => false;
val _ =
if Term.exists_subterm eq_x concl then ()
else
error ("No such variable in subgoal: " ^
- quote (Syntax.string_of_term ctxt t) ^ Position.here pos);
+ quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
val _ =
if (exists o Term.exists_subterm) eq_x prems then
warning ("Induction variable occurs also among premises: " ^
- quote (Syntax.string_of_term ctxt t) ^ Position.here pos)
+ quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos)
else ();
- in #1 (check_type ctxt (t, pos)) end;
+ in #1 (check_type goal_ctxt (t, pos)) end;
- val argss = map (map (Option.map induct_var)) varss;
+ val argss = (map o map o Option.map) induct_var varss;
val rule =
(case opt_rules of
SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
@@ -117,9 +111,6 @@
end;
-fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
-fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
-
(* method syntax *)
@@ -139,14 +130,13 @@
Theory.setup
(Method.setup @{binding case_tac}
(Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
- (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s xs r)))
+ (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
"unstructured case analysis on types" #>
Method.setup @{binding induct_tac}
(Args.goal_spec -- varss -- opt_rules >>
- (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+ (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt vs rs)))
"unstructured induction on types");
end;
end;
-