src/HOL/datatype.ML
changeset 4613 67a726003cf8
parent 4545 4eadc8c2681b
child 4874 c66a42846887
equal deleted inserted replaced
4612:26764de50c74 4613:67a726003cf8
    75             val exh_tac = #exhaust_tac(datatype_info_sg sign tn)
    75             val exh_tac = #exhaust_tac(datatype_info_sg sign tn)
    76         in exh_tac aterm i end;
    76         in exh_tac aterm i end;
    77 
    77 
    78 end;
    78 end;
    79 
    79 
    80 
       
    81 (* should go into Pure *)
       
    82 fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
       
    83   (tac i THEN
       
    84    (fn st1 => st1 |> 
       
    85         let val d = nprems_of st1 - nprems_of st0
       
    86         in EVERY(map tacf ((i+d) downto i)) end));
       
    87 
    80 
    88 (*used for constructor parameters*)
    81 (*used for constructor parameters*)
    89 datatype dt_type = dtVar of string |
    82 datatype dt_type = dtVar of string |
    90   dtTyp of dt_type list * string |
    83   dtTyp of dt_type list * string |
    91   dtRek of dt_type list * string;
    84   dtRek of dt_type list * string;
   975        in Const(s', the (Sign.const_type sign s')) end
   968        in Const(s', the (Sign.const_type sign s')) end
   976      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
   969      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
   977      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
   970      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
   978      val exhaustion = mk_exhaust nchotomy
   971      val exhaustion = mk_exhaust nchotomy
   979      val exh_var = exhaust_var exhaustion;
   972      val exh_var = exhaust_var exhaustion;
   980      fun exhaust_tac a =
   973      fun exhaust_tac a =  (res_inst_tac [(exh_var,a)] exhaustion)
   981            ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
   974                           THEN_ALL_NEW (rotate_tac ~1);
   982                           (rotate_tac ~1);
       
   983      val induct_tac = Datatype.occs_in_prems itac 
   975      val induct_tac = Datatype.occs_in_prems itac 
   984  in
   976  in
   985   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
   977   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
   986         case_const = const (ty^"_case"),
   978         case_const = const (ty^"_case"),
   987         case_rewrites = map mk_rw case_rewrites,
   979         case_rewrites = map mk_rw case_rewrites,