src/Tools/induct_tacs.ML
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (18 months ago)
changeset 67835 c8e4ee2b5482
parent 67149 e61557884799
permissions -rw-r--r--
tuned imports;
     1 (*  Title:      Tools/induct_tacs.ML
     2     Author:     Makarius
     3 
     4 Unstructured induction and cases analysis.
     5 *)
     6 
     7 signature INDUCT_TACS =
     8 sig
     9   val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
    10     thm option -> int -> tactic
    11   val induct_tac: Proof.context -> string option list list ->
    12     thm list option -> int -> tactic
    13 end
    14 
    15 structure Induct_Tacs: INDUCT_TACS =
    16 struct
    17 
    18 (* case analysis *)
    19 
    20 fun check_type ctxt (t, pos) =
    21   let
    22     val u = singleton (Variable.polymorphic ctxt) t;
    23     val U = Term.fastype_of u;
    24     val _ = Term.is_TVar U andalso
    25       error ("Cannot determine type of " ^
    26         quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
    27   in (u, U) end;
    28 
    29 fun case_tac ctxt s fixes opt_rule = SUBGOAL (fn (goal, i) =>
    30   let
    31     val rule =
    32       (case opt_rule of
    33         SOME rule => rule
    34       | NONE =>
    35           let
    36             val (t, ctxt') = ctxt
    37               |> Rule_Insts.goal_context goal |> #2
    38               |> Context_Position.set_visible false
    39               |> Rule_Insts.read_term s;
    40             val pos = Syntax.read_input_pos s;
    41           in
    42             (case Induct.find_casesT ctxt' (#2 (check_type ctxt' (t, pos))) of
    43               rule :: _ => rule
    44             | [] => @{thm case_split})
    45           end);
    46     val _ = Method.trace ctxt [rule];
    47   in
    48     (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) handle THM _ => [] of
    49       Var (xi, _) :: _ => Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i
    50     | _ => no_tac)
    51   end);
    52 
    53 
    54 (* induction *)
    55 
    56 local
    57 
    58 fun prep_var (Var (xi, _), SOME x) = SOME ((xi, Position.none), x)
    59   | prep_var _ = NONE;
    60 
    61 fun prep_inst (concl, xs) =
    62   let val vs = Induct.vars_of concl
    63   in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end;
    64 
    65 in
    66 
    67 fun induct_tac ctxt varss opt_rules i st =
    68   let
    69     val goal = Thm.cprem_of st i;
    70     val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
    71     and ((_, goal'), _) = Variable.focus_cterm NONE goal ctxt;
    72     val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
    73 
    74     fun induct_var name =
    75       let
    76         val t = Syntax.read_term goal_ctxt name;
    77         val pos = Syntax.read_input_pos name;
    78         val (x, _) = Term.dest_Free t handle TERM _ =>
    79           error ("Induction argument not a variable: " ^
    80             quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
    81         val eq_x = fn Free (y, _) => x = y | _ => false;
    82         val _ =
    83           if Term.exists_subterm eq_x concl then ()
    84           else
    85             error ("No such variable in subgoal: " ^
    86               quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos);
    87         val _ =
    88           if (exists o Term.exists_subterm) eq_x prems then
    89             warning ("Induction variable occurs also among premises: " ^
    90               quote (Syntax.string_of_term goal_ctxt t) ^ Position.here pos)
    91           else ();
    92       in #1 (check_type goal_ctxt (t, pos)) end;
    93 
    94     val argss = (map o map o Option.map) induct_var varss;
    95     val rule =
    96       (case opt_rules of
    97         SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
    98       | NONE =>
    99           (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
   100             (_, rule) :: _ => rule
   101           | [] => raise THM ("No induction rules", 0, [])));
   102 
   103     val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 (Object_Logic.atomize ctxt));
   104     val _ = Method.trace ctxt [rule'];
   105 
   106     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
   107     val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
   108       error "Induction rule has different numbers of variables";
   109   in Rule_Insts.res_inst_tac ctxt insts [] rule' i st end
   110   handle THM _ => Seq.empty;
   111 
   112 end;
   113 
   114 
   115 (* method syntax *)
   116 
   117 local
   118 
   119 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":");
   120 val opt_rule = Scan.option (rule_spec |-- Attrib.thm);
   121 val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
   122 
   123 val varss =
   124   Parse.and_list'
   125     (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.embedded_inner_syntax))));
   126 
   127 in
   128 
   129 val _ =
   130   Theory.setup
   131    (Method.setup \<^binding>\<open>case_tac\<close>
   132       (Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) -- opt_rule >>
   133         (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
   134       "unstructured case analysis on types" #>
   135     Method.setup \<^binding>\<open>induct_tac\<close>
   136       (Args.goal_spec -- varss -- opt_rules >>
   137         (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt vs rs)))
   138       "unstructured induction on types");
   139 
   140 end;
   141 
   142 end;