--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Jul 24 12:50:06 1998 +0200
@@ -0,0 +1,557 @@
+(* Title: HOL/Tools/datatype_abs_proofs.ML
+ ID: $Id$
+ Author: Stefan Berghofer
+ Copyright 1998 TU Muenchen
+
+Proofs and defintions independent of concrete representation
+of datatypes (i.e. requiring only abstract properties such as
+injectivity / distinctness of constructors and induction)
+
+ - case distinction (exhaustion) theorems
+ - characteristic equations for primrec combinators
+ - characteristic equations for case combinators
+ - distinctness of constructors (external version)
+ - equations for splitting "P (case ...)" expressions
+ - datatype size function
+ - "nchotomy" and "case_cong" theorems for TFL
+
+*)
+
+signature DATATYPE_ABS_PROOFS =
+sig
+ val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ thm -> theory -> theory * thm list
+ val prove_primrec_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
+ thm -> theory -> theory * string list * thm list
+ val prove_case_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ string list -> thm list -> theory -> theory * string list * thm list list
+ val prove_distinctness_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ thm list list -> thm list list -> theory -> theory * thm list list
+ val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ thm list list -> thm list list -> thm list -> thm list list -> theory ->
+ theory * (thm * thm) list
+ val prove_size_thms : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ string list -> thm list -> theory -> theory * thm list
+ val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ thm list -> theory -> theory * thm list
+ val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ thm list -> thm list list -> theory -> theory * thm list
+end;
+
+structure DatatypeAbsProofs : DATATYPE_ABS_PROOFS =
+struct
+
+open DatatypeAux;
+
+val thin = read_instantiate_sg (sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
+
+val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
+
+(************************ case distinction theorems ***************************)
+
+fun prove_casedist_thms new_type_names descr sorts induct thy =
+ let
+ val _ = writeln "Proving case distinction theorems...";
+
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+
+ fun prove_casedist_thm ((i, t), T) =
+ let
+ val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
+ Abs ("z", T', Const ("True", T''))) induct_Ps;
+ val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", 0), T), Bound 0) $
+ Var (("P", 0), HOLogic.boolT))
+ val insts = take (i, dummyPs) @ (P::(drop (i + 1, dummyPs)));
+ val cert = cterm_of (sign_of thy);
+ val insts' = (map cert induct_Ps) ~~ (map cert insts);
+ val induct' = refl RS ((nth_elem (i,
+ split_conj_thm (cterm_instantiate insts' induct))) RSN (2, rev_mp))
+
+ in prove_goalw_cterm [] (cert t) (fn prems =>
+ [rtac induct' 1,
+ REPEAT (rtac TrueI 1),
+ REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
+ REPEAT (rtac TrueI 1)])
+ end;
+
+ val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
+ (DatatypeProp.make_casedists descr sorts) ~~ newTs)
+
+ in
+ (store_thms "exhaust" new_type_names casedist_thms thy, casedist_thms)
+ end;
+
+(*************************** primrec combinators ******************************)
+
+fun prove_primrec_thms new_type_names descr sorts
+ (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
+ let
+ val _ = writeln "Constructing primrec combinators...";
+
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
+
+ val big_rec_name' = (space_implode "_" new_type_names) ^ "_rec_set";
+ val rec_set_names = map (Sign.full_name (sign_of thy))
+ (if length descr' = 1 then [big_rec_name'] else
+ (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
+ (1 upto (length descr'))));
+
+ val rec_result_Ts = map (fn (i, _) =>
+ TFree ("'t" ^ (string_of_int (i + 1)), HOLogic.termS)) descr';
+
+ val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
+ map (fn (_, cargs) =>
+ let
+ val recs = filter is_rec_type cargs;
+ val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
+ (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+ in argTs ---> nth_elem (i, rec_result_Ts)
+ end) constrs) descr');
+
+ val rec_set_Ts = map (fn (T1, T2) => reccomb_fn_Ts ---> HOLogic.mk_setT
+ (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
+
+ val rec_fns = map (uncurry (mk_Free "f"))
+ (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
+ val rec_sets = map (fn c => list_comb (Const c, rec_fns))
+ (rec_set_names ~~ rec_set_Ts);
+
+ (* introduction rules for graph of primrec function *)
+
+ fun make_rec_intr T set_name ((rec_intr_ts, l), (cname, cargs)) =
+ let
+ fun mk_prem (dt, (j, k, prems, t1s, t2s)) =
+ let
+ val T = typ_of_dtyp descr' sorts dt;
+ val free1 = mk_Free "x" T j
+ in (case dt of
+ DtRec m =>
+ let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
+ in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
+ (HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
+ free1::t1s, free2::t2s)
+ end
+ | _ => (j + 1, k, prems, free1::t1s, t2s))
+ end;
+
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs, (1, 1, [], [], []))
+
+ in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
+ (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
+ list_comb (nth_elem (l, rec_fns), t1s @ t2s)), set_name)))], l + 1)
+ end;
+
+ val (rec_intr_ts, _) = foldl (fn (x, ((d, T), set_name)) =>
+ foldl (make_rec_intr T set_name) (x, #3 (snd d)))
+ (([], 0), descr' ~~ recTs ~~ rec_sets);
+
+ val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
+ InductivePackage.add_inductive_i false true big_rec_name' false false true
+ rec_sets rec_intr_ts [] [] thy;
+
+ (* prove uniqueness and termination of primrec combinators *)
+
+ val _ = writeln "Proving termination and uniqueness of primrec functions...";
+
+ fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
+ let
+ val distinct_tac = (etac Pair_inject 1) THEN
+ (if i < length newTs then
+ full_simp_tac (HOL_ss addsimps (nth_elem (i, dist_rewrites))) 1
+ else full_simp_tac (HOL_ss addsimps
+ ((#distinct (the (Symtab.lookup (dt_info, tname)))) @
+ [Suc_Suc_eq, Suc_not_Zero, Zero_not_Suc])) 1);
+
+ val inject = map (fn r => r RS iffD1)
+ (if i < length newTs then nth_elem (i, constr_inject)
+ else #inject (the (Symtab.lookup (dt_info, tname))));
+
+ fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
+ let
+ val k = length (filter is_rec_type cargs)
+
+ in (EVERY [DETERM tac,
+ REPEAT (etac ex1E 1), rtac ex1I 1,
+ DEPTH_SOLVE_1 (ares_tac [intr] 1),
+ REPEAT_DETERM_N k (etac thin 1),
+ etac elim 1,
+ REPEAT_DETERM_N j distinct_tac,
+ etac Pair_inject 1, TRY (dresolve_tac inject 1),
+ REPEAT (etac conjE 1), hyp_subst_tac 1,
+ REPEAT (etac allE 1),
+ REPEAT (dtac mp 1 THEN atac 1),
+ TRY (hyp_subst_tac 1),
+ rtac refl 1,
+ REPEAT_DETERM_N (n - j - 1) distinct_tac],
+ intrs, j + 1)
+ end;
+
+ val (tac', intrs', _) = foldl (mk_unique_constr_tac (length constrs))
+ ((tac, intrs, 0), constrs);
+
+ in (tac', intrs') end;
+
+ val rec_unique_thms =
+ let
+ val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
+ Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
+ absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod
+ (mk_Free "x" T1 i, Free ("y", T2)), set_t)))
+ (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
+ val cert = cterm_of (sign_of thy1)
+ val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
+ ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
+ val induct' = cterm_instantiate ((map cert induct_Ps) ~~
+ (map cert insts)) induct;
+ val (tac, _) = foldl mk_unique_tac
+ ((rtac induct' 1, rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+
+ in split_conj_thm (prove_goalw_cterm []
+ (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
+ end;
+
+ val rec_total_thms = map (fn r =>
+ r RS ex1_implies_ex RS (select_eq_Ex RS iffD2)) rec_unique_thms;
+
+ (* define primrec combinators *)
+
+ val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
+ val reccomb_names = map (Sign.full_name (sign_of thy1))
+ (if length descr' = 1 then [big_reccomb_name] else
+ (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
+ (1 upto (length descr'))));
+ val reccombs = map (fn ((name, T), T') => list_comb
+ (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+ (reccomb_names ~~ recTs ~~ rec_result_Ts);
+
+ val thy2 = thy1 |>
+ Theory.add_consts_i (map (fn ((name, T), T') =>
+ (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
+ (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
+ Theory.add_defs_i (map (fn ((((name, comb), set), T), T') =>
+ ((Sign.base_name name) ^ "_def", Logic.mk_equals
+ (comb $ Free ("x", T),
+ Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
+ HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))
+ (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
+
+ val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
+
+ (* prove characteristic equations for primrec combinators *)
+
+ val _ = writeln "Proving characteristic theorems for primrec combinators..."
+
+ val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
+ (cterm_of (sign_of thy2) t) (fn _ =>
+ [rtac select1_equality 1,
+ resolve_tac rec_unique_thms 1,
+ resolve_tac rec_intrs 1,
+ REPEAT (resolve_tac rec_total_thms 1)]))
+ (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
+
+ in
+ (PureThy.add_tthmss [(("recs", map Attribute.tthm_of rec_thms), [])] thy2,
+ reccomb_names, rec_thms)
+ end;
+
+(***************************** case combinators *******************************)
+
+fun prove_case_thms new_type_names descr sorts reccomb_names primrec_thms thy =
+ let
+ val _ = writeln "Proving characteristic theorems for case combinators...";
+
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val free = TFree ("'t", HOLogic.termS);
+ val Ts' = replicate (length (filter is_rec_type cargs)) free
+ in Const ("arbitrary", Ts @ Ts' ---> free)
+ end) constrs) descr';
+
+ val case_names = map (fn s =>
+ Sign.full_name (sign_of thy) (s ^ "_case")) new_type_names;
+
+ (* define case combinators via primrec combinators *)
+
+ val (case_defs, thy2) = foldl (fn ((defs, thy),
+ ((((i, (_, _, constrs)), T), name), recname)) =>
+ let
+ val T' = TFree ("'t", HOLogic.termS);
+
+ val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val Ts' = Ts @ (replicate (length (filter is_rec_type cargs)) T');
+ val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
+ val frees = take (length cargs, frees');
+ val free = mk_Free "f" (Ts ---> T') j
+ in
+ (free, list_abs_free (map dest_Free frees',
+ list_comb (free, frees)))
+ end) (constrs ~~ (1 upto length constrs)));
+
+ val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
+ val fns = (flat (take (i, case_dummy_fns))) @
+ fns2 @ (flat (drop (i + 1, case_dummy_fns)));
+ val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
+ val decl = (Sign.base_name name, caseT, NoSyn);
+ val def = ((Sign.base_name name) ^ "_def",
+ Logic.mk_equals (list_comb (Const (name, caseT), fns1),
+ list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
+ fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
+ val thy' = thy |>
+ Theory.add_consts_i [decl] |> Theory.add_defs_i [def];
+
+ in (defs @ [get_def thy' (Sign.base_name name)], thy')
+ end) (([], thy), (hd descr) ~~ newTs ~~ case_names ~~
+ (take (length newTs, reccomb_names)));
+
+ val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
+ (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
+ (fn _ => [rtac refl 1])))
+ (DatatypeProp.make_cases new_type_names descr sorts thy2);
+
+ val thy3 = Theory.add_trrules_i
+ (DatatypeProp.make_case_trrules new_type_names descr) thy2
+
+ in (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
+ end;
+
+(************************ distinctness of constructors ************************)
+
+fun prove_distinctness_thms new_type_names descr sorts dist_rewrites case_thms thy =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ (*--------------------------------------------------------------------*)
+ (* define t_ord - functions for proving distinctness of constructors: *)
+ (* t_ord C_i ... = i *)
+ (*--------------------------------------------------------------------*)
+
+ fun define_ord ((thy, ord_defs), (((_, (_, _, constrs)), T), tname)) =
+ if length constrs < DatatypeProp.dtK then (thy, ord_defs)
+ else
+ let
+ val Tss = map ((map (typ_of_dtyp descr' sorts)) o snd) constrs;
+ val ts = map HOLogic.mk_nat (0 upto length constrs - 1);
+ val mk_abs = foldr (fn (T, t') => Abs ("x", T, t'));
+ val fs = map mk_abs (Tss ~~ ts);
+ val fTs = map (fn Ts => Ts ---> HOLogic.natT) Tss;
+ val ord_name = Sign.full_name (sign_of thy) (tname ^ "_ord");
+ val case_name = Sign.intern_const (sign_of thy) (tname ^ "_case");
+ val ordT = T --> HOLogic.natT;
+ val caseT = fTs ---> ordT;
+ val defpair = (tname ^ "_ord_def", Logic.mk_equals
+ (Const (ord_name, ordT), list_comb (Const (case_name, caseT), fs)));
+ val thy' = thy |>
+ Theory.add_consts_i [(tname ^ "_ord", ordT, NoSyn)] |>
+ Theory.add_defs_i [defpair];
+ val def = get_def thy' (tname ^ "_ord")
+
+ in (thy', ord_defs @ [def]) end;
+
+ val (thy2, ord_defs) =
+ foldl define_ord ((thy, []), (hd descr) ~~ newTs ~~ new_type_names);
+
+ (**** number of constructors < dtK ****)
+
+ fun prove_distinct_thms _ [] = []
+ | prove_distinct_thms dist_rewrites' (t::_::ts) =
+ let
+ val dist_thm = prove_goalw_cterm [] (cterm_of (sign_of thy2) t) (fn _ =>
+ [simp_tac (HOL_ss addsimps dist_rewrites') 1])
+ in dist_thm::(standard (dist_thm RS not_sym))::
+ (prove_distinct_thms dist_rewrites' ts)
+ end;
+
+ val distinct_thms = map (fn ((((_, (_, _, constrs)), ts),
+ dist_rewrites'), case_thms) =>
+ if length constrs < DatatypeProp.dtK then
+ prove_distinct_thms dist_rewrites' ts
+ else
+ let
+ val t::ts' = rev ts;
+ val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
+ val cert = cterm_of (sign_of thy2);
+ val distinct_lemma' = cterm_instantiate
+ [(cert distinct_f, cert f)] distinct_lemma;
+ val rewrites = ord_defs @ (map mk_meta_eq case_thms)
+ in
+ (map (fn t => prove_goalw_cterm rewrites (cert t)
+ (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
+ end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
+ descr sorts thy2) ~~ dist_rewrites ~~ case_thms)
+
+ in (store_thmss "distinct" new_type_names distinct_thms thy2, distinct_thms)
+ end;
+
+(******************************* case splitting *******************************)
+
+fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
+ casedist_thms case_thms thy =
+ let
+ val _ = writeln "Proving equations for case splitting...";
+
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
+ exhaustion), case_thms'), T) =
+ let
+ val cert = cterm_of (sign_of thy);
+ val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
+ val exhaustion' = cterm_instantiate
+ [(cert lhs, cert (Free ("x", T)))] exhaustion;
+ val tacsf = K [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
+ (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]
+ in
+ (prove_goalw_cterm [] (cert t1) tacsf,
+ prove_goalw_cterm [] (cert t2) tacsf)
+ end;
+
+ val split_thm_pairs = map prove_split_thms
+ ((DatatypeProp.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
+ dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
+
+ val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
+
+ in
+ (thy |> store_thms "split" new_type_names split_thms |>
+ store_thms "split_asm" new_type_names split_asm_thms,
+ split_thm_pairs)
+ end;
+
+(******************************* size functions *******************************)
+
+fun prove_size_thms new_type_names descr sorts reccomb_names primrec_thms thy =
+ let
+ val _ = writeln "Proving equations for size function...";
+
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+
+ val big_size_name = space_implode "_" new_type_names ^ "_size";
+ val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy))) "size";
+ val size_names = replicate (length (hd descr)) size_name @
+ map (Sign.full_name (sign_of thy))
+ (if length (flat (tl descr)) = 1 then [big_size_name] else
+ map (fn i => big_size_name ^ "_" ^ string_of_int i)
+ (1 upto length (flat (tl descr))));
+ val def_names = map (fn i => big_size_name ^ "_def_" ^ string_of_int i)
+ (1 upto length recTs);
+
+ val plus_t = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT);
+
+ fun make_sizefun (_, cargs) =
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val k = length (filter is_rec_type cargs);
+ val t = if k = 0 then HOLogic.zero else
+ foldl1 (app plus_t) (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
+ in
+ foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
+ end;
+
+ val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
+ val fTs = map fastype_of fs;
+
+ val thy' = thy |>
+ Theory.add_consts_i (map (fn (s, T) =>
+ (Sign.base_name s, T --> HOLogic.natT, NoSyn))
+ (drop (length (hd descr), size_names ~~ recTs))) |>
+ Theory.add_defs_i (map (fn (((s, T), def_name), rec_name) =>
+ (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
+ list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
+ (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
+
+ val size_def_thms = map (get_axiom thy') def_names;
+ val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
+
+ val size_thms = map (fn t => prove_goalw_cterm rewrites
+ (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1]))
+ (DatatypeProp.make_size new_type_names descr sorts thy')
+
+ in
+ (PureThy.add_tthmss [(("size", map Attribute.tthm_of size_thms), [])] thy',
+ size_thms)
+ end;
+
+(************************* additional theorems for TFL ************************)
+
+fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
+ let
+ val _ = writeln "Proving additional theorems for TFL...";
+
+ fun prove_nchotomy (t, exhaustion) =
+ let
+ (* For goal i, select the correct disjunct to attack, then prove it *)
+ fun tac i 0 = EVERY [TRY (rtac disjI1 i),
+ hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
+ | tac i n = rtac disjI2 i THEN tac i (n - 1)
+ in
+ prove_goalw_cterm [] (cterm_of (sign_of thy) t) (fn _ =>
+ [rtac allI 1,
+ exh_tac (K exhaustion) 1,
+ ALLGOALS (fn i => tac i (i-1))])
+ end;
+
+ val nchotomys =
+ map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms)
+
+ in
+ (store_thms "nchotomy" new_type_names nchotomys thy, nchotomys)
+ end;
+
+fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
+ let
+ fun prove_case_cong ((t, nchotomy), case_rewrites) =
+ let
+ val (Const ("==>", _) $ tm $ _) = t;
+ val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
+ val cert = cterm_of (sign_of thy);
+ val nchotomy' = nchotomy RS spec;
+ val nchotomy'' = cterm_instantiate
+ [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
+ in
+ prove_goalw_cterm [] (cert t) (fn prems =>
+ let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
+ in [simp_tac (HOL_ss addsimps [hd prems]) 1,
+ cut_facts_tac [nchotomy''] 1,
+ REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
+ REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
+ end)
+ end;
+
+ val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
+ new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
+
+ in
+ (store_thms "case_cong" new_type_names case_congs thy, case_congs)
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_aux.ML Fri Jul 24 12:50:06 1998 +0200
@@ -0,0 +1,269 @@
+(* Title: HOL/Tools/datatype_aux.ML
+ ID: $Id$
+ Author: Stefan Berghofer
+ Copyright 1998 TU Muenchen
+
+Auxiliary functions for defining datatypes
+*)
+
+signature DATATYPE_AUX =
+sig
+ val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
+
+ val get_thy : string -> theory -> theory option
+
+ val store_thmss : string -> string list -> thm list list -> theory -> theory
+ val store_thms : string -> string list -> thm list -> theory -> theory
+
+ val split_conj_thm : thm -> thm list
+ val mk_conj : term list -> term
+ val mk_disj : term list -> term
+
+ val indtac : thm -> int -> tactic
+ val exh_tac : (string -> thm) -> int -> tactic
+
+ datatype dtyp =
+ DtTFree of string
+ | DtType of string * (dtyp list)
+ | DtRec of int;
+
+ type datatype_info
+
+ val dtyp_of_typ : (string * string list) list -> typ -> dtyp
+ val mk_Free : string -> typ -> int -> term
+ val is_rec_type : dtyp -> bool
+ val typ_of_dtyp : (int * (string * dtyp list *
+ (string * dtyp list) list)) list -> (string * sort) list -> dtyp -> typ
+ val dest_DtTFree : dtyp -> string
+ val dest_DtRec : dtyp -> int
+ val dest_TFree : typ -> string
+ val dest_conj : term -> term list
+ val get_nonrec_types : (int * (string * dtyp list *
+ (string * dtyp list) list)) list -> (string * sort) list -> typ list
+ val get_rec_types : (int * (string * dtyp list *
+ (string * dtyp list) list)) list -> (string * sort) list -> typ list
+ val check_nonempty : (int * (string * dtyp list *
+ (string * dtyp list) list)) list list -> unit
+ val unfold_datatypes :
+ datatype_info Symtab.table ->
+ (int * (string * dtyp list *
+ (string * dtyp list) list)) list -> int ->
+ (int * (string * dtyp list *
+ (string * dtyp list) list)) list list * int
+end;
+
+structure DatatypeAux : DATATYPE_AUX =
+struct
+
+(* FIXME: move to library ? *)
+fun foldl1 f (x::xs) = foldl f (x, xs);
+
+fun get_thy name thy = find_first
+ (equal name o Sign.name_of o sign_of) (ancestors_of thy);
+
+(* store theorems in theory *)
+
+fun store_thmss label tnames thmss thy =
+ foldr (fn ((tname, thms), thy') => thy' |>
+ (if length tnames = 1 then I else Theory.add_path tname) |>
+ PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
+ (if length tnames = 1 then I else Theory.parent_path))
+ (tnames ~~ thmss, thy);
+
+fun store_thms label tnames thms thy =
+ foldr (fn ((tname, thm), thy') => thy' |>
+ (if length tnames = 1 then I else Theory.add_path tname) |>
+ PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
+ (if length tnames = 1 then I else Theory.parent_path))
+ (tnames ~~ thms, thy);
+
+(* split theorem thm_1 & ... & thm_n into n theorems *)
+
+fun split_conj_thm th =
+ ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle _ => [th];
+
+val mk_conj = foldr1 (HOLogic.mk_binop "op &");
+val mk_disj = foldr1 (HOLogic.mk_binop "op |");
+
+fun dest_conj (Const ("op &", _) $ t $ t') = t::(dest_conj t')
+ | dest_conj t = [t];
+
+(* instantiate induction rule *)
+
+fun indtac indrule i st =
+ let
+ val ts = dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
+ val ts' = dest_conj (HOLogic.dest_Trueprop
+ (Logic.strip_imp_concl (nth_elem (i - 1, prems_of st))));
+ val getP = if can HOLogic.dest_imp (hd ts) then
+ (apfst Some) o HOLogic.dest_imp else pair None;
+ fun abstr (t1, t2) = (case t1 of
+ None => let val [Free (s, T)] = add_term_frees (t2, [])
+ in absfree (s, T, t2) end
+ | Some (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
+ val cert = cterm_of (sign_of_thm st);
+ val Ps = map (cert o head_of o snd o getP) ts;
+ val indrule' = cterm_instantiate (Ps ~~
+ (map (cert o abstr o getP) ts')) indrule
+ in
+ rtac indrule' i st
+ end;
+
+(* perform exhaustive case analysis on last parameter of subgoal i *)
+
+fun exh_tac exh_thm_of i state =
+ let
+ val sg = sign_of_thm state;
+ val prem = nth_elem (i - 1, prems_of state);
+ val params = Logic.strip_params prem;
+ val (_, Type (tname, _)) = hd (rev params);
+ val exhaustion = lift_rule (state, i) (exh_thm_of tname);
+ val prem' = hd (prems_of exhaustion);
+ val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
+ val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
+ cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
+ (params, Bound 0)))] exhaustion
+ in compose_tac (false, exhaustion', nprems_of exhaustion) i state
+ end;
+
+(********************** Internal description of datatypes *********************)
+
+datatype dtyp =
+ DtTFree of string
+ | DtType of string * (dtyp list)
+ | DtRec of int;
+
+(* information about datatypes *)
+
+type datatype_info =
+ {index : int,
+ descr : (int * (string * dtyp list *
+ (string * dtyp list) list)) list,
+ rec_names : string list,
+ rec_rewrites : thm list,
+ case_name : string,
+ case_rewrites : thm list,
+ induction : thm,
+ exhaustion : thm,
+ distinct : thm list,
+ inject : thm list,
+ nchotomy : thm,
+ case_cong : thm};
+
+fun mk_Free s T i = Free (s ^ (string_of_int i), T);
+
+fun subst_DtTFree _ substs (T as (DtTFree name)) =
+ (case assoc (substs, name) of
+ None => T
+ | Some U => U)
+ | subst_DtTFree i substs (DtType (name, ts)) =
+ DtType (name, map (subst_DtTFree i substs) ts)
+ | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
+
+fun dest_DtTFree (DtTFree a) = a;
+fun dest_DtRec (DtRec i) = i;
+
+fun is_rec_type (DtType (_, dts)) = exists is_rec_type dts
+ | is_rec_type (DtRec _) = true
+ | is_rec_type _ = false;
+
+fun dest_TFree (TFree (n, _)) = n;
+
+fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
+ | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
+ | dtyp_of_typ new_dts (Type (tname, Ts)) =
+ (case assoc (new_dts, tname) of
+ None => DtType (tname, map (dtyp_of_typ new_dts) Ts)
+ | Some vs => if map (try dest_TFree) Ts = map Some vs then
+ DtRec (find_index (curry op = tname o fst) new_dts)
+ else error ("Illegal occurence of recursive type " ^ tname));
+
+fun typ_of_dtyp descr sorts (DtTFree a) = TFree (a, the (assoc (sorts, a)))
+ | typ_of_dtyp descr sorts (DtRec i) =
+ let val (s, ds, _) = the (assoc (descr, i))
+ in Type (s, map (typ_of_dtyp descr sorts) ds) end
+ | typ_of_dtyp descr sorts (DtType (s, ds)) =
+ Type (s, map (typ_of_dtyp descr sorts) ds);
+
+(* find all non-recursive types in datatype description *)
+
+fun get_nonrec_types descr sorts =
+ let fun add (Ts, T as DtTFree _) = T ins Ts
+ | add (Ts, T as DtType _) = T ins Ts
+ | add (Ts, _) = Ts
+ in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+ foldl (fn (Ts', (_, cargs)) =>
+ foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
+ end;
+
+(* get all recursive types in datatype description *)
+
+fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
+ Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
+
+(* nonemptiness check for datatypes *)
+
+fun check_nonempty descr =
+ let
+ val descr' = flat descr;
+ fun is_nonempty_dt is i =
+ let
+ val (_, _, constrs) = the (assoc (descr', i));
+ fun arg_nonempty (DtRec i) = if i mem is then false
+ else is_nonempty_dt (i::is) i
+ | arg_nonempty _ = true;
+ in exists ((forall arg_nonempty) o snd) constrs
+ end
+ in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
+ (fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
+ end;
+
+(* unfold a list of mutually recursive datatype specifications *)
+(* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
+(* need to be unfolded *)
+
+fun unfold_datatypes (dt_info : datatype_info Symtab.table) descr i =
+ let
+ fun get_dt_descr i tname dts =
+ (case Symtab.lookup (dt_info, tname) of
+ None => error (tname ^ " is not a datatype - can't use it in\
+ \ indirect recursion")
+ | (Some {index, descr, ...}) =>
+ let val (_, vars, _) = the (assoc (descr, index));
+ val subst = ((map dest_DtTFree vars) ~~ dts) handle _ =>
+ error ("Type constructor " ^ tname ^ " used with wrong\
+ \ number of arguments")
+ in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
+ (tn, map (subst_DtTFree i subst) args,
+ map (apsnd (map (subst_DtTFree i subst))) cs))) descr)
+ end);
+
+ (* unfold a single constructor argument *)
+
+ fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
+ if is_rec_type T then
+ let val (index, descr) = get_dt_descr i tname dts;
+ val (descr', i') = unfold_datatypes dt_info descr (i + length descr)
+ in (i', Ts @ [DtRec index], descrs @ descr') end
+ else (i, Ts @ [T], descrs)
+ | unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
+
+ (* unfold a constructor *)
+
+ fun unfold_constr ((i, constrs, descrs), (cname, cargs)) =
+ let val (i', cargs', descrs') = foldl unfold_arg ((i, [], descrs), cargs)
+ in (i', constrs @ [(cname, cargs')], descrs') end;
+
+ (* unfold a single datatype *)
+
+ fun unfold_datatype ((i, dtypes, descrs), (j, (tname, tvars, constrs))) =
+ let val (i', constrs', descrs') =
+ foldl unfold_constr ((i, [], descrs), constrs)
+ in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs')
+ end;
+
+ val (i', descr', descrs) = foldl unfold_datatype ((i, [],[]), descr);
+
+ in (descr' :: descrs, i') end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_package.ML Fri Jul 24 12:50:06 1998 +0200
@@ -0,0 +1,622 @@
+(* Title: HOL/Tools/datatype_package.ML
+ ID: $Id$
+ Author: Stefan Berghofer
+ Copyright 1998 TU Muenchen
+
+Datatype package for Isabelle/HOL
+*)
+
+signature DATATYPE_PACKAGE =
+sig
+ val add_datatype : string list -> (string list * bstring * mixfix *
+ (bstring * mixfix * string list) list) list -> theory -> theory *
+ {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ size : thm list,
+ simps : thm list}
+ val add_datatype_i : string list -> (string list * bstring * mixfix *
+ (bstring * mixfix * typ list) list) list -> theory -> theory *
+ {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ size : thm list,
+ simps : thm list}
+ val add_rep_datatype : string list option -> thm list list ->
+ thm list list -> thm -> theory -> theory *
+ {distinct : thm list list,
+ inject : thm list list,
+ exhaustion : thm list,
+ rec_thms : thm list,
+ case_thms : thm list list,
+ split_thms : (thm * thm) list,
+ induction : thm,
+ size : thm list,
+ simps : thm list}
+ val setup: (theory -> theory) list
+ val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
+ val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info
+ val datatype_info : theory -> string -> DatatypeAux.datatype_info
+ val constrs_of : theory -> string -> term list option
+ val case_const_of : theory -> string -> term option
+ val mutual_induct_tac : string list -> int -> tactic
+ val induct_tac : string -> int -> tactic
+ val exhaust_tac : string -> int -> tactic
+end;
+
+structure DatatypePackage : DATATYPE_PACKAGE =
+struct
+
+open DatatypeAux;
+
+(* data kind 'HOL/datatypes' *)
+
+structure DatatypesArgs =
+struct
+ val name = "HOL/datatypes";
+ type T = datatype_info Symtab.table;
+
+ val empty = Symtab.empty;
+ val prep_ext = I;
+ val merge: T * T -> T = Symtab.merge (K true);
+
+ fun print sg tab =
+ Pretty.writeln (Pretty.strs ("datatypes:" ::
+ map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+end;
+
+structure DatatypesData = TheoryDataFun(DatatypesArgs);
+val get_datatypes_sg = DatatypesData.get_sg;
+val get_datatypes = DatatypesData.get;
+val put_datatypes = DatatypesData.put;
+
+(* setup *)
+
+val setup = [DatatypesData.init];
+
+(** theory information about datatypes **)
+
+fun datatype_info_sg sg name =
+ (case Symtab.lookup (get_datatypes_sg sg, name) of
+ Some info => info
+ | None => error ("Unknown datatype " ^ quote name));
+
+val datatype_info = datatype_info_sg o sign_of;
+
+fun constrs_of thy tname =
+ let
+ val {index, descr, ...} = datatype_info thy tname;
+ val (_, _, constrs) = the (assoc (descr, index))
+ in
+ Some (map (fn (cname, _) =>
+ Const (cname, the (Sign.const_type (sign_of thy) cname))) constrs)
+ end handle _ => None;
+
+fun case_const_of thy tname =
+ let
+ val {case_name, ...} = datatype_info thy tname;
+ in
+ Some (Const (case_name, the (Sign.const_type (sign_of thy) case_name)))
+ end handle _ => None;
+
+fun find_tname var Bi =
+ let val frees = map dest_Free (term_frees Bi)
+ val params = Logic.strip_params Bi;
+ in case assoc (frees @ params, var) of
+ None => error ("No such variable in subgoal: " ^ quote var)
+ | Some(Type (tn, _)) => tn
+ | _ => error ("Cannot determine type of " ^ quote var)
+ end;
+
+fun infer_tname state sign i aterm =
+ let
+ val (_, _, Bi, _) = dest_state (state, i)
+ val params = Logic.strip_params Bi; (*params of subgoal i*)
+ val params = rev (rename_wrt_term Bi params); (*as they are printed*)
+ val (types, sorts) = types_sorts state;
+ fun types' (a, ~1) = (case assoc (params, a) of None => types(a, ~1) | sm => sm)
+ | types' ixn = types ixn;
+ val (ct, _) = read_def_cterm (sign, types', sorts) [] false
+ (aterm, TVar (("", 0), []));
+ in case #T (rep_cterm ct) of
+ Type (tn, _) => tn
+ | _ => error ("Cannot determine type of " ^ quote aterm)
+ end;
+
+(*Warn if the (induction) variable occurs Free among the premises, which
+ usually signals a mistake. But calls the tactic either way!*)
+fun occs_in_prems tacf vars =
+ SUBGOAL (fn (Bi, i) =>
+ (if exists (fn Free (a, _) => a mem vars)
+ (foldr add_term_frees (#2 (strip_context Bi), []))
+ then warning "Induction variable occurs also among premises!"
+ else ();
+ tacf i));
+
+(* generic induction tactic for datatypes *)
+
+fun mutual_induct_tac vars i state =
+ let
+ val (_, _, Bi, _) = dest_state (state, i);
+ val {sign, ...} = rep_thm state;
+ val tn = find_tname (hd vars) Bi;
+ val {induction, ...} = datatype_info_sg sign tn;
+ val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
+ implode (tl (explode (Syntax.string_of_vname ixn))))
+ (dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
+ val insts = (ind_vnames ~~ vars) handle _ =>
+ error ("Induction rule for type " ^ tn ^ " has different number of variables")
+ in
+ occs_in_prems (res_inst_tac insts induction) vars i state
+ end;
+
+fun induct_tac var = mutual_induct_tac [var];
+
+(* generic exhaustion tactic for datatypes *)
+
+fun exhaust_tac aterm i state =
+ let
+ val {sign, ...} = rep_thm state;
+ val tn = infer_tname state sign i aterm;
+ val {exhaustion, ...} = datatype_info_sg sign tn;
+ val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
+ (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
+ val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
+ in
+ res_inst_tac [(exh_vname, aterm)] exhaustion i state
+ end;
+
+
+(* prepare types *)
+
+fun read_typ sign ((Ts, sorts), str) =
+ let
+ val T = Type.no_tvars (Sign.read_typ (sign, (curry assoc)
+ (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
+ in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
+
+fun cert_typ sign ((Ts, sorts), raw_T) =
+ let
+ val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
+ TYPE (msg, _, _) => error msg;
+ val sorts' = add_typ_tfrees (T, sorts)
+ in (Ts @ [T],
+ case duplicates (map fst sorts') of
+ [] => sorts'
+ | dups => error ("Inconsistent sort constraints for " ^ commas dups))
+ end;
+
+
+(**** make datatype info ****)
+
+fun make_dt_info descr induct reccomb_names rec_thms
+ ((((((((i, (_, (tname, _, _))), case_name), case_thms),
+ exhaustion_thm), distinct_thm), inject), nchotomy), case_cong) = (tname,
+ {index = i,
+ descr = descr,
+ rec_names = reccomb_names,
+ rec_rewrites = rec_thms,
+ case_name = case_name,
+ case_rewrites = case_thms,
+ induction = induct,
+ exhaustion = exhaustion_thm,
+ distinct = distinct_thm,
+ inject = inject,
+ nchotomy = nchotomy,
+ case_cong = case_cong});
+
+fun store_clasimp thy (cla, simp) =
+ (claset_ref_of thy := cla; simpset_ref_of thy := simp);
+
+infix 4 addDistinct;
+
+fun clasimp addDistinct ([], _) = clasimp
+ | clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
+ if length constrs < DatatypeProp.dtK then
+ clasimp addIffs thms addDistinct (thmss, descr)
+ else
+ clasimp addsimps2 thms addDistinct (thmss, descr);
+
+
+(********************* axiomatic introduction of datatypes ********************)
+
+fun add_and_get_axioms label tnames ts thy =
+ foldr (fn ((tname, t), (thy', axs)) =>
+ let
+ val thy'' = thy' |>
+ (if length tnames = 1 then I else Theory.add_path tname) |>
+ PureThy.add_axioms_i [((label, t), [])];
+ val ax = get_axiom thy'' label
+ in (if length tnames = 1 then thy'' else Theory.parent_path thy'', ax::axs)
+ end) (tnames ~~ ts, (thy, []));
+
+fun add_and_get_axiomss label tnames tss thy =
+ foldr (fn ((tname, ts), (thy', axss)) =>
+ let
+ val thy'' = thy' |>
+ (if length tnames = 1 then I else Theory.add_path tname) |>
+ PureThy.add_axiomss_i [((label, ts), [])];
+ val axs = PureThy.get_thms thy'' label
+ in (if length tnames = 1 then thy'' else Theory.parent_path thy'', axs::axss)
+ end) (tnames ~~ tss, (thy, []));
+
+fun add_datatype_axm new_type_names descr sorts types_syntax constr_syntax dt_info thy =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ val _ = writeln ("Adding axioms for datatype(s) " ^ commas new_type_names);
+
+ (**** declare new types and constants ****)
+
+ val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
+
+ val constr_decls = map (fn (((_, (_, _, constrs)), T), constr_syntax') =>
+ map (fn ((_, cargs), (cname, mx)) =>
+ (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
+ (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
+
+ val rec_result_Ts = map (fn (i, _) =>
+ TFree ("'t" ^ (string_of_int (i + 1)), HOLogic.termS)) descr';
+
+ val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
+ map (fn (_, cargs) =>
+ let
+ val recs = filter is_rec_type cargs;
+ val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
+ (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+ in argTs ---> nth_elem (i, rec_result_Ts)
+ end) constrs) descr');
+
+ val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
+ val reccomb_names = if length descr' = 1 then [big_reccomb_name] else
+ (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
+ (1 upto (length descr')));
+
+ val big_size_name = space_implode "_" new_type_names ^ "_size";
+ val size_names = if length (flat (tl descr)) = 1 then [big_size_name] else
+ map (fn i => big_size_name ^ "_" ^ string_of_int i)
+ (1 upto length (flat (tl descr)));
+
+ val freeT = TFree ("'t", HOLogic.termS);
+ val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
+ map (fn (_, cargs) =>
+ let val Ts = map (typ_of_dtyp descr' sorts) cargs
+ in Ts ---> freeT end) constrs) (hd descr);
+
+ val case_names = map (fn s => (s ^ "_case")) new_type_names;
+
+ val thy2 = thy |>
+
+ Theory.add_path (space_implode "_" new_type_names) |>
+
+ (** new types **)
+
+ curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
+ PureThy.add_typedecls [(name, tvs, mx)] |>
+ Theory.add_arities_i
+ [(Sign.full_name (sign_of thy') (Syntax.type_name name mx),
+ replicate (length tvs) HOLogic.termS, HOLogic.termS)]))
+ (types_syntax ~~ tyvars) |>
+
+ (** constructors **)
+
+ curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
+ constr_syntax'), thy') => thy' |>
+ (if length newTs = 1 then I else Theory.add_path tname) |>
+ Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
+ (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
+ (constrs ~~ constr_syntax')) |>
+ (if length newTs = 1 then I else Theory.parent_path)))
+ (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax) |>
+
+ (** primrec combinators **)
+
+ Theory.add_consts_i (map (fn ((name, T), T') =>
+ (name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
+ (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
+
+ (** case combinators **)
+
+ Theory.add_consts_i (map (fn ((name, T), Ts) =>
+ (name, Ts @ [T] ---> freeT, NoSyn))
+ (case_names ~~ newTs ~~ case_fn_Ts)) |>
+ Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr) |>
+
+ (** t_ord functions **)
+
+ Theory.add_consts_i
+ (foldr (fn ((((_, (_, _, constrs)), tname), T), decls) =>
+ if length constrs < DatatypeProp.dtK then decls
+ else (tname ^ "_ord", T --> HOLogic.natT, NoSyn)::decls)
+ ((hd descr) ~~ new_type_names ~~ newTs, [])) |>
+
+ (** size functions **)
+
+ Theory.add_consts_i (map (fn (s, T) =>
+ (Sign.base_name s, T --> HOLogic.natT, NoSyn))
+ (size_names ~~ drop (length (hd descr), recTs)));
+
+ (**** introduction of axioms ****)
+
+ val (thy3, inject) = thy2 |>
+ Theory.add_path (space_implode "_" new_type_names) |>
+ PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
+ add_and_get_axiomss "inject" new_type_names
+ (DatatypeProp.make_injs descr sorts);
+ val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
+ (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
+ val induct = get_axiom thy4 "induct";
+
+ val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
+ (DatatypeProp.make_casedists descr sorts) (PureThy.add_axiomss_i [(("recs",
+ DatatypeProp.make_primrecs new_type_names descr sorts thy4), [])] thy4);
+ val rec_thms = get_thms thy5 "recs";
+ val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
+ (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
+ val (split_ts, split_asm_ts) = ListPair.unzip
+ (DatatypeProp.make_splits new_type_names descr sorts thy6);
+ val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
+ val (thy8, split_asm) = add_and_get_axioms "split_asm" new_type_names
+ split_asm_ts thy7;
+ val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
+ (DatatypeProp.make_nchotomys descr sorts) thy8;
+ val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
+ (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
+ val thy11 = PureThy.add_axiomss_i [(("size",
+ DatatypeProp.make_size new_type_names descr sorts thy10), [])] thy10;
+ val size_thms = get_thms thy11 "size";
+
+ val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
+ ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
+ exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+
+ val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
+
+ val thy12 = thy11 |>
+ PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
+ put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
+ Theory.parent_path;
+
+ val _ = store_clasimp thy12 ((claset_of thy12, simpset_of thy12)
+ addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
+ addIffs flat inject addDistinct (distinct, hd descr));
+
+ in
+ (thy12,
+ {distinct = distinct,
+ inject = inject,
+ exhaustion = exhaustion,
+ rec_thms = rec_thms,
+ case_thms = case_thms,
+ split_thms = split ~~ split_asm,
+ induction = induct,
+ size = size_thms,
+ simps = simps})
+ end;
+
+
+(******************* definitional introduction of datatypes *******************)
+
+fun add_datatype_def new_type_names descr sorts types_syntax constr_syntax dt_info thy =
+ let
+ val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
+
+ val (thy2, inject, dist_rewrites, induct) = thy |>
+ Theory.add_path (space_implode "_" new_type_names) |>
+ DatatypeRepProofs.representation_proofs dt_info new_type_names descr sorts
+ types_syntax constr_syntax;
+
+ val (thy3, casedist_thms) =
+ DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
+ val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
+ new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
+ val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
+ new_type_names descr sorts reccomb_names rec_thms thy4;
+ val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
+ new_type_names descr sorts dist_rewrites case_thms thy5;
+ val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
+ descr sorts inject dist_rewrites casedist_thms case_thms thy6;
+ val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ descr sorts casedist_thms thy7;
+ val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
+ descr sorts nchotomys case_thms thy8;
+ val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms new_type_names
+ descr sorts reccomb_names rec_thms thy9;
+
+ val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
+ ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
+ casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+
+ val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
+
+ val thy11 = thy10 |>
+ PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
+ put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
+ Theory.parent_path;
+
+ val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
+ addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
+ addIffs flat inject addDistinct (distinct, hd descr));
+
+ in
+ (thy11,
+ {distinct = distinct,
+ inject = inject,
+ exhaustion = casedist_thms,
+ rec_thms = rec_thms,
+ case_thms = case_thms,
+ split_thms = split_thms,
+ induction = induct,
+ size = size_thms,
+ simps = simps})
+ end;
+
+
+(*********************** declare non-datatype as datatype *********************)
+
+fun add_rep_datatype alt_names distinct inject induction thy =
+ let
+ val sign = sign_of thy;
+
+ val induction' = freezeT induction;
+
+ fun err t = error ("Ill-formed predicate in induction rule: " ^
+ Sign.string_of_term sign t);
+
+ fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
+ ((tname, map dest_TFree Ts) handle _ => err t)
+ | get_typ t = err t;
+
+ val dtnames = map get_typ (dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
+ val new_type_names = if_none alt_names (map fst dtnames);
+
+ fun get_constr t = (case Logic.strip_assums_concl t of
+ _ $ (_ $ t') => (case head_of t' of
+ Const (cname, cT) => (case strip_type cT of
+ (Ts, Type (tname, _)) => (tname, (cname, map (dtyp_of_typ dtnames) Ts))
+ | _ => err t)
+ | _ => err t)
+ | _ => err t);
+
+ fun make_dt_spec [] _ _ = []
+ | make_dt_spec ((tname, tvs)::dtnames') i constrs =
+ let val (constrs', constrs'') = take_prefix (equal tname o fst) constrs
+ in (i, (tname, map DtTFree tvs, map snd constrs'))::
+ (make_dt_spec dtnames' (i + 1) constrs'')
+ end;
+
+ val descr = make_dt_spec dtnames 0 (map get_constr (prems_of induction'));
+ val sorts = add_term_tfrees (concl_of induction', []);
+ val dt_info = get_datatypes thy;
+
+ val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
+
+ val (thy2, casedist_thms) = thy |>
+ Theory.add_path (space_implode "_" new_type_names) |>
+ DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
+ val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
+ new_type_names [descr] sorts dt_info inject distinct induction thy2;
+ val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
+ new_type_names [descr] sorts reccomb_names rec_thms thy3;
+ val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
+ new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
+ val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ [descr] sorts casedist_thms thy5;
+ val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
+ [descr] sorts nchotomys case_thms thy6;
+ val (thy8, size_thms) =
+ if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
+ DatatypeAbsProofs.prove_size_thms new_type_names
+ [descr] sorts reccomb_names rec_thms thy7
+ else (thy7, []);
+
+ val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
+ ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
+ casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+
+ val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
+
+ val thy9 = thy8 |>
+ PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
+ put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
+ Theory.parent_path;
+
+ val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
+ addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
+ addIffs flat inject addDistinct (distinct, descr));
+
+ in
+ (thy9,
+ {distinct = distinct,
+ inject = inject,
+ exhaustion = casedist_thms,
+ rec_thms = rec_thms,
+ case_thms = case_thms,
+ split_thms = split_thms,
+ induction = induction,
+ size = size_thms,
+ simps = simps})
+ end;
+
+
+(******************************** add datatype ********************************)
+
+fun gen_add_datatype prep_typ new_type_names dts thy =
+ let
+ val _ = Theory.requires thy "Datatype" "datatype definitions";
+
+ (* this theory is used just for parsing *)
+
+ val tmp_thy = thy |>
+ Theory.prep_ext |>
+ Theory.add_path (space_implode "_" new_type_names) |>
+ Theory.add_types (map (fn (tvs, tname, mx, _) =>
+ (tname, length tvs, mx)) dts);
+
+ val sign = sign_of tmp_thy;
+
+ val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
+ let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
+ in (case duplicates tvs of
+ [] => ((full_tname, tvs), (tname, mx))
+ | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
+ " : " ^ commas dups))
+ end) dts);
+
+ val _ = (case duplicates (map fst new_dts) @ duplicates new_type_names of
+ [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
+
+ fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
+ let
+ fun prep_constr ((constrs, constr_syntax', sorts'), (cname, mx', cargs)) =
+ let val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs)
+ in (constrs @ [((if length dts = 1 then Sign.full_name sign
+ else Sign.full_name_path sign (Sign.base_name tname))
+ (Syntax.const_name cname mx'),
+ map (dtyp_of_typ new_dts) cargs')],
+ constr_syntax' @ [(cname, mx')], sorts'')
+ end handle ERROR =>
+ error ("The error above occured in constructor " ^ cname ^
+ " of datatype " ^ tname);
+
+ val (constrs', constr_syntax', sorts') =
+ foldl prep_constr (([], [], sorts), constrs)
+
+ in
+ case duplicates (map fst constrs') of
+ [] =>
+ (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
+ map DtTFree tvs, constrs'))],
+ constr_syntax @ [constr_syntax'], sorts', i + 1)
+ | dups => error ("Duplicate constructors " ^ commas dups ^
+ " in datatype " ^ tname)
+ end;
+
+ val (dts', constr_syntax, sorts, i) = foldl prep_dt_spec (([], [], [], 0), dts);
+ val dt_info = get_datatypes thy;
+ val (descr, _) = unfold_datatypes dt_info dts' i;
+ val _ = check_nonempty descr;
+
+ in
+ (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
+ new_type_names descr sorts types_syntax constr_syntax dt_info thy
+ end;
+
+val add_datatype_i = gen_add_datatype cert_typ;
+val add_datatype = gen_add_datatype read_typ;
+
+end;
+
+val induct_tac = DatatypePackage.induct_tac;
+val mutual_induct_tac = DatatypePackage.mutual_induct_tac;
+val exhaust_tac = DatatypePackage.exhaust_tac;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_prop.ML Fri Jul 24 12:50:06 1998 +0200
@@ -0,0 +1,513 @@
+(* Title: HOL/Tools/datatype_prop.ML
+ ID: $Id$
+ Author: Stefan Berghofer
+ Copyright 1998 TU Muenchen
+
+Characteristic properties of datatypes
+*)
+
+signature DATATYPE_PROP =
+sig
+ val dtK : int
+ val make_injs : (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ term list list
+ val make_ind : (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
+ val make_casedists : (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
+ val make_primrecs : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ theory -> term list
+ val make_cases : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ theory -> term list list
+ val make_distincts : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ theory -> term list list
+ val make_splits : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ theory -> (term * term) list
+ val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
+ val make_size : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ theory -> term list
+ val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ theory -> term list
+ val make_nchotomys : (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
+end;
+
+structure DatatypeProp : DATATYPE_PROP =
+struct
+
+open DatatypeAux;
+
+(*the kind of distinctiveness axioms depends on number of constructors*)
+val dtK = 7;
+
+fun make_tnames Ts =
+ let
+ fun type_name (TFree (name, _)) = implode (tl (explode name))
+ | type_name (Type (name, _)) =
+ let val name' = Sign.base_name name
+ in if Syntax.is_identifier name' then name' else "x"
+ end;
+
+ fun index_vnames (vn::vns) tab =
+ (case assoc (tab, vn) of
+ None => if vn mem vns
+ then (vn ^ "1") :: index_vnames vns ((vn, 2)::tab)
+ else vn :: index_vnames vns tab
+ | Some i => (vn ^ (string_of_int i))::
+ index_vnames vns ((vn, i + 1)::tab))
+ | index_vnames [] _ = []
+
+ in index_vnames (map type_name Ts) []
+ end;
+
+(** FIXME: move to hologic.ML ? **)
+val Not = Const ("Not", HOLogic.boolT --> HOLogic.boolT);
+
+(************************* injectivity of constructors ************************)
+
+fun make_injs descr sorts =
+ let
+ val descr' = flat descr;
+
+ fun make_inj T ((cname, cargs), injs) =
+ if null cargs then injs else
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val constr_t = Const (cname, Ts ---> T);
+ val tnames = make_tnames Ts;
+ val frees = map Free (tnames ~~ Ts);
+ val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
+ in (HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
+ foldr1 (HOLogic.mk_binop "op &")
+ (map HOLogic.mk_eq (frees ~~ frees')))))::injs
+ end;
+
+ in map (fn (d, T) => foldr (make_inj T) (#3 (snd d), []))
+ ((hd descr) ~~ take (length (hd descr), get_rec_types descr' sorts))
+ end;
+
+(********************************* induction **********************************)
+
+fun make_ind descr sorts =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val pnames = if length descr' = 1 then ["P"]
+ else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
+
+ fun make_pred i T =
+ let val T' = T --> HOLogic.boolT
+ in Free (nth_elem (i, pnames), T') end;
+
+ fun make_ind_prem k T (cname, cargs) =
+ let
+ val recs = filter is_rec_type cargs;
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val recTs' = map (typ_of_dtyp descr' sorts) recs;
+ val tnames = variantlist (make_tnames Ts, pnames);
+ val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+ val frees = tnames ~~ Ts;
+ val prems = map (fn ((r, s), T) => HOLogic.mk_Trueprop
+ (make_pred (dest_DtRec r) T $ Free (s, T))) (recs ~~ rec_tnames ~~ recTs');
+
+ in list_all_free (frees, Logic.list_implies (prems,
+ HOLogic.mk_Trueprop (make_pred k T $
+ list_comb (Const (cname, Ts ---> T), map Free frees))))
+ end;
+
+ val prems = flat (map (fn ((i, (_, _, constrs)), T) =>
+ map (make_ind_prem i T) constrs) (descr' ~~ recTs));
+ val tnames = make_tnames recTs;
+ val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+ (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
+ (descr' ~~ recTs ~~ tnames)))
+
+ in Logic.list_implies (prems, concl) end;
+
+(******************************* case distinction *****************************)
+
+fun make_casedists descr sorts =
+ let
+ val descr' = flat descr;
+
+ fun make_casedist_prem T (cname, cargs) =
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val frees = variantlist (make_tnames Ts, ["P", "y"]) ~~ Ts;
+ val free_ts = map Free frees
+ in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
+ HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
+ end;
+
+ fun make_casedist ((_, (_, _, constrs)), T) =
+ let val prems = map (make_casedist_prem T) constrs
+ in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
+ end
+
+ in map make_casedist
+ ((hd descr) ~~ take (length (hd descr), get_rec_types descr' sorts))
+ end;
+
+(*************** characteristic equations for primrec combinator **************)
+
+fun make_primrecs new_type_names descr sorts thy =
+ let
+ val sign = sign_of thy;
+
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+
+ val rec_result_Ts = map (fn (i, _) =>
+ TFree ("'t" ^ (string_of_int (i + 1)), HOLogic.termS)) descr';
+
+ val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
+ map (fn (_, cargs) =>
+ let
+ val recs = filter is_rec_type cargs;
+ val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
+ (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+ in argTs ---> nth_elem (i, rec_result_Ts)
+ end) constrs) descr');
+
+ val rec_fns = map (uncurry (mk_Free "f"))
+ (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
+
+ val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
+ val reccomb_names = map (Sign.intern_const sign)
+ (if length descr' = 1 then [big_reccomb_name] else
+ (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
+ (1 upto (length descr'))));
+ val reccombs = map (fn ((name, T), T') => list_comb
+ (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+ (reccomb_names ~~ recTs ~~ rec_result_Ts);
+
+ fun make_primrec T comb_t ((ts, f::fs), (cname, cargs)) =
+ let
+ val recs = filter is_rec_type cargs;
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val recTs' = map (typ_of_dtyp descr' sorts) recs;
+ val tnames = make_tnames Ts;
+ val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+ val frees = map Free (tnames ~~ Ts);
+ val frees' = map Free (rec_tnames ~~ recTs');
+ val reccombs' = map (fn (DtRec i) => nth_elem (i, reccombs)) recs
+
+ in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
+ list_comb (f, frees @ (map (uncurry ap) (reccombs' ~~ frees')))))], fs)
+ end
+
+ in fst (foldl (fn (x, ((dt, T), comb_t)) =>
+ foldl (make_primrec T comb_t) (x, #3 (snd dt)))
+ (([], rec_fns), descr' ~~ recTs ~~ reccombs))
+ end;
+
+(****************** make terms of form t_case f1 ... fn *********************)
+
+fun make_case_combs new_type_names descr sorts thy fname =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+ val T' = TFree ("'t", HOLogic.termS);
+
+ val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
+ map (fn (_, cargs) =>
+ let val Ts = map (typ_of_dtyp descr' sorts) cargs
+ in Ts ---> T' end) constrs) (hd descr);
+
+ val case_names = map (fn s =>
+ Sign.intern_const (sign_of thy) (s ^ "_case")) new_type_names
+ in
+ map (fn ((name, Ts), T) => list_comb
+ (Const (name, Ts @ [T] ---> T'),
+ map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
+ (case_names ~~ case_fn_Ts ~~ newTs)
+ end;
+
+(**************** characteristic equations for case combinator ****************)
+
+fun make_cases new_type_names descr sorts thy =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ fun make_case T comb_t ((cname, cargs), f) =
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val frees = map Free ((make_tnames Ts) ~~ Ts)
+ in HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
+ list_comb (f, frees)))
+ end
+
+ in map (fn (((_, (_, _, constrs)), T), comb_t) =>
+ map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
+ ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
+ end;
+
+(************************* distinctness of constructors ***********************)
+
+fun make_distincts new_type_names descr sorts thy =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ (**** number of constructors < dtK : C_i ... ~= C_j ... ****)
+
+ fun make_distincts_1 _ [] = []
+ | make_distincts_1 T ((cname, cargs)::constrs) =
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val frees = map Free ((make_tnames Ts) ~~ Ts);
+ val t = list_comb (Const (cname, Ts ---> T), frees);
+
+ fun make_distincts' [] = []
+ | make_distincts' ((cname', cargs')::constrs') =
+ let
+ val Ts' = map (typ_of_dtyp descr' sorts) cargs';
+ val frees' = map Free ((map ((op ^) o (rpair "'"))
+ (make_tnames Ts')) ~~ Ts');
+ val t' = list_comb (Const (cname', Ts' ---> T), frees')
+ in
+ (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq (t, t')))::
+ (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq (t', t)))::
+ (make_distincts' constrs')
+ end
+
+ in (make_distincts' constrs) @ (make_distincts_1 T constrs)
+ end;
+
+ (**** number of constructors >= dtK : t_ord C_i ... = i ****)
+
+ fun make_distincts_2 T tname i constrs =
+ let
+ val ord_name = Sign.intern_const (sign_of thy) (tname ^ "_ord");
+ val ord_t = Const (ord_name, T --> HOLogic.natT)
+
+ in (case constrs of
+ [] => [Logic.mk_implies (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
+ (ord_t $ Free ("x", T), ord_t $ Free ("y", T))),
+ HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
+ (Free ("x", T), Free ("y", T))))]
+ | ((cname, cargs)::constrs) =>
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val frees = map Free ((make_tnames Ts) ~~ Ts);
+ in
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (ord_t $
+ list_comb (Const (cname, Ts ---> T), frees), HOLogic.mk_nat i)))::
+ (make_distincts_2 T tname (i + 1) constrs)
+ end)
+ end;
+
+ in map (fn (((_, (_, _, constrs)), T), tname) =>
+ if length constrs < dtK then make_distincts_1 T constrs
+ else make_distincts_2 T tname 0 constrs)
+ ((hd descr) ~~ newTs ~~ new_type_names)
+ end;
+
+(*************************** the "split" - equations **************************)
+
+fun make_splits new_type_names descr sorts thy =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+ val T' = TFree ("'t", HOLogic.termS);
+ val P = Free ("P", T' --> HOLogic.boolT);
+
+ fun make_split (((_, (_, _, constrs)), T), comb_t) =
+ let
+ val (_, fs) = strip_comb comb_t;
+ val used = ["P", "x"] @ (map (fst o dest_Free) fs);
+
+ fun process_constr (((cname, cargs), f), (t1s, t2s)) =
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val frees = map Free (variantlist (make_tnames Ts, used) ~~ Ts);
+ val eqn = HOLogic.mk_eq (Free ("x", T),
+ list_comb (Const (cname, Ts ---> T), frees));
+ val P' = P $ list_comb (f, frees)
+ in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
+ (frees, HOLogic.imp $ eqn $ P'))::t1s,
+ (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
+ (frees, HOLogic.conj $ eqn $ (Not $ P')))::t2s)
+ end;
+
+ val (t1s, t2s) = foldr process_constr (constrs ~~ fs, ([], []));
+ val lhs = P $ (comb_t $ Free ("x", T))
+ in
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, Not $ mk_disj t2s)))
+ end
+
+ in map make_split ((hd descr) ~~ newTs ~~
+ (make_case_combs new_type_names descr sorts thy "f"))
+ end;
+
+(************************ translation rules for case **************************)
+
+fun make_case_trrules new_type_names descr =
+ let
+ fun mk_asts i j ((cname, cargs)::constrs) =
+ let
+ val k = length cargs;
+ val xs = map (fn i => Variable ("x" ^ string_of_int i)) (i upto i + k - 1);
+ val t = Variable ("t" ^ string_of_int j);
+ val ast = Ast.mk_appl (Constant "@case1")
+ [Ast.mk_appl (Constant (Sign.base_name cname)) xs, t];
+ val ast' = foldr (fn (x, y) =>
+ Ast.mk_appl (Constant "_abs") [x, y]) (xs, t)
+ in
+ (case constrs of
+ [] => (ast, [ast'])
+ | cs => let val (ast'', asts) = mk_asts (i + k) (j + 1) cs
+ in (Ast.mk_appl (Constant "@case2") [ast, ast''],
+ ast'::asts)
+ end)
+ end;
+
+ fun mk_trrule ((_, (_, _, constrs)), tname) =
+ let val (ast, asts) = mk_asts 1 1 constrs
+ in Syntax.ParsePrintRule
+ (Ast.mk_appl (Constant "@case") [Variable "t", ast],
+ Ast.mk_appl (Constant (tname ^ "_case"))
+ (asts @ [Variable "t"]))
+ end
+
+ in
+ map mk_trrule (hd descr ~~ new_type_names)
+ end;
+
+(******************************* size functions *******************************)
+
+fun make_size new_type_names descr sorts thy =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+
+ val big_size_name = space_implode "_" new_type_names ^ "_size";
+ val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy))) "size";
+ val size_names = replicate (length (hd descr)) size_name @
+ map (Sign.intern_const (sign_of thy))
+ (if length (flat (tl descr)) = 1 then [big_size_name] else
+ map (fn i => big_size_name ^ "_" ^ string_of_int i)
+ (1 upto length (flat (tl descr))));
+ val size_consts = map (fn (s, T) =>
+ Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
+
+ val plus_t = Const ("op +", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT);
+
+ fun make_size_eqn size_const T (cname, cargs) =
+ let
+ val recs = filter is_rec_type cargs;
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val recTs = map (typ_of_dtyp descr' sorts) recs;
+ val tnames = make_tnames Ts;
+ val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
+ val ts = map (fn ((r, s), T) => nth_elem (dest_DtRec r, size_consts) $
+ Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
+ val t = if ts = [] then HOLogic.zero else
+ foldl1 (app plus_t) (ts @ [HOLogic.mk_nat 1])
+ in
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
+ list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))
+ end
+
+ in
+ flat (map (fn (((_, (_, _, constrs)), size_const), T) =>
+ map (make_size_eqn size_const T) constrs) (descr' ~~ size_consts ~~ recTs))
+ end;
+
+(************************* additional rules for TFL ***************************)
+
+(*---------------------------------------------------------------------------
+ * Structure of case congruence theorem looks like this:
+ *
+ * (M = M')
+ * ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk))
+ * ==> ...
+ * ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj))
+ * ==>
+ * (ty_case f1..fn M = ty_case g1..gn M')
+ *---------------------------------------------------------------------------*)
+
+fun make_case_congs new_type_names descr sorts thy =
+ let
+ val case_combs = make_case_combs new_type_names descr sorts thy "f";
+ val case_combs' = make_case_combs new_type_names descr sorts thy "g";
+
+ fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
+ let
+ val Type ("fun", [T, _]) = fastype_of comb;
+ val (_, fs) = strip_comb comb;
+ val (_, gs) = strip_comb comb';
+ val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs);
+ val M = Free ("M", T);
+ val M' = Free ("M'", T);
+
+ fun mk_clause ((f, g), (cname, _)) =
+ let
+ val (Ts, _) = strip_type (fastype_of f);
+ val tnames = variantlist (make_tnames Ts, used);
+ val frees = map Free (tnames ~~ Ts)
+ in
+ list_all_free (tnames ~~ Ts, Logic.mk_implies
+ (HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
+ HOLogic.mk_Trueprop
+ (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
+ end
+
+ in
+ Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::
+ map mk_clause (fs ~~ gs ~~ constrs),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb' $ M')))
+ end
+
+ in
+ map mk_case_cong (case_combs ~~ case_combs' ~~ hd descr)
+ end;
+
+(*---------------------------------------------------------------------------
+ * Structure of exhaustion theorem looks like this:
+ *
+ * !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)
+ *---------------------------------------------------------------------------*)
+
+fun make_nchotomys descr sorts =
+ let
+ val descr' = flat descr;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+
+ fun mk_eqn T (cname, cargs) =
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) cargs;
+ val tnames = variantlist (make_tnames Ts, ["v"]);
+ val frees = tnames ~~ Ts
+ in
+ foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
+ (frees, HOLogic.mk_eq (Free ("v", T),
+ list_comb (Const (cname, Ts ---> T), map Free frees)))
+ end
+
+ in map (fn ((_, (_, _, constrs)), T) =>
+ HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, mk_disj (map (mk_eqn T) constrs))))
+ (hd descr ~~ newTs)
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Jul 24 12:50:06 1998 +0200
@@ -0,0 +1,542 @@
+(* Title: HOL/Tools/datatype_rep_proofs.ML
+ ID: $Id$
+ Author: Stefan Berghofer
+ Copyright 1998 TU Muenchen
+
+Definitional introduction of datatypes
+Proof of characteristic theorems:
+
+ - injectivity of constructors
+ - distinctness of constructors (internal version)
+ - induction theorem
+
+*)
+
+signature DATATYPE_REP_PROOFS =
+sig
+ val representation_proofs : DatatypeAux.datatype_info Symtab.table ->
+ string list -> (int * (string * DatatypeAux.dtyp list *
+ (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ (string * mixfix) list -> (string * mixfix) list list -> theory ->
+ theory * thm list list * thm list list * thm
+end;
+
+structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
+struct
+
+open DatatypeAux;
+
+val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
+
+(* figure out internal names *)
+
+val image_name = Sign.intern_const (sign_of Set.thy) "op ``";
+val UNIV_name = Sign.intern_const (sign_of Set.thy) "UNIV";
+val inj_name = Sign.intern_const (sign_of Fun.thy) "inj";
+val inj_on_name = Sign.intern_const (sign_of Fun.thy) "inj_on";
+val inv_name = Sign.intern_const (sign_of Fun.thy) "inv";
+
+fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
+ #exhaustion (the (Symtab.lookup (dt_info, tname)));
+
+(******************************************************************************)
+
+(*----------------------------------------------------------*)
+(* Proofs dependent on concrete representation of datatypes *)
+(* *)
+(* - injectivity of constructors *)
+(* - distinctness of constructors (internal version) *)
+(* - induction theorem *)
+(*----------------------------------------------------------*)
+
+fun representation_proofs (dt_info : datatype_info Symtab.table)
+ new_type_names descr sorts types_syntax constr_syntax thy =
+ let
+ val Univ_thy = the (get_thy "Univ" thy);
+ val node_name = Sign.intern_tycon (sign_of Univ_thy) "node";
+ val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name] =
+ map (Sign.intern_const (sign_of Univ_thy))
+ ["In0", "In1", "Scons", "Leaf", "Numb"];
+ val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
+ In0_not_In1, In1_not_In0] = map (get_thm Univ_thy)
+ ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq",
+ "In1_eq", "In0_not_In1", "In1_not_In0"];
+
+ val descr' = flat descr;
+
+ val big_rec_name = (space_implode "_" new_type_names) ^ "_rep_set";
+ val rep_set_names = map (Sign.full_name (sign_of thy))
+ (if length descr' = 1 then [big_rec_name] else
+ (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
+ (1 upto (length descr'))));
+
+ val leafTs = get_nonrec_types descr' sorts;
+ val recTs = get_rec_types descr' sorts;
+ val newTs = take (length (hd descr), recTs);
+ val oldTs = drop (length (hd descr), recTs);
+ val sumT = if null leafTs then HOLogic.unitT
+ else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
+ val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT]));
+ val UnivT = HOLogic.mk_setT Univ_elT;
+
+ val In0 = Const (In0_name, Univ_elT --> Univ_elT);
+ val In1 = Const (In1_name, Univ_elT --> Univ_elT);
+ val Leaf = Const (Leaf_name, sumT --> Univ_elT);
+
+ (* make injections needed for embedding types in leaves *)
+
+ fun mk_inj T' x =
+ let
+ fun mk_inj' T n i =
+ if n = 1 then x else
+ let val n2 = n div 2;
+ val Type (_, [T1, T2]) = T
+ in
+ if i <= n2 then
+ Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
+ else
+ Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
+ end
+ in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
+ end;
+
+ (* make injections for constructors *)
+
+ fun mk_univ_inj ts = access_bal (ap In0, ap In1, if ts = [] then
+ Const ("arbitrary", Univ_elT)
+ else
+ foldr1 (HOLogic.mk_binop Scons_name) ts);
+
+ (************** generate introduction rules for representing set **********)
+
+ val _ = writeln "Constructing representing sets...";
+
+ (* make introduction rule for a single constructor *)
+
+ fun make_intr s n (i, (_, cargs)) =
+ let
+ fun mk_prem (DtRec k, (j, prems, ts)) =
+ let val free_t = mk_Free "x" Univ_elT j
+ in (j + 1, (HOLogic.mk_mem (free_t,
+ Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
+ end
+ | mk_prem (dt, (j, prems, ts)) =
+ let val T = typ_of_dtyp descr' sorts dt
+ in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
+ end;
+
+ val (_, prems, ts) = foldr mk_prem (cargs, (1, [], []));
+ val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
+ (mk_univ_inj ts n i, Const (s, UnivT)))
+ in Logic.list_implies (map HOLogic.mk_Trueprop prems, concl)
+ end;
+
+ val consts = map (fn s => Const (s, UnivT)) rep_set_names;
+
+ val intr_ts = flat (map (fn ((_, (_, _, constrs)), rep_set_name) =>
+ map (make_intr rep_set_name (length constrs))
+ ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names));
+
+ val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
+ InductivePackage.add_inductive_i false true big_rec_name false true false
+ consts intr_ts [] [] thy;
+
+ (********************************* typedef ********************************)
+
+ val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
+
+ val thy3 = foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
+ TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
+ (Some (BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) thy)
+ (thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
+ new_type_names);
+
+ (*********************** definition of constructors ***********************)
+
+ val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_";
+ val rep_names = map (curry op ^ "Rep_") new_type_names;
+ val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
+ (1 upto (length (flat (tl descr))));
+ val all_rep_names = map (Sign.full_name (sign_of thy3)) (rep_names @ rep_names');
+
+ (* isomorphism declarations *)
+
+ val iso_decls = map (fn (T, s) => (s, T --> Univ_elT, NoSyn))
+ (oldTs ~~ rep_names');
+
+ (* constructor definitions *)
+
+ fun make_constr_def tname T n ((thy, defs, eqns, i), ((cname, cargs), (cname', mx))) =
+ let
+ fun constr_arg (dt, (j, l_args, r_args)) =
+ let val T = typ_of_dtyp descr' sorts dt;
+ val free_t = mk_Free "x" T j
+ in (case dt of
+ DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
+ T --> Univ_elT) $ free_t)::r_args)
+ | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
+ end;
+
+ val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], []));
+ val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
+ val abs_name = Sign.intern_const (sign_of thy) ("Abs_" ^ tname);
+ val rep_name = Sign.intern_const (sign_of thy) ("Rep_" ^ tname);
+ val lhs = list_comb (Const (cname, constrT), l_args);
+ val rhs = mk_univ_inj r_args n i;
+ val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
+ val def_name = (Sign.base_name cname) ^ "_def";
+ val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
+ val thy' = thy |>
+ Theory.add_consts_i [(cname', constrT, mx)] |>
+ Theory.add_defs_i [(def_name, def)];
+
+ in (thy', defs @ [get_axiom thy' def_name], eqns @ [eqn], i + 1)
+ end;
+
+ (* constructor definitions for datatype *)
+
+ fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas),
+ ((((_, (_, _, constrs)), tname), T), constr_syntax)) =
+ let
+ val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
+ val sg = sign_of thy;
+ val rep_const = cterm_of sg
+ (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
+ val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
+ val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
+ val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
+ ((if length newTs = 1 then thy else Theory.add_path tname thy, defs, [], 1),
+ constrs ~~ constr_syntax)
+ in
+ (if length newTs = 1 then thy' else Theory.parent_path thy', defs', eqns @ [eqns'],
+ rep_congs @ [cong'], dist_lemmas @ [dist])
+ end;
+
+ val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs
+ ((Theory.add_consts_i iso_decls thy3, [], [], [], []),
+ hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
+
+ (*********** isomorphisms for new types (introduced by typedef) ***********)
+
+ val _ = writeln "Proving isomorphism properties...";
+
+ (* get axioms from theory *)
+
+ val newT_iso_axms = map (fn s =>
+ (get_axiom thy4 ("Abs_" ^ s ^ "_inverse"),
+ get_axiom thy4 ("Rep_" ^ s ^ "_inverse"),
+ get_axiom thy4 ("Rep_" ^ s))) new_type_names;
+
+ (*------------------------------------------------*)
+ (* prove additional theorems: *)
+ (* inj_on dt_Abs_i rep_set_i and inj dt_Rep_i *)
+ (*------------------------------------------------*)
+
+ fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) =
+ let
+ val sg = sign_of thy4;
+ val RepT = T --> Univ_elT;
+ val Rep_name = Sign.intern_const sg ("Rep_" ^ s);
+ val AbsT = Univ_elT --> T;
+ val Abs_name = Sign.intern_const sg ("Abs_" ^ s);
+
+ val inj_on_Abs_thm = prove_goalw_cterm [] (cterm_of sg
+ (HOLogic.mk_Trueprop (Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $
+ Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
+ (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]);
+
+ val inj_Rep_thm = prove_goalw_cterm [] (cterm_of sg
+ (HOLogic.mk_Trueprop (Const (inj_name, RepT --> HOLogic.boolT) $
+ Const (Rep_name, RepT))))
+ (fn _ => [rtac inj_inverseI 1, rtac thm2 1])
+
+ in (inj_on_Abs_thm, inj_Rep_thm) end;
+
+ val newT_iso_inj_thms = map prove_newT_iso_inj_thm
+ (new_type_names ~~ newT_iso_axms ~~ newTs ~~
+ take (length newTs, rep_set_names));
+
+ (********* isomorphisms between existing types and "unfolded" types *******)
+
+ (*---------------------------------------------------------------------*)
+ (* isomorphisms are defined using primrec-combinators: *)
+ (* generate appropriate functions for instantiating primrec-combinator *)
+ (* *)
+ (* e.g. dt_Rep_i = list_rec ... (%h t y. In1 ((Leaf h) $ y)) *)
+ (* *)
+ (* also generate characteristic equations for isomorphisms *)
+ (* *)
+ (* e.g. dt_Rep_i (cons h t) = In1 ((dt_Rep_j h) $ (dt_Rep_i t)) *)
+ (*---------------------------------------------------------------------*)
+
+ fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
+ let
+ val argTs = map (typ_of_dtyp descr' sorts) cargs;
+ val T = nth_elem (k, recTs);
+ val rep_name = nth_elem (k, all_rep_names);
+ val rep_const = Const (rep_name, T --> Univ_elT);
+ val constr = Const (cname, argTs ---> T);
+
+ fun process_arg ks' ((i2, i2', ts), dt) =
+ let val T' = typ_of_dtyp descr' sorts dt
+ in (case dt of
+ DtRec j => if j mem ks' then
+ (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'])
+ else
+ (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
+ T' --> Univ_elT) $ mk_Free "x" T' i2])
+ | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)]))
+ end;
+
+ val (i2, i2', ts) = foldl (process_arg ks) ((1, 1, []), cargs);
+ val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
+ val ys = map (mk_Free "y" Univ_elT) (1 upto (i2' - 1));
+ val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
+
+ val (_, _, ts') = foldl (process_arg []) ((1, 1, []), cargs);
+ val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
+
+ in (fs @ [f], eqns @ [eqn], i + 1) end;
+
+ (* define isomorphisms for all mutually recursive datatypes in list ds *)
+
+ fun make_iso_defs (ds, (thy, char_thms)) =
+ let
+ val ks = map fst ds;
+ val (_, (tname, _, _)) = hd ds;
+ val {rec_rewrites, rec_names, ...} = the (Symtab.lookup (dt_info, tname));
+
+ fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
+ let
+ val (fs', eqns', _) = foldl (make_iso_def k ks (length constrs))
+ ((fs, eqns, 1), constrs);
+ val iso = (nth_elem (k, recTs), nth_elem (k, all_rep_names))
+ in (fs', eqns', isos @ [iso]) end;
+
+ val (fs, eqns, isos) = foldl process_dt (([], [], []), ds);
+ val fTs = map fastype_of fs;
+ val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
+ equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
+ list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
+ val thy' = Theory.add_defs_i defs thy;
+ val def_thms = map (get_axiom thy') (map fst defs);
+
+ (* prove characteristic equations *)
+
+ val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
+ val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
+ (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
+
+ in (thy', char_thms' @ char_thms) end;
+
+ val (thy5, iso_char_thms) = foldr make_iso_defs (tl descr, (thy4, []));
+
+ (* prove isomorphism properties *)
+
+ (* prove x : dt_rep_set_i --> x : range dt_Rep_i *)
+
+ fun mk_iso_t (((set_name, iso_name), i), T) =
+ let val isoT = T --> Univ_elT
+ in HOLogic.imp $
+ HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $
+ (if i < length newTs then Const ("True", HOLogic.boolT)
+ else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
+ Const (image_name, [isoT, HOLogic.mk_setT T] ---> UnivT) $
+ Const (iso_name, isoT) $ Const (UNIV_name, HOLogic.mk_setT T)))
+ end;
+
+ val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
+ (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
+
+ val newT_Abs_inverse_thms = map (fn (iso, _, _) => iso RS subst) newT_iso_axms;
+
+ (* all the theorems are proved by one single simultaneous induction *)
+
+ val iso_thms = if length descr = 1 then [] else
+ drop (length newTs, split_conj_thm
+ (prove_goalw_cterm [] (cterm_of (sign_of thy5) iso_t) (fn _ =>
+ [indtac rep_induct 1,
+ REPEAT (rtac TrueI 1),
+ REPEAT (EVERY
+ [REPEAT (etac rangeE 1),
+ REPEAT (eresolve_tac newT_Abs_inverse_thms 1),
+ TRY (hyp_subst_tac 1),
+ rtac (sym RS range_eqI) 1,
+ resolve_tac iso_char_thms 1])])));
+
+ val Abs_inverse_thms = newT_Abs_inverse_thms @ (map (fn r =>
+ r RS mp RS f_inv_f RS subst) iso_thms);
+
+ (* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *)
+
+ fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
+ let
+ val (_, (tname, _, _)) = hd ds;
+ val {induction, ...} = the (Symtab.lookup (dt_info, tname));
+
+ fun mk_ind_concl (i, _) =
+ let
+ val T = nth_elem (i, recTs);
+ val Rep_t = Const (nth_elem (i, all_rep_names), T --> Univ_elT);
+ val rep_set_name = nth_elem (i, rep_set_names)
+ in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
+ HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
+ HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
+ HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT)))
+ end;
+
+ val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
+
+ val rewrites = map mk_meta_eq iso_char_thms;
+ val inj_thms' = map (fn r => r RS injD) inj_thms;
+
+ val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
+ (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
+ [indtac induction 1,
+ REPEAT (EVERY
+ [rtac allI 1, rtac impI 1,
+ exh_tac (exh_thm_of dt_info) 1,
+ REPEAT (EVERY
+ [hyp_subst_tac 1,
+ rewrite_goals_tac rewrites,
+ REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
+ (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
+ ORELSE (EVERY
+ [REPEAT (etac Scons_inject 1),
+ REPEAT (dresolve_tac
+ (inj_thms' @ [Leaf_inject, Inl_inject, Inr_inject]) 1),
+ REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
+ TRY (hyp_subst_tac 1),
+ rtac refl 1])])])]);
+
+ val inj_thms'' = map (fn r =>
+ r RS (allI RS (inj_def RS meta_eq_to_obj_eq RS iffD2)))
+ (split_conj_thm inj_thm);
+
+ val elem_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
+ (HOLogic.mk_Trueprop (mk_conj ind_concl2))) (fn _ =>
+ [indtac induction 1,
+ rewrite_goals_tac rewrites,
+ REPEAT (EVERY
+ [resolve_tac rep_intrs 1,
+ REPEAT ((atac 1) ORELSE (resolve_tac elem_thms 1))])]);
+
+ in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
+ end;
+
+ val (iso_inj_thms, iso_elem_thms) = foldr prove_iso_thms
+ (tl descr, (map snd newT_iso_inj_thms, map #3 newT_iso_axms));
+
+ (******************* freeness theorems for constructors *******************)
+
+ val _ = writeln "Proving freeness of constructors...";
+
+ (* prove theorem Rep_i (Constr_j ...) = Inj_j ... *)
+
+ fun prove_constr_rep_thm eqn =
+ let
+ val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
+ val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
+ in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
+ [resolve_tac inj_thms 1,
+ rewrite_goals_tac rewrites,
+ rtac refl 1,
+ resolve_tac rep_intrs 2,
+ REPEAT (resolve_tac iso_elem_thms 1)])
+ end;
+
+ (*--------------------------------------------------------------*)
+ (* constr_rep_thms and rep_congs are used to prove distinctness *)
+ (* of constructors internally. *)
+ (* the external version uses dt_case which is not defined yet *)
+ (*--------------------------------------------------------------*)
+
+ val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns;
+
+ val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
+ dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
+ (constr_rep_thms ~~ dist_lemmas);
+
+ (* prove injectivity of constructors *)
+
+ fun prove_constr_inj_thm rep_thms t =
+ let val inj_thms = Scons_inject::(map make_elim
+ ((map (fn r => r RS injD) iso_inj_thms) @
+ [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject]))
+ in prove_goalw_cterm [] (cterm_of (sign_of thy5) t) (fn _ =>
+ [rtac iffI 1,
+ REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
+ dresolve_tac rep_congs 1, dtac box_equals 1,
+ REPEAT (resolve_tac rep_thms 1),
+ REPEAT (eresolve_tac inj_thms 1),
+ hyp_subst_tac 1,
+ REPEAT (resolve_tac [conjI, refl] 1)])
+ end;
+
+ val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
+ ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
+
+ val thy6 = store_thmss "inject" new_type_names constr_inject thy5;
+
+ (*************************** induction theorem ****************************)
+
+ val _ = writeln "Proving induction rule for datatypes...";
+
+ val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
+ (map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
+ val Rep_inverse_thms' = map (fn r => r RS inv_f_f)
+ (drop (length newTs, iso_inj_thms));
+
+ fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
+ let
+ val Rep_t = Const (nth_elem (i, all_rep_names), T --> Univ_elT) $
+ mk_Free "x" T i;
+
+ val Abs_t = if i < length newTs then
+ Const (Sign.intern_const (sign_of thy6)
+ ("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T)
+ else Const (inv_name, [T --> Univ_elT, Univ_elT] ---> T) $
+ Const (nth_elem (i, all_rep_names), T --> Univ_elT)
+
+ in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,
+ Const (nth_elem (i, rep_set_names), UnivT)) $
+ (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
+ concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
+ end;
+
+ val (indrule_lemma_prems, indrule_lemma_concls) =
+ foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
+
+ val cert = cterm_of (sign_of thy6);
+
+ val indrule_lemma = prove_goalw_cterm [] (cert
+ (Logic.mk_implies
+ (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
+ HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls)))) (fn prems =>
+ [cut_facts_tac prems 1, REPEAT (etac conjE 1),
+ REPEAT (EVERY
+ [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
+ etac mp 1, resolve_tac iso_elem_thms 1])]);
+
+ val Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
+ val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
+ map (Free o apfst fst o dest_Var) Ps;
+ val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
+
+ val dt_induct = prove_goalw_cterm [] (cert
+ (DatatypeProp.make_ind descr sorts)) (fn prems =>
+ [rtac indrule_lemma' 1, indtac rep_induct 1,
+ EVERY (map (fn (prem, r) => (EVERY
+ [REPEAT (eresolve_tac Abs_inverse_thms 1),
+ simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
+ DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
+ (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
+
+ val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
+
+ in (thy7, constr_inject, dist_rewrites, dt_induct)
+ end;
+
+end;