src/HOL/Tools/datatype_package.ML
changeset 20715 c1f16b427d86
parent 20597 65fe827aa595
child 20820 58693343905f
equal deleted inserted replaced
20714:6a122dba034c 20715:c1f16b427d86
   402     let
   402     let
   403       val thy = Context.theory_of context;
   403       val thy = Context.theory_of context;
   404       fun case_error s name ts = raise TERM ("Error in case expression" ^
   404       fun case_error s name ts = raise TERM ("Error in case expression" ^
   405         getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
   405         getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
   406       fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
   406       fun dest_case1 (Const ("_case1", _) $ t $ u) = (case strip_comb t of
   407             (Const (s, _), ts) => (Sign.intern_const thy s, ts)
   407             (Const (s, _), ts) => (((perhaps o try o unprefix) Syntax.constN o Sign.intern_const thy) s, ts)
   408           | (Free (s, _), ts) => (Sign.intern_const thy s, ts)
   408           | (Free (s, _), ts) => (Sign.intern_const thy s, ts) (*FIXME?*)
   409           | _ => case_error "Head is not a constructor" NONE [t, u], u)
   409           | _ => case_error "Head is not a constructor" NONE [t, u], u)
   410         | dest_case1 t = raise TERM ("dest_case1", [t]);
   410         | dest_case1 t = raise TERM ("dest_case1", [t]);
   411       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   411       fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   412         | dest_case2 t = [t];
   412         | dest_case2 t = [t];
   413       val cases as ((cname, _), _) :: _ = map dest_case1 (dest_case2 u);
   413       val cases as ((cname, _), _) :: _ = map dest_case1 (dest_case2 u);
   815     val (((distinct, inject), [induction]), thy1) =
   815     val (((distinct, inject), [induction]), thy1) =
   816       thy0
   816       thy0
   817       |> fold_map apply_theorems raw_distinct
   817       |> fold_map apply_theorems raw_distinct
   818       ||>> fold_map apply_theorems raw_inject
   818       ||>> fold_map apply_theorems raw_inject
   819       ||>> apply_theorems [raw_induction];
   819       ||>> apply_theorems [raw_induction];
   820     val sign = Theory.sign_of thy1;
       
   821 
   820 
   822     val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
   821     val ((_, [induction']), _) = Variable.importT [induction] (Variable.thm_context induction);
   823 
   822 
   824     fun err t = error ("Ill-formed predicate in induction rule: " ^
   823     fun err t = error ("Ill-formed predicate in induction rule: " ^
   825       Sign.string_of_term sign t);
   824       Sign.string_of_term thy1 t);
   826 
   825 
   827     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   826     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   828           ((tname, map dest_TFree Ts) handle TERM _ => err t)
   827           ((tname, map dest_TFree Ts) handle TERM _ => err t)
   829       | get_typ t = err t;
   828       | get_typ t = err t;
   830 
   829 
   848 
   847 
   849     val descr = make_dt_spec dtnames 0 (map get_constr (prems_of induction'));
   848     val descr = make_dt_spec dtnames 0 (map get_constr (prems_of induction'));
   850     val sorts = add_term_tfrees (concl_of induction', []);
   849     val sorts = add_term_tfrees (concl_of induction', []);
   851     val dt_info = get_datatypes thy1;
   850     val dt_info = get_datatypes thy1;
   852 
   851 
   853     val case_names_induct = mk_case_names_induct descr;
   852     val (case_names_induct, case_names_exhausts) = case RuleCases.get induction
   854     val case_names_exhausts = mk_case_names_exhausts descr (map #1 dtnames);
   853      of (("1", _) :: _, _) => (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames))
       
   854       | (cases, _) => (RuleCases.case_names (map fst cases),
       
   855           replicate (length ((List.filter (fn ((_, (name, _, _))) => member (op =)
       
   856             (map #1 dtnames) name) descr)))
       
   857             (RuleCases.case_names (map fst cases)));
   855     
   858     
   856 
   859 
   857     val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   860     val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   858 
   861 
   859     val (casedist_thms, thy2) = thy1 |>
   862     val (casedist_thms, thy2) = thy1 |>