src/HOL/Tools/induct_method.ML
changeset 9066 b1e874e38dab
parent 8815 187547eae4c5
child 9230 17ae63f82ad8
equal deleted inserted replaced
9065:15f82c9aa331 9066:b1e874e38dab
   189         cases t       - datatype exhaustion
   189         cases t       - datatype exhaustion
   190   <x:A> cases ...     - set elimination
   190   <x:A> cases ...     - set elimination
   191   ...   cases ... R   - explicit rule
   191   ...   cases ... R   - explicit rule
   192 *)
   192 *)
   193 
   193 
       
   194 val case_split = RuleCases.name ["True", "False"] case_split_thm;
       
   195 
   194 local
   196 local
   195 
   197 
   196 fun cases_var thm =
   198 fun cases_var thm =
   197   (case try (hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of
   199   (case try (hd o vars_of o hd o Logic.strip_assums_hyp o Library.last_elem o Thm.prems_of) thm of
   198     None => raise THM ("Malformed cases rule", 0, [thm])
   200     None => raise THM ("Malformed cases rule", 0, [thm])
   215       NetRules.may_unify (#2 (get_cases ctxt))
   217       NetRules.may_unify (#2 (get_cases ctxt))
   216         (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
   218         (Logic.strip_assums_concl (#prop (Thm.rep_thm th)));
   217 
   219 
   218     val rules =
   220     val rules =
   219       (case (args, facts) of
   221       (case (args, facts) of
   220         ((None, None), []) => [(case_split_thm, ["True", "False"])]
   222         ((None, None), []) => [RuleCases.add case_split]
   221       | ((Some t, None), []) =>
   223       | ((Some t, None), []) =>
   222           let val name = type_name t in
   224           let val name = type_name t in
   223             (case lookup_casesT ctxt name of
   225             (case lookup_casesT ctxt name of
   224               None => error ("No cases rule for type: " ^ quote name)
   226               None => error ("No cases rule for type: " ^ quote name)
   225             | Some thm => [(inst_rule t thm, RuleCases.get thm)])
   227             | Some thm => [(inst_rule t thm, RuleCases.get thm)])
   425    Attrib.add_attributes
   427    Attrib.add_attributes
   426     [(casesN, cases_attr, "cases rule for type or set"),
   428     [(casesN, cases_attr, "cases rule for type or set"),
   427      (inductN, induct_attr, "induction rule for type or set")],
   429      (inductN, induct_attr, "induction rule for type or set")],
   428    Method.add_methods
   430    Method.add_methods
   429     [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
   431     [("cases", cases_meth oo cases_args, "case analysis on types or sets"),
   430      ("induct", induct_meth oo induct_args, "induction on types or sets")]];
   432      ("induct", induct_meth oo induct_args, "induction on types or sets")],
   431 
   433    (#1 o PureThy.add_thms [(("case_split", case_split), [])])];
   432 end;
   434 
       
   435 end;