src/HOL/Tools/datatype_package.ML
changeset 27104 791607529f6d
parent 27097 9a6db5d8ee8c
child 27130 4ba366056426
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 10 15:30:06 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 10 15:30:33 2008 +0200
     1.3 @@ -20,36 +20,25 @@
     1.4      -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a}
     1.5      -> (string * sort) list -> string list
     1.6      -> (string * (string * 'a list) list) list
     1.7 -  val induct_tac : string -> int -> tactic
     1.8 -  val induct_thm_tac : thm -> string -> int -> tactic
     1.9 +  val induct_tac : Proof.context -> string -> int -> tactic
    1.10 +  val induct_thm_tac : Proof.context -> thm -> string -> int -> tactic
    1.11    val case_tac : string -> int -> tactic
    1.12    val distinct_simproc : simproc
    1.13    val make_case :  Proof.context -> bool -> string list -> term ->
    1.14      (term * term) list -> term * (term * (int * bool)) list
    1.15    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    1.16    val interpretation : (string list -> theory -> theory) -> theory -> theory
    1.17 -  val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
    1.18 -    (thm list * attribute list) list list -> (thm list * attribute list) ->
    1.19 -    theory ->
    1.20 -      {distinct : thm list list,
    1.21 +  val rep_datatype : ({distinct : thm list list,
    1.22         inject : thm list list,
    1.23         exhaustion : thm list,
    1.24         rec_thms : thm list,
    1.25         case_thms : thm list list,
    1.26         split_thms : (thm * thm) list,
    1.27         induction : thm,
    1.28 -       simps : thm list} * theory
    1.29 -  val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list ->
    1.30 -    (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> theory ->
    1.31 -      {distinct : thm list list,
    1.32 -       inject : thm list list,
    1.33 -       exhaustion : thm list,
    1.34 -       rec_thms : thm list,
    1.35 -       case_thms : thm list list,
    1.36 -       split_thms : (thm * thm) list,
    1.37 -       induction : thm,
    1.38 -       simps : thm list} * theory
    1.39 -  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
    1.40 +       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
    1.41 +    -> theory -> Proof.state;
    1.42 +  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
    1.43 +  val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
    1.44      (bstring * typ list * mixfix) list) list -> theory ->
    1.45        {distinct : thm list list,
    1.46         inject : thm list list,
    1.47 @@ -59,7 +48,7 @@
    1.48         split_thms : (thm * thm) list,
    1.49         induction : thm,
    1.50         simps : thm list} * theory
    1.51 -  val add_datatype : bool -> string list -> (string list * bstring * mixfix *
    1.52 +  val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
    1.53      (bstring * string list * mixfix) list) list -> theory ->
    1.54        {distinct : thm list list,
    1.55         inject : thm list list,
    1.56 @@ -221,7 +210,7 @@
    1.57  
    1.58  in
    1.59  
    1.60 -fun gen_induct_tac inst_tac (varss, opt_rule) i state =
    1.61 +fun gen_induct_tac inst_tac ctxt (varss, opt_rule) i state =
    1.62    SUBGOAL (fn (Bi,_) =>
    1.63    let
    1.64      val (rule, rule_name) =
    1.65 @@ -230,7 +219,9 @@
    1.66          | NONE =>
    1.67              let val tn = find_tname (hd (map_filter I (flat varss))) Bi
    1.68                  val thy = Thm.theory_of_thm state
    1.69 -            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn)
    1.70 +            in case Induct.lookup_inductT ctxt tn of
    1.71 +                SOME thm => (thm, "Induction rule for type " ^ tn)
    1.72 +              | NONE => error ("No induction rule for type " ^ tn)
    1.73              end
    1.74      val concls = HOLogic.dest_concls (Thm.concl_of rule);
    1.75      val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    1.76 @@ -238,12 +229,12 @@
    1.77    in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
    1.78    i state;
    1.79  
    1.80 -fun induct_tac s =
    1.81 -  gen_induct_tac Tactic.res_inst_tac'
    1.82 +fun induct_tac ctxt s =
    1.83 +  gen_induct_tac Tactic.res_inst_tac' ctxt
    1.84      (map (single o SOME) (Syntax.read_idents s), NONE);
    1.85  
    1.86 -fun induct_thm_tac th s =
    1.87 -  gen_induct_tac Tactic.res_inst_tac'
    1.88 +fun induct_thm_tac ctxt th s =
    1.89 +  gen_induct_tac Tactic.res_inst_tac' ctxt
    1.90      ([map SOME (Syntax.read_idents s)], SOME th);
    1.91  
    1.92  end;
    1.93 @@ -284,7 +275,7 @@
    1.94  val inst_tac = RuleInsts.bires_inst_tac false;
    1.95  
    1.96  fun induct_meth ctxt (varss, opt_rule) =
    1.97 -  gen_induct_tac (inst_tac ctxt) (varss, opt_rule);
    1.98 +  gen_induct_tac (inst_tac ctxt) ctxt (varss, opt_rule);
    1.99  fun case_meth ctxt (varss, opt_rule) =
   1.100    gen_case_tac (inst_tac ctxt) (varss, opt_rule);
   1.101  
   1.102 @@ -545,57 +536,32 @@
   1.103  
   1.104  (*********************** declare existing type as datatype *********************)
   1.105  
   1.106 -fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
   1.107 +fun prove_rep_datatype alt_names new_type_names descr sorts induct inject distinct thy =
   1.108    let
   1.109 -    val (((distinct, inject), [induction]), thy1) =
   1.110 -      thy0
   1.111 -      |> fold_map apply_theorems raw_distinct
   1.112 -      ||>> fold_map apply_theorems raw_inject
   1.113 -      ||>> apply_theorems [raw_induction];
   1.114 -
   1.115 -    val ((_, [induction']), _) =
   1.116 -      Variable.importT_thms [induction] (Variable.thm_context induction);
   1.117 +    val ((_, [induct']), _) =
   1.118 +      Variable.importT_thms [induct] (Variable.thm_context induct);
   1.119  
   1.120      fun err t = error ("Ill-formed predicate in induction rule: " ^
   1.121 -      Syntax.string_of_term_global thy1 t);
   1.122 +      Syntax.string_of_term_global thy t);
   1.123  
   1.124      fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   1.125            ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
   1.126        | get_typ t = err t;
   1.127 -
   1.128 -    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));
   1.129 -    val new_type_names = getOpt (alt_names, map fst dtnames);
   1.130 +    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
   1.131  
   1.132 -    fun get_constr t = (case Logic.strip_assums_concl t of
   1.133 -        _ $ (_ $ t') => (case head_of t' of
   1.134 -            Const (cname, cT) => (case strip_type cT of
   1.135 -                (Ts, Type (tname, _)) => (tname, (cname, map (dtyp_of_typ dtnames) Ts))
   1.136 -              | _ => err t)
   1.137 -          | _ => err t)
   1.138 -      | _ => err t);
   1.139 -
   1.140 -    fun make_dt_spec [] _ _ = []
   1.141 -      | make_dt_spec ((tname, tvs)::dtnames') i constrs =
   1.142 -          let val (constrs', constrs'') = take_prefix (equal tname o fst) constrs
   1.143 -          in (i, (tname, map DtTFree tvs, map snd constrs'))::
   1.144 -            (make_dt_spec dtnames' (i + 1) constrs'')
   1.145 -          end;
   1.146 -
   1.147 -    val descr = make_dt_spec dtnames 0 (map get_constr (prems_of induction'));
   1.148 -    val sorts = add_term_tfrees (concl_of induction', []);
   1.149 -    val dt_info = get_datatypes thy1;
   1.150 +    val dt_info = get_datatypes thy;
   1.151  
   1.152      val (case_names_induct, case_names_exhausts) =
   1.153        (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
   1.154  
   1.155      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   1.156  
   1.157 -    val (casedist_thms, thy2) = thy1 |>
   1.158 -      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
   1.159 +    val (casedist_thms, thy2) = thy |>
   1.160 +      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
   1.161          case_names_exhausts;
   1.162      val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
   1.163        false new_type_names [descr] sorts dt_info inject distinct
   1.164 -      (Simplifier.theory_context thy2 dist_ss) induction thy2;
   1.165 +      (Simplifier.theory_context thy2 dist_ss) induct thy2;
   1.166      val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
   1.167        new_type_names [descr] sorts reccomb_names rec_thms thy3;
   1.168      val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
   1.169 @@ -607,14 +573,14 @@
   1.170      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   1.171        [descr] sorts thy7;
   1.172  
   1.173 -    val ((_, [induction']), thy10) =
   1.174 +    val ((_, [induct']), thy10) =
   1.175        thy8
   1.176        |> store_thmss "inject" new_type_names inject
   1.177        ||>> store_thmss "distinct" new_type_names distinct
   1.178        ||> Sign.add_path (space_implode "_" new_type_names)
   1.179 -      ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
   1.180 +      ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])];
   1.181  
   1.182 -    val dt_infos = map (make_dt_info alt_names descr sorts induction' reccomb_names rec_thms)
   1.183 +    val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
   1.184        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
   1.185          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   1.186  
   1.187 @@ -626,7 +592,7 @@
   1.188        |> add_rules simps case_thms rec_thms inject distinct
   1.189             weak_case_congs (Simplifier.attrib (op addcongs))
   1.190        |> put_dt_infos dt_infos
   1.191 -      |> add_cases_induct dt_infos induction'
   1.192 +      |> add_cases_induct dt_infos induct'
   1.193        |> Sign.parent_path
   1.194        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   1.195        |> snd
   1.196 @@ -638,12 +604,77 @@
   1.197        rec_thms = rec_thms,
   1.198        case_thms = case_thms,
   1.199        split_thms = split_thms,
   1.200 -      induction = induction',
   1.201 +      induction = induct',
   1.202        simps = simps}, thy11)
   1.203    end;
   1.204  
   1.205 -val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems;
   1.206 -val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i;
   1.207 +fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
   1.208 +  let
   1.209 +    fun constr_of_term (Const (c, T)) = (c, T)
   1.210 +      | constr_of_term t =
   1.211 +          error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   1.212 +    fun no_constr (c, T) = error ("Bad constructor: "
   1.213 +      ^ Sign.extern_const thy c ^ "::"
   1.214 +      ^ Syntax.string_of_typ_global thy T);
   1.215 +    fun type_of_constr (cT as (_, T)) =
   1.216 +      let
   1.217 +        val frees = typ_tfrees T;
   1.218 +        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
   1.219 +          handle TYPE _ => no_constr cT
   1.220 +        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
   1.221 +        val _ = if length frees <> length vs then no_constr cT else ();
   1.222 +      in (tyco, (vs, cT)) end;
   1.223 +
   1.224 +    val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
   1.225 +    val _ = case map_filter (fn (tyco, _) =>
   1.226 +        if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
   1.227 +     of [] => ()
   1.228 +      | tycos => error ("Type(s) " ^ commas (map quote tycos)
   1.229 +          ^ " already represented inductivly");
   1.230 +    val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
   1.231 +    val ms = case distinct (op =) (map length raw_vss)
   1.232 +     of [n] => 0 upto n - 1
   1.233 +      | _ => error ("Different types in given constructors");
   1.234 +    fun inter_sort m = map (fn xs => nth xs m) raw_vss
   1.235 +      |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   1.236 +    val sorts = map inter_sort ms;
   1.237 +    val vs = Name.names Name.context Name.aT sorts;
   1.238 +
   1.239 +    fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
   1.240 +      (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
   1.241 +
   1.242 +    val cs = map (apsnd (map norm_constr)) raw_cs;
   1.243 +    val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
   1.244 +      o fst o strip_type;
   1.245 +    val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names);
   1.246 +
   1.247 +    fun mk_spec (i, (tyco, constr)) = (i, (tyco,
   1.248 +      map (DtTFree o fst) vs,
   1.249 +      (map o apsnd) dtyps_of_typ constr))
   1.250 +    val descr = map_index mk_spec cs;
   1.251 +    val injs = DatatypeProp.make_injs [descr] vs;
   1.252 +    val distincts = map snd (DatatypeProp.make_distincts [descr] vs);
   1.253 +    val ind = DatatypeProp.make_ind [descr] vs;
   1.254 +    val rules = (map o map o map) Logic.close_form [[[ind]], injs, distincts];
   1.255 +
   1.256 +    fun after_qed' raw_thms =
   1.257 +      let
   1.258 +        val [[[induct]], injs, distincts] =
   1.259 +          unflat rules (map Drule.zero_var_indexes_list raw_thms);
   1.260 +            (*FIXME somehow dubious*)
   1.261 +      in
   1.262 +        ProofContext.theory_result
   1.263 +          (prove_rep_datatype alt_names new_type_names descr vs induct injs distincts)
   1.264 +        #-> after_qed
   1.265 +      end;
   1.266 +  in
   1.267 +    thy
   1.268 +    |> ProofContext.init
   1.269 +    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
   1.270 +  end;
   1.271 +
   1.272 +val rep_datatype = gen_rep_datatype Sign.cert_term;
   1.273 +val rep_datatype_cmd = gen_rep_datatype Sign.read_term (K I);
   1.274  
   1.275  
   1.276  
   1.277 @@ -719,8 +750,8 @@
   1.278        case_names_induct case_names_exhausts thy
   1.279    end;
   1.280  
   1.281 -val add_datatype_i = gen_add_datatype cert_typ;
   1.282 -val add_datatype = gen_add_datatype read_typ true;
   1.283 +val add_datatype = gen_add_datatype cert_typ;
   1.284 +val add_datatype_cmd = gen_add_datatype read_typ true;
   1.285  
   1.286  
   1.287  (** a datatype antiquotation **)
   1.288 @@ -786,8 +817,6 @@
   1.289  
   1.290  local structure P = OuterParse and K = OuterKeyword in
   1.291  
   1.292 -val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
   1.293 -
   1.294  val datatype_decl =
   1.295    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
   1.296      (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
   1.297 @@ -797,24 +826,17 @@
   1.298      val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
   1.299      val specs = map (fn ((((_, vs), t), mx), cons) =>
   1.300        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   1.301 -  in snd o add_datatype false names specs end;
   1.302 +  in snd o add_datatype_cmd false names specs end;
   1.303  
   1.304  val _ =
   1.305    OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   1.306      (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
   1.307  
   1.308 -
   1.309 -val rep_datatype_decl =
   1.310 -  Scan.option (Scan.repeat1 P.name) --
   1.311 -    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
   1.312 -    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
   1.313 -    (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
   1.314 -
   1.315 -fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
   1.316 -
   1.317  val _ =
   1.318 -  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
   1.319 -    (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
   1.320 +  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
   1.321 +    (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
   1.322 +      >> (fn (alt_names, ts) => Toplevel.print
   1.323 +           o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
   1.324  
   1.325  val _ =
   1.326    ThyOutput.add_commands [("datatype",
   1.327 @@ -822,6 +844,5 @@
   1.328  
   1.329  end;
   1.330  
   1.331 -
   1.332  end;
   1.333