src/Tools/induct_tacs.ML
changeset 30541 9f168bdc468a
parent 30161 c26e515f1c29
child 32863 5e8cef567042
equal deleted inserted replaced
30540:5e2d9604a3d3 30541:9f168bdc468a
    24     val U = Term.fastype_of u;
    24     val U = Term.fastype_of u;
    25     val _ = Term.is_TVar U andalso
    25     val _ = Term.is_TVar U andalso
    26       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    26       error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
    27   in (u, U) end;
    27   in (u, U) end;
    28 
    28 
    29 fun gen_case_tac ctxt0 (s, opt_rule) i st =
    29 fun gen_case_tac ctxt0 s opt_rule i st =
    30   let
    30   let
    31     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    31     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    32     val rule =
    32     val rule =
    33       (case opt_rule of
    33       (case opt_rule of
    34         SOME rule => rule
    34         SOME rule => rule
    44         Var (xi, _) :: _ => xi
    44         Var (xi, _) :: _ => xi
    45       | _ => raise THM ("Malformed cases rule", 0, [rule]));
    45       | _ => raise THM ("Malformed cases rule", 0, [rule]));
    46   in res_inst_tac ctxt [(xi, s)] rule i st end
    46   in res_inst_tac ctxt [(xi, s)] rule i st end
    47   handle THM _ => Seq.empty;
    47   handle THM _ => Seq.empty;
    48 
    48 
    49 fun case_tac ctxt s = gen_case_tac ctxt (s, NONE);
    49 fun case_tac ctxt s = gen_case_tac ctxt s NONE;
    50 fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule);
    50 fun case_rule_tac ctxt s rule = gen_case_tac ctxt s (SOME rule);
    51 
    51 
    52 
    52 
    53 (* induction *)
    53 (* induction *)
    54 
    54 
    55 local
    55 local
    61   let val vs = Induct.vars_of concl
    61   let val vs = Induct.vars_of concl
    62   in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    62   in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    63 
    63 
    64 in
    64 in
    65 
    65 
    66 fun gen_induct_tac ctxt0 (varss, opt_rules) i st =
    66 fun gen_induct_tac ctxt0 varss opt_rules i st =
    67   let
    67   let
    68     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    68     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
    69     val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
    69     val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
    70 
    70 
    71     fun induct_var name =
    71     fun induct_var name =
   101   in res_inst_tac ctxt insts rule' i st end
   101   in res_inst_tac ctxt insts rule' i st end
   102   handle THM _ => Seq.empty;
   102   handle THM _ => Seq.empty;
   103 
   103 
   104 end;
   104 end;
   105 
   105 
   106 fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE);
   106 fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
   107 fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules);
   107 fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
   108 
   108 
   109 
   109 
   110 (* method syntax *)
   110 (* method syntax *)
   111 
   111 
   112 local
   112 local
   120     (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
   120     (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
   121 
   121 
   122 in
   122 in
   123 
   123 
   124 val setup =
   124 val setup =
   125   Method.add_methods
   125   Method.setup @{binding case_tac}
   126    [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
   126     (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
   127       "unstructured case analysis on types"),
   127       (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
   128     ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
   128     "unstructured case analysis on types" #>
   129       "unstructured induction on types")];
   129   Method.setup @{binding induct_tac}
       
   130     (Args.goal_spec -- varss -- opt_rules >>
       
   131       (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
       
   132     "unstructured induction on types";
   130 
   133 
   131 end;
   134 end;
   132 
   135 
   133 end;
   136 end;
   134 
   137