--- a/src/HOL/HOL.thy Mon Jun 23 15:51:37 2008 +0200
+++ b/src/HOL/HOL.thy Mon Jun 23 15:51:38 2008 +0200
@@ -25,7 +25,7 @@
"~~/src/Tools/random_word.ML"
"~~/src/Tools/atomize_elim.ML"
"~~/src/Tools/induct.ML"
- ("~~/src/HOL/Tools/induct_tacs.ML")
+ ("~~/src/Tools/induct_tacs.ML")
"~~/src/Tools/code/code_name.ML"
"~~/src/Tools/code/code_funcgr.ML"
"~~/src/Tools/code/code_thingol.ML"
@@ -1554,7 +1554,7 @@
setup Induct.setup
-use "~~/src/HOL/Tools/induct_tacs.ML"
+use "~~/src/Tools/induct_tacs.ML"
setup InductTacs.setup
--- a/src/HOL/IsaMakefile Mon Jun 23 15:51:37 2008 +0200
+++ b/src/HOL/IsaMakefile Mon Jun 23 15:51:38 2008 +0200
@@ -81,26 +81,27 @@
$(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_inst.ML \
$(SRC)/Tools/IsaPlanner/rw_tools.ML \
$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML \
- $(SRC)/Provers/blast.ML $(SRC)/Provers/clasimp.ML \
- $(SRC)/Provers/classical.ML $(SRC)/Provers/eqsubst.ML \
- $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/order.ML \
- $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
- $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML \
- $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML \
- $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML \
- $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
- $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML \
- Tools/TFL/casesplit.ML ATP_Linkup.thy Arith_Tools.thy Code_Setup.thy \
- Datatype.thy Divides.thy Equiv_Relations.thy Extraction.thy \
- Finite_Set.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy \
- Inductive.thy Int.thy IntDiv.thy Lattices.thy List.thy Main.thy \
- Map.thy Nat.thy NatBin.thy OrderedGroup.thy Orderings.thy Power.thy \
- Predicate.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy \
- Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy \
- SAT.thy Set.thy SetInterval.thy Sum_Type.thy Groebner_Basis.thy \
- Tools/watcher.ML Tools/Groebner_Basis/groebner.ML \
- Tools/Groebner_Basis/misc.ML Tools/Groebner_Basis/normalizer.ML \
+ $(SRC)/Tools/induct_tacs.ML $(SRC)/Provers/blast.ML \
+ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
+ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
+ $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML \
+ $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/quasi.ML \
+ $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML \
+ $(SRC)/Tools/Metis/metis.ML $(SRC)/Tools/code/code_funcgr.ML \
+ $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_target.ML \
+ $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML \
+ $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/random_word.ML \
+ $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \
+ Arith_Tools.thy Code_Setup.thy Datatype.thy Divides.thy \
+ Equiv_Relations.thy Extraction.thy Finite_Set.thy Fun.thy FunDef.thy \
+ HOL.thy Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy \
+ Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \
+ OrderedGroup.thy Orderings.thy Power.thy Predicate.thy \
+ Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy \
+ Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy \
+ SetInterval.thy Sum_Type.thy Groebner_Basis.thy Tools/watcher.ML \
+ Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \
+ Tools/Groebner_Basis/normalizer.ML \
Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \
Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML \
Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML \
@@ -125,11 +126,10 @@
Tools/function_package/measure_functions.ML \
Tools/function_package/mutual.ML \
Tools/function_package/pattern_split.ML \
- Tools/function_package/size.ML Tools/induct_tacs.ML \
- Tools/inductive_codegen.ML Tools/inductive_package.ML \
- Tools/inductive_realizer.ML Tools/inductive_set_package.ML \
- Tools/lin_arith.ML Tools/meson.ML Tools/metis_tools.ML \
- Tools/numeral.ML Tools/numeral_syntax.ML \
+ Tools/function_package/size.ML Tools/inductive_codegen.ML \
+ Tools/inductive_package.ML Tools/inductive_realizer.ML \
+ Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML \
+ Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML \
Tools/old_primrec_package.ML Tools/polyhash.ML \
Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML \
Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML \
--- a/src/HOL/Tools/induct_tacs.ML Mon Jun 23 15:51:37 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,136 +0,0 @@
-(* Title: HOL/Tools/induct_tacs.ML
- ID: $Id$
- Author: Makarius
-
-Unstructured induction and cases analysis for Isabelle/HOL.
-*)
-
-signature INDUCT_TACS =
-sig
- val case_tac: Proof.context -> string -> int -> tactic
- val case_rule_tac: Proof.context -> string -> 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
- val setup: theory -> theory
-end
-
-structure InductTacs: INDUCT_TACS =
-struct
-
-(* case analysis *)
-
-fun check_type ctxt t =
- let
- val u = singleton (Variable.polymorphic ctxt) t;
- val U = Term.fastype_of u;
- val _ = Term.is_TVar U andalso
- error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
- in (u, U) end;
-
-fun gen_case_tac ctxt0 (s, opt_rule) i st =
- let
- val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
- val rule =
- (case opt_rule of
- SOME rule => rule
- | NONE =>
- (case Induct.find_casesT ctxt
- (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
- rule :: _ => rule
- | [] => @{thm case_split}));
- 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 res_inst_tac ctxt [(xi, s)] rule i st end
- handle THM _ => Seq.empty;
-
-fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
-fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
-
-
-(* induction *)
-
-local
-
-fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
- | prep_var _ = NONE;
-
-fun prep_inst (concl, xs) =
- let val vs = Induct.vars_of concl
- in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
-
-in
-
-fun gen_induct_tac ctxt0 (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);
-
- fun induct_var name =
- let
- val t = Syntax.read_term ctxt name;
- val (x, _) = Term.dest_Free t handle TERM _ =>
- error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
- 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: " ^ Syntax.string_of_term ctxt t);
- val _ =
- if (exists o Term.exists_subterm) eq_x prems then
- warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
- else ();
- in #1 (check_type ctxt t) end;
-
- val argss = map (map (Option.map induct_var)) varss;
- val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);
-
- val rule =
- (case opt_rules of
- SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
- | NONE =>
- (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
- (_, rule) :: _ => rule
- | [] => raise THM ("No induction rules", 0, [])));
-
- val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
- val _ = Method.trace ctxt [rule'];
-
- val concls = Logic.dest_conjunctions (Thm.concl_of rule);
- val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
- error "Induction rule has different numbers of variables";
- in res_inst_tac ctxt insts rule' i st end
- handle THM _ => Seq.empty;
-
-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 *)
-
-local
-
-val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
-val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
-val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
-
-val varss =
- Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
-
-in
-
-val setup =
- Method.add_methods
- [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
- "unstructured case analysis on types"),
- ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
- "unstructured induction on types")];
-
-end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/induct_tacs.ML Mon Jun 23 15:51:38 2008 +0200
@@ -0,0 +1,136 @@
+(* Title: HOL/Tools/induct_tacs.ML
+ ID: $Id$
+ Author: Makarius
+
+Unstructured induction and cases analysis.
+*)
+
+signature INDUCT_TACS =
+sig
+ val case_tac: Proof.context -> string -> int -> tactic
+ val case_rule_tac: Proof.context -> string -> 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
+ val setup: theory -> theory
+end
+
+structure InductTacs: INDUCT_TACS =
+struct
+
+(* case analysis *)
+
+fun check_type ctxt t =
+ let
+ val u = singleton (Variable.polymorphic ctxt) t;
+ val U = Term.fastype_of u;
+ val _ = Term.is_TVar U andalso
+ error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
+ in (u, U) end;
+
+fun gen_case_tac ctxt0 (s, opt_rule) i st =
+ let
+ val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
+ val rule =
+ (case opt_rule of
+ SOME rule => rule
+ | NONE =>
+ (case Induct.find_casesT ctxt
+ (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
+ rule :: _ => rule
+ | [] => @{thm case_split}));
+ 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 res_inst_tac ctxt [(xi, s)] rule i st end
+ handle THM _ => Seq.empty;
+
+fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
+fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
+
+
+(* induction *)
+
+local
+
+fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
+ | prep_var _ = NONE;
+
+fun prep_inst (concl, xs) =
+ let val vs = Induct.vars_of concl
+ in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
+
+in
+
+fun gen_induct_tac ctxt0 (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);
+
+ fun induct_var name =
+ let
+ val t = Syntax.read_term ctxt name;
+ val (x, _) = Term.dest_Free t handle TERM _ =>
+ error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
+ 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: " ^ Syntax.string_of_term ctxt t);
+ val _ =
+ if (exists o Term.exists_subterm) eq_x prems then
+ warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
+ else ();
+ in #1 (check_type ctxt t) end;
+
+ val argss = map (map (Option.map induct_var)) varss;
+ val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);
+
+ val rule =
+ (case opt_rules of
+ SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
+ | NONE =>
+ (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
+ (_, rule) :: _ => rule
+ | [] => raise THM ("No induction rules", 0, [])));
+
+ val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
+ val _ = Method.trace ctxt [rule'];
+
+ val concls = Logic.dest_conjunctions (Thm.concl_of rule);
+ val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
+ error "Induction rule has different numbers of variables";
+ in res_inst_tac ctxt insts rule' i st end
+ handle THM _ => Seq.empty;
+
+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 *)
+
+local
+
+val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
+val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
+val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
+
+val varss =
+ Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
+
+in
+
+val setup =
+ Method.add_methods
+ [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
+ "unstructured case analysis on types"),
+ ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
+ "unstructured induction on types")];
+
+end;
+
+end;
+