# HG changeset patch # User berghofe # Date 901277406 -7200 # Node ID 0d3a168e4d44ef74339b07c741b4bd2f3c7e11cb # Parent 36d38be7e814329188248b78db98a9bc7958ae58 New datatype definition package diff -r 36d38be7e814 -r 0d3a168e4d44 src/HOL/Tools/datatype_abs_proofs.ML --- /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; diff -r 36d38be7e814 -r 0d3a168e4d44 src/HOL/Tools/datatype_aux.ML --- /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; diff -r 36d38be7e814 -r 0d3a168e4d44 src/HOL/Tools/datatype_package.ML --- /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; diff -r 36d38be7e814 -r 0d3a168e4d44 src/HOL/Tools/datatype_prop.ML --- /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; diff -r 36d38be7e814 -r 0d3a168e4d44 src/HOL/Tools/datatype_rep_proofs.ML --- /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;