# HG changeset patch # User wenzelm # Date 1214229098 -7200 # Node ID d3beec3709646591aa1b122987a926cc161bb3c8 # Parent 70e4eb732fa97dbfaf4b707639c347183e469f8f moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML; diff -r 70e4eb732fa9 -r d3beec370964 src/HOL/HOL.thy --- 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 diff -r 70e4eb732fa9 -r d3beec370964 src/HOL/IsaMakefile --- 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 \ diff -r 70e4eb732fa9 -r d3beec370964 src/HOL/Tools/induct_tacs.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; - diff -r 70e4eb732fa9 -r d3beec370964 src/Tools/induct_tacs.ML --- /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; +