src/HOL/Tools/datatype_package.ML
changeset 27130 4ba366056426
parent 27104 791607529f6d
child 27261 5b3101338f42
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 10 19:15:21 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 10 19:15:23 2008 +0200
     1.3 @@ -20,9 +20,6 @@
     1.4      -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a}
     1.5      -> (string * sort) list -> string list
     1.6      -> (string * (string * 'a list) list) list
     1.7 -  val induct_tac : Proof.context -> string -> int -> tactic
     1.8 -  val induct_thm_tac : Proof.context -> thm -> string -> int -> tactic
     1.9 -  val case_tac : string -> int -> tactic
    1.10    val distinct_simproc : simproc
    1.11    val make_case :  Proof.context -> bool -> string list -> term ->
    1.12      (term * term) list -> term * (term * (int * bool)) list
    1.13 @@ -162,133 +159,6 @@
    1.14      fun interpK (_, (tyco, _, cs)) = (tyco, map interpC cs);
    1.15    in map interpK (Library.take (k, descr)) end;
    1.16  
    1.17 -fun find_tname var Bi =
    1.18 -  let val frees = map dest_Free (term_frees Bi)
    1.19 -      val params = rename_wrt_term Bi (Logic.strip_params Bi);
    1.20 -  in case AList.lookup (op =) (frees @ params) var of
    1.21 -       NONE => error ("No such variable in subgoal: " ^ quote var)
    1.22 -     | SOME(Type (tn, _)) => tn
    1.23 -     | _ => error ("Cannot determine type of " ^ quote var)
    1.24 -  end;
    1.25 -
    1.26 -fun infer_tname state i aterm =
    1.27 -  let
    1.28 -    val sign = Thm.theory_of_thm state;
    1.29 -    val (_, _, Bi, _) = Thm.dest_state (state, i)
    1.30 -    val params = Logic.strip_params Bi;   (*params of subgoal i*)
    1.31 -    val params = rev (rename_wrt_term Bi params);   (*as they are printed*)
    1.32 -    val (types, sorts) = types_sorts state;
    1.33 -    fun types' (a, ~1) = (case AList.lookup (op =) params a of NONE => types(a, ~1) | sm => sm)
    1.34 -      | types' ixn = types ixn;
    1.35 -    val ([ct], _) = Thm.read_def_cterms (sign, types', sorts) [] false [(aterm, dummyT)];
    1.36 -  in case #T (rep_cterm ct) of
    1.37 -       Type (tn, _) => tn
    1.38 -     | _ => error ("Cannot determine type of " ^ quote aterm)
    1.39 -  end;
    1.40 -
    1.41 -(*Warn if the (induction) variable occurs Free among the premises, which
    1.42 -  usually signals a mistake.  But calls the tactic either way!*)
    1.43 -fun occs_in_prems tacf vars =
    1.44 -  SUBGOAL (fn (Bi, i) =>
    1.45 -           (if exists (fn (a, _) => member (op =) vars a)
    1.46 -                      (fold Term.add_frees (#2 (strip_context Bi)) [])
    1.47 -             then warning "Induction variable occurs also among premises!"
    1.48 -             else ();
    1.49 -            tacf i));
    1.50 -
    1.51 -
    1.52 -(* generic induction tactic for datatypes *)
    1.53 -
    1.54 -local
    1.55 -
    1.56 -fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x)
    1.57 -  | prep_var _ = NONE;
    1.58 -
    1.59 -fun prep_inst (concl, xs) = (*exception Library.UnequalLengths*)
    1.60 -  let val vs = Induct.vars_of concl
    1.61 -  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    1.62 -
    1.63 -in
    1.64 -
    1.65 -fun gen_induct_tac inst_tac ctxt (varss, opt_rule) i state =
    1.66 -  SUBGOAL (fn (Bi,_) =>
    1.67 -  let
    1.68 -    val (rule, rule_name) =
    1.69 -      case opt_rule of
    1.70 -          SOME r => (r, "Induction rule")
    1.71 -        | NONE =>
    1.72 -            let val tn = find_tname (hd (map_filter I (flat varss))) Bi
    1.73 -                val thy = Thm.theory_of_thm state
    1.74 -            in case Induct.lookup_inductT ctxt tn of
    1.75 -                SOME thm => (thm, "Induction rule for type " ^ tn)
    1.76 -              | NONE => error ("No induction rule for type " ^ tn)
    1.77 -            end
    1.78 -    val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.79 -    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    1.80 -      error (rule_name ^ " has different numbers of variables");
    1.81 -  in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
    1.82 -  i state;
    1.83 -
    1.84 -fun induct_tac ctxt s =
    1.85 -  gen_induct_tac Tactic.res_inst_tac' ctxt
    1.86 -    (map (single o SOME) (Syntax.read_idents s), NONE);
    1.87 -
    1.88 -fun induct_thm_tac ctxt th s =
    1.89 -  gen_induct_tac Tactic.res_inst_tac' ctxt
    1.90 -    ([map SOME (Syntax.read_idents s)], SOME th);
    1.91 -
    1.92 -end;
    1.93 -
    1.94 -
    1.95 -(* generic case tactic for datatypes *)
    1.96 -
    1.97 -fun case_inst_tac inst_tac t rule i state =
    1.98 -  let
    1.99 -    val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
   1.100 -      (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
   1.101 -  in inst_tac [(ixn, t)] rule i state end;
   1.102 -
   1.103 -fun gen_case_tac inst_tac (t, SOME rule) i state =
   1.104 -      case_inst_tac inst_tac t rule i state
   1.105 -  | gen_case_tac inst_tac (t, NONE) i state =
   1.106 -      let val tn = infer_tname state i t in
   1.107 -        if tn = HOLogic.boolN then inst_tac [(("P", 0), t)] case_split_thm i state
   1.108 -        else case_inst_tac inst_tac t
   1.109 -               (#exhaustion (the_datatype (Thm.theory_of_thm state) tn))
   1.110 -               i state
   1.111 -      end handle THM _ => Seq.empty;
   1.112 -
   1.113 -fun case_tac t = gen_case_tac Tactic.res_inst_tac' (t, NONE);
   1.114 -
   1.115 -
   1.116 -
   1.117 -(** Isar tactic emulations **)
   1.118 -
   1.119 -local
   1.120 -
   1.121 -val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   1.122 -val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   1.123 -
   1.124 -val varss =
   1.125 -  Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name))));
   1.126 -
   1.127 -val inst_tac = RuleInsts.bires_inst_tac false;
   1.128 -
   1.129 -fun induct_meth ctxt (varss, opt_rule) =
   1.130 -  gen_induct_tac (inst_tac ctxt) ctxt (varss, opt_rule);
   1.131 -fun case_meth ctxt (varss, opt_rule) =
   1.132 -  gen_case_tac (inst_tac ctxt) (varss, opt_rule);
   1.133 -
   1.134 -in
   1.135 -
   1.136 -val tactic_emulations =
   1.137 - [("induct_tac", Method.goal_args_ctxt' (varss -- opt_rule) induct_meth,
   1.138 -    "induct_tac emulation (dynamic instantiation)"),
   1.139 -  ("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) case_meth,
   1.140 -    "case_tac emulation (dynamic instantiation)")];
   1.141 -
   1.142 -end;
   1.143 -
   1.144  
   1.145  
   1.146  (** induct method setup **)
   1.147 @@ -807,7 +677,6 @@
   1.148  
   1.149  val setup =
   1.150    DatatypeRepProofs.distinctness_limit_setup #>
   1.151 -  Method.add_methods tactic_emulations #>
   1.152    simproc_setup #>
   1.153    trfun_setup #>
   1.154    DatatypeInterpretation.init;