moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
authorwenzelm
Mon Jun 23 15:51:38 2008 +0200 (2008-06-23)
changeset 27326d3beec370964
parent 27325 70e4eb732fa9
child 27327 efd626efcb04
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Tools/induct_tacs.ML
src/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Jun 23 15:51:37 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Jun 23 15:51:38 2008 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    "~~/src/Tools/random_word.ML"
     1.5    "~~/src/Tools/atomize_elim.ML"
     1.6    "~~/src/Tools/induct.ML"
     1.7 -  ("~~/src/HOL/Tools/induct_tacs.ML")
     1.8 +  ("~~/src/Tools/induct_tacs.ML")
     1.9    "~~/src/Tools/code/code_name.ML"
    1.10    "~~/src/Tools/code/code_funcgr.ML"
    1.11    "~~/src/Tools/code/code_thingol.ML"
    1.12 @@ -1554,7 +1554,7 @@
    1.13  
    1.14  setup Induct.setup
    1.15  
    1.16 -use "~~/src/HOL/Tools/induct_tacs.ML"
    1.17 +use "~~/src/Tools/induct_tacs.ML"
    1.18  setup InductTacs.setup
    1.19  
    1.20  
     2.1 --- a/src/HOL/IsaMakefile	Mon Jun 23 15:51:37 2008 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Jun 23 15:51:38 2008 +0200
     2.3 @@ -81,26 +81,27 @@
     2.4    $(SRC)/Tools/IsaPlanner/isand.ML $(SRC)/Tools/IsaPlanner/rw_inst.ML	\
     2.5    $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
     2.6    $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML		\
     2.7 -  $(SRC)/Provers/blast.ML $(SRC)/Provers/clasimp.ML			\
     2.8 -  $(SRC)/Provers/classical.ML $(SRC)/Provers/eqsubst.ML			\
     2.9 -  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/order.ML			\
    2.10 -  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
    2.11 -  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
    2.12 -  $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML			\
    2.13 -  $(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML	\
    2.14 -  $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML	\
    2.15 -  $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML			\
    2.16 -  $(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML			\
    2.17 -  Tools/TFL/casesplit.ML ATP_Linkup.thy Arith_Tools.thy Code_Setup.thy	\
    2.18 -  Datatype.thy Divides.thy Equiv_Relations.thy Extraction.thy		\
    2.19 -  Finite_Set.thy Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy		\
    2.20 -  Inductive.thy Int.thy IntDiv.thy Lattices.thy List.thy Main.thy	\
    2.21 -  Map.thy Nat.thy NatBin.thy OrderedGroup.thy Orderings.thy Power.thy	\
    2.22 -  Predicate.thy Product_Type.thy ROOT.ML Recdef.thy Record.thy		\
    2.23 -  Refute.thy Relation.thy Relation_Power.thy Ring_and_Field.thy		\
    2.24 -  SAT.thy Set.thy SetInterval.thy Sum_Type.thy Groebner_Basis.thy	\
    2.25 -  Tools/watcher.ML Tools/Groebner_Basis/groebner.ML			\
    2.26 -  Tools/Groebner_Basis/misc.ML Tools/Groebner_Basis/normalizer.ML	\
    2.27 +  $(SRC)/Tools/induct_tacs.ML $(SRC)/Provers/blast.ML			\
    2.28 +  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
    2.29 +  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
    2.30 +  $(SRC)/Provers/order.ML $(SRC)/Provers/project_rule.ML		\
    2.31 +  $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/quasi.ML			\
    2.32 +  $(SRC)/Provers/splitter.ML $(SRC)/Provers/trancl.ML			\
    2.33 +  $(SRC)/Tools/Metis/metis.ML $(SRC)/Tools/code/code_funcgr.ML		\
    2.34 +  $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_target.ML	\
    2.35 +  $(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML			\
    2.36 +  $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/random_word.ML		\
    2.37 +  $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy		\
    2.38 +  Arith_Tools.thy Code_Setup.thy Datatype.thy Divides.thy		\
    2.39 +  Equiv_Relations.thy Extraction.thy Finite_Set.thy Fun.thy FunDef.thy	\
    2.40 +  HOL.thy Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy		\
    2.41 +  Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy		\
    2.42 +  OrderedGroup.thy Orderings.thy Power.thy Predicate.thy		\
    2.43 +  Product_Type.thy ROOT.ML Recdef.thy Record.thy Refute.thy		\
    2.44 +  Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy	\
    2.45 +  SetInterval.thy Sum_Type.thy Groebner_Basis.thy Tools/watcher.ML	\
    2.46 +  Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
    2.47 +  Tools/Groebner_Basis/normalizer.ML					\
    2.48    Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML		\
    2.49    Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML			\
    2.50    Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML		\
    2.51 @@ -125,11 +126,10 @@
    2.52    Tools/function_package/measure_functions.ML				\
    2.53    Tools/function_package/mutual.ML					\
    2.54    Tools/function_package/pattern_split.ML				\
    2.55 -  Tools/function_package/size.ML Tools/induct_tacs.ML			\
    2.56 -  Tools/inductive_codegen.ML Tools/inductive_package.ML			\
    2.57 -  Tools/inductive_realizer.ML Tools/inductive_set_package.ML		\
    2.58 -  Tools/lin_arith.ML Tools/meson.ML Tools/metis_tools.ML		\
    2.59 -  Tools/numeral.ML Tools/numeral_syntax.ML				\
    2.60 +  Tools/function_package/size.ML Tools/inductive_codegen.ML		\
    2.61 +  Tools/inductive_package.ML Tools/inductive_realizer.ML		\
    2.62 +  Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
    2.63 +  Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
    2.64    Tools/old_primrec_package.ML Tools/polyhash.ML			\
    2.65    Tools/primrec_package.ML Tools/prop_logic.ML Tools/recdef_package.ML	\
    2.66    Tools/recfun_codegen.ML Tools/record_package.ML Tools/refute.ML	\
     3.1 --- a/src/HOL/Tools/induct_tacs.ML	Mon Jun 23 15:51:37 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,136 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/induct_tacs.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Makarius
     3.7 -
     3.8 -Unstructured induction and cases analysis for Isabelle/HOL.
     3.9 -*)
    3.10 -
    3.11 -signature INDUCT_TACS =
    3.12 -sig
    3.13 -  val case_tac: Proof.context -> string -> int -> tactic
    3.14 -  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
    3.15 -  val induct_tac: Proof.context -> string option list list -> int -> tactic
    3.16 -  val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
    3.17 -  val setup: theory -> theory
    3.18 -end
    3.19 -
    3.20 -structure InductTacs: INDUCT_TACS =
    3.21 -struct
    3.22 -
    3.23 -(* case analysis *)
    3.24 -
    3.25 -fun check_type ctxt t =
    3.26 -  let
    3.27 -    val u = singleton (Variable.polymorphic ctxt) t;
    3.28 -    val U = Term.fastype_of u;
    3.29 -    val _ = Term.is_TVar U andalso
    3.30 -      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    3.31 -  in (u, U) end;
    3.32 -
    3.33 -fun gen_case_tac ctxt0 (s, opt_rule) i st =
    3.34 -  let
    3.35 -    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    3.36 -    val rule =
    3.37 -      (case opt_rule of
    3.38 -        SOME rule => rule
    3.39 -      | NONE =>
    3.40 -          (case Induct.find_casesT ctxt
    3.41 -              (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
    3.42 -            rule :: _ => rule
    3.43 -          | [] => @{thm case_split}));
    3.44 -    val _ = Method.trace ctxt [rule];
    3.45 -
    3.46 -    val xi =
    3.47 -      (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
    3.48 -        Var (xi, _) :: _ => xi
    3.49 -      | _ => raise THM ("Malformed cases rule", 0, [rule]));
    3.50 -  in res_inst_tac ctxt [(xi, s)] rule i st end
    3.51 -  handle THM _ => Seq.empty;
    3.52 -
    3.53 -fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
    3.54 -fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
    3.55 -
    3.56 -
    3.57 -(* induction *)
    3.58 -
    3.59 -local
    3.60 -
    3.61 -fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
    3.62 -  | prep_var _ = NONE;
    3.63 -
    3.64 -fun prep_inst (concl, xs) =
    3.65 -  let val vs = Induct.vars_of concl
    3.66 -  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    3.67 -
    3.68 -in
    3.69 -
    3.70 -fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
    3.71 -  let
    3.72 -    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    3.73 -    val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
    3.74 -
    3.75 -    fun induct_var name =
    3.76 -      let
    3.77 -        val t = Syntax.read_term ctxt name;
    3.78 -        val (x, _) = Term.dest_Free t handle TERM _ =>
    3.79 -          error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
    3.80 -        val eq_x = fn Free (y, _) => x = y | _ => false;
    3.81 -        val _ =
    3.82 -          if Term.exists_subterm eq_x concl then ()
    3.83 -          else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t);
    3.84 -        val _ =
    3.85 -          if (exists o Term.exists_subterm) eq_x prems then
    3.86 -            warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
    3.87 -          else ();
    3.88 -      in #1 (check_type ctxt t) end;
    3.89 -
    3.90 -    val argss = map (map (Option.map induct_var)) varss;
    3.91 -    val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);
    3.92 -
    3.93 -    val rule =
    3.94 -      (case opt_rules of
    3.95 -        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
    3.96 -      | NONE =>
    3.97 -          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
    3.98 -            (_, rule) :: _ => rule
    3.99 -          | [] => raise THM ("No induction rules", 0, [])));
   3.100 -
   3.101 -    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
   3.102 -    val _ = Method.trace ctxt [rule'];
   3.103 -
   3.104 -    val concls = Logic.dest_conjunctions (Thm.concl_of rule);
   3.105 -    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
   3.106 -      error "Induction rule has different numbers of variables";
   3.107 -  in res_inst_tac ctxt insts rule' i st end
   3.108 -  handle THM _ => Seq.empty;
   3.109 -
   3.110 -end;
   3.111 -
   3.112 -fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
   3.113 -fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
   3.114 -
   3.115 -
   3.116 -(* method syntax *)
   3.117 -
   3.118 -local
   3.119 -
   3.120 -val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   3.121 -val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   3.122 -val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
   3.123 -
   3.124 -val varss =
   3.125 -  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
   3.126 -
   3.127 -in
   3.128 -
   3.129 -val setup =
   3.130 -  Method.add_methods
   3.131 -   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
   3.132 -      "unstructured case analysis on types"),
   3.133 -    ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
   3.134 -      "unstructured induction on types")];
   3.135 -
   3.136 -end;
   3.137 -
   3.138 -end;
   3.139 -
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/induct_tacs.ML	Mon Jun 23 15:51:38 2008 +0200
     4.3 @@ -0,0 +1,136 @@
     4.4 +(*  Title:      HOL/Tools/induct_tacs.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +Unstructured induction and cases analysis.
     4.9 +*)
    4.10 +
    4.11 +signature INDUCT_TACS =
    4.12 +sig
    4.13 +  val case_tac: Proof.context -> string -> int -> tactic
    4.14 +  val case_rule_tac: Proof.context -> string -> thm -> int -> tactic
    4.15 +  val induct_tac: Proof.context -> string option list list -> int -> tactic
    4.16 +  val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
    4.17 +  val setup: theory -> theory
    4.18 +end
    4.19 +
    4.20 +structure InductTacs: INDUCT_TACS =
    4.21 +struct
    4.22 +
    4.23 +(* case analysis *)
    4.24 +
    4.25 +fun check_type ctxt t =
    4.26 +  let
    4.27 +    val u = singleton (Variable.polymorphic ctxt) t;
    4.28 +    val U = Term.fastype_of u;
    4.29 +    val _ = Term.is_TVar U andalso
    4.30 +      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    4.31 +  in (u, U) end;
    4.32 +
    4.33 +fun gen_case_tac ctxt0 (s, opt_rule) i st =
    4.34 +  let
    4.35 +    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    4.36 +    val rule =
    4.37 +      (case opt_rule of
    4.38 +        SOME rule => rule
    4.39 +      | NONE =>
    4.40 +          (case Induct.find_casesT ctxt
    4.41 +              (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of
    4.42 +            rule :: _ => rule
    4.43 +          | [] => @{thm case_split}));
    4.44 +    val _ = Method.trace ctxt [rule];
    4.45 +
    4.46 +    val xi =
    4.47 +      (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
    4.48 +        Var (xi, _) :: _ => xi
    4.49 +      | _ => raise THM ("Malformed cases rule", 0, [rule]));
    4.50 +  in res_inst_tac ctxt [(xi, s)] rule i st end
    4.51 +  handle THM _ => Seq.empty;
    4.52 +
    4.53 +fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
    4.54 +fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
    4.55 +
    4.56 +
    4.57 +(* induction *)
    4.58 +
    4.59 +local
    4.60 +
    4.61 +fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
    4.62 +  | prep_var _ = NONE;
    4.63 +
    4.64 +fun prep_inst (concl, xs) =
    4.65 +  let val vs = Induct.vars_of concl
    4.66 +  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    4.67 +
    4.68 +in
    4.69 +
    4.70 +fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
    4.71 +  let
    4.72 +    val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    4.73 +    val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
    4.74 +
    4.75 +    fun induct_var name =
    4.76 +      let
    4.77 +        val t = Syntax.read_term ctxt name;
    4.78 +        val (x, _) = Term.dest_Free t handle TERM _ =>
    4.79 +          error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
    4.80 +        val eq_x = fn Free (y, _) => x = y | _ => false;
    4.81 +        val _ =
    4.82 +          if Term.exists_subterm eq_x concl then ()
    4.83 +          else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t);
    4.84 +        val _ =
    4.85 +          if (exists o Term.exists_subterm) eq_x prems then
    4.86 +            warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
    4.87 +          else ();
    4.88 +      in #1 (check_type ctxt t) end;
    4.89 +
    4.90 +    val argss = map (map (Option.map induct_var)) varss;
    4.91 +    val _ = forall null argss andalso raise THM ("No induction arguments", 0, []);
    4.92 +
    4.93 +    val rule =
    4.94 +      (case opt_rules of
    4.95 +        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
    4.96 +      | NONE =>
    4.97 +          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
    4.98 +            (_, rule) :: _ => rule
    4.99 +          | [] => raise THM ("No induction rules", 0, [])));
   4.100 +
   4.101 +    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
   4.102 +    val _ = Method.trace ctxt [rule'];
   4.103 +
   4.104 +    val concls = Logic.dest_conjunctions (Thm.concl_of rule);
   4.105 +    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
   4.106 +      error "Induction rule has different numbers of variables";
   4.107 +  in res_inst_tac ctxt insts rule' i st end
   4.108 +  handle THM _ => Seq.empty;
   4.109 +
   4.110 +end;
   4.111 +
   4.112 +fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
   4.113 +fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
   4.114 +
   4.115 +
   4.116 +(* method syntax *)
   4.117 +
   4.118 +local
   4.119 +
   4.120 +val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   4.121 +val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   4.122 +val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
   4.123 +
   4.124 +val varss =
   4.125 +  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
   4.126 +
   4.127 +in
   4.128 +
   4.129 +val setup =
   4.130 +  Method.add_methods
   4.131 +   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
   4.132 +      "unstructured case analysis on types"),
   4.133 +    ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
   4.134 +      "unstructured induction on types")];
   4.135 +
   4.136 +end;
   4.137 +
   4.138 +end;
   4.139 +