# HG changeset patch # User wenzelm # Date 1323982012 -3600 # Node ID 36f3f0010b7d55a7bf0b456582b1e0a174922668 # Parent e7dbb27c13083ef00b65c58405d14189516faffe# Parent 629d123b7dbe63e5e2a7d11ba74484c9fad440c8 merged; diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Inductive.thy Thu Dec 15 21:46:52 2011 +0100 @@ -11,9 +11,10 @@ "Tools/dseq.ML" "Tools/Datatype/datatype_aux.ML" "Tools/Datatype/datatype_prop.ML" - "Tools/Datatype/datatype_case.ML" ("Tools/Datatype/datatype_abs_proofs.ML") ("Tools/Datatype/datatype_data.ML") + ("Tools/Datatype/datatype_case.ML") + ("Tools/Datatype/rep_datatype.ML") ("Tools/primrec.ML") ("Tools/Datatype/datatype_codegen.ML") begin @@ -276,8 +277,9 @@ text {* Package setup. *} use "Tools/Datatype/datatype_abs_proofs.ML" -use "Tools/Datatype/datatype_data.ML" -setup Datatype_Data.setup +use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup +use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup +use "Tools/Datatype/rep_datatype.ML" use "Tools/Datatype/datatype_codegen.ML" setup Datatype_Codegen.setup @@ -297,7 +299,7 @@ let (* FIXME proper name context!? *) val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT); - val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs]; + val ft = Datatype_Case.case_tr true ctxt [x, cs]; in lambda x ft end in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end *} diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/IsaMakefile Thu Dec 15 21:46:52 2011 +0100 @@ -218,6 +218,7 @@ Tools/Datatype/datatype_data.ML \ Tools/Datatype/datatype_prop.ML \ Tools/Datatype/datatype_realizer.ML \ + Tools/Datatype/rep_datatype.ML \ Tools/Function/context_tree.ML \ Tools/Function/fun.ML \ Tools/Function/function.ML \ @@ -247,6 +248,7 @@ Tools/arith_data.ML \ Tools/cnf_funcs.ML \ Tools/dseq.ML \ + Tools/enriched_type.ML \ Tools/inductive.ML \ Tools/inductive_realizer.ML \ Tools/inductive_set.ML \ @@ -263,7 +265,6 @@ Tools/split_rule.ML \ Tools/try_methods.ML \ Tools/typedef.ML \ - Tools/enriched_type.ML \ Transitive_Closure.thy \ Typedef.thy \ Wellfounded.thy diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/List.thy --- a/src/HOL/List.thy Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/List.thy Thu Dec 15 21:46:52 2011 +0100 @@ -391,7 +391,7 @@ Syntax.const @{syntax_const "_case1"} $ Syntax.const @{const_syntax dummy_pattern} $ NilC; val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2; - val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs]; + val ft = Datatype_Case.case_tr false ctxt [x, cs]; in lambda x ft end; fun abs_tr ctxt (p as Free (s, T)) e opti = diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 21:46:52 2011 +0100 @@ -38,35 +38,6 @@ open NominalAtoms; -(** FIXME: Datatype should export this function **) - -local - -fun dt_recs (Datatype_Aux.DtTFree _) = [] - | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts - | dt_recs (Datatype_Aux.DtRec i) = [i]; - -fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) = - let - fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); - val bnames = map the_bname (distinct op = (maps dt_recs args)); - in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; - - -fun induct_cases descr = - Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr)); - -fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i)); - -in - -fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr); - -fun mk_case_names_exhausts descr new = - map (Rule_Cases.case_names o exhaust_cases descr o #1) - (filter (fn ((_, (name, _, _))) => member (op =) new name) descr); - -end; (* theory data *) @@ -858,14 +829,14 @@ dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]) constr_rep_thmss dist_lemmas; - fun prove_distinct_thms _ (_, []) = [] - | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) = + fun prove_distinct_thms _ [] = [] + | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) = let val dist_thm = Goal.prove_global thy8 [] [] t (fn _ => simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1) in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: - prove_distinct_thms p (k, ts) + prove_distinct_thms p ts end; val distinct_thms = map2 prove_distinct_thms @@ -1074,7 +1045,7 @@ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)])) (prems ~~ constr_defs))]); - val case_names_induct = mk_case_names_induct descr''; + val case_names_induct = Datatype_Data.mk_case_names_induct descr''; (**** prove that new datatypes have finite support ****) diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Dec 15 21:46:52 2011 +0100 @@ -211,7 +211,7 @@ (* constructor definitions *) - fun make_constr_def tname (typedef: Typedef.info) T n + fun make_constr_def (typedef: Typedef.info) T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) = let fun constr_arg dt (j, l_args, r_args) = @@ -257,7 +257,7 @@ Drule.export_without_context (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); val (thy', defs', eqns', _) = - fold (make_constr_def tname typedef T (length constrs)) + fold (make_constr_def typedef T (length constrs)) (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1); in (Sign.parent_path thy', defs', eqns @ [eqns'], @@ -534,7 +534,7 @@ dist_lemma :: (rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) (constr_rep_thms ~~ dist_lemmas); - fun prove_distinct_thms dist_rewrites' (k, ts) = + fun prove_distinct_thms dist_rewrites' = let fun prove [] = [] | prove (t :: ts) = @@ -542,7 +542,7 @@ val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ => EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]) in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end; - in prove ts end; + in prove end; val distinct_thms = map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr); @@ -734,9 +734,9 @@ [] => () | dups => error ("Duplicate datatypes: " ^ commas_quote dups)); - fun prep_dt_spec ((tname, tvs, mx), constrs) (dts', constr_syntax, i) = + fun prep_dt_spec ((tname, tvs, _), constrs) (dts', constr_syntax, i) = let - fun prep_constr (cname, cargs, mx') (constrs, constr_syntax') = + fun prep_constr (cname, cargs, mx) (constrs, constr_syntax') = let val _ = (case subtract (op =) tvs (fold Term.add_tfreesT cargs []) of @@ -745,7 +745,7 @@ val c = Sign.full_name_path thy (Binding.name_of tname) cname; in (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs)], - constr_syntax' @ [(cname, mx')]) + constr_syntax' @ [(cname, mx)]) end handle ERROR msg => cat_error msg ("The error above occurred in constructor " ^ Binding.print cname ^ " of datatype " ^ Binding.print tname); @@ -779,7 +779,7 @@ |> representation_proofs config dt_info descr types_syntax constr_syntax (Datatype_Data.mk_case_names_induct (flat descr)) |-> (fn (inject, distinct, induct) => - Datatype_Data.derive_datatype_props config dt_names descr induct inject distinct) + Rep_Datatype.derive_datatype_props config dt_names descr induct inject distinct) end; val add_datatype = gen_add_datatype check_specs; diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 21:46:52 2011 +0100 @@ -9,17 +9,12 @@ sig datatype config = Error | Warning | Quiet type info = Datatype_Aux.info - val make_case: (string * typ -> info option) -> - Proof.context -> config -> string list -> term -> (term * term) list -> - term - val dest_case: (string -> info option) -> bool -> - string list -> term -> (term * (term * term) list) option - val strip_case: (string -> info option) -> bool -> - term -> (term * (term * term) list) option - val case_tr: bool -> (theory -> string * typ -> info option) -> - Proof.context -> term list -> term - val case_tr': (theory -> string -> info option) -> - string -> Proof.context -> term list -> term + val make_case : Proof.context -> config -> string list -> term -> (term * term) list -> term + val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option + val case_tr: bool -> Proof.context -> term list -> term + val case_tr': string -> Proof.context -> term list -> term + val add_case_tr' : string list -> theory -> theory + val setup: theory -> theory end; structure Datatype_Case : DATATYPE_CASE = @@ -34,19 +29,16 @@ (* Get information about datatypes *) -fun ty_info tab sT = - (case tab sT of - SOME ({descr, case_name, index, ...} : info) => - let - val (_, (tname, dts, constrs)) = nth descr index; - val mk_ty = Datatype_Aux.typ_of_dtyp descr; - val T = Type (tname, map mk_ty dts); - in - SOME {case_name = case_name, - constructors = map (fn (cname, dts') => - Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs} - end - | NONE => NONE); +fun ty_info ({descr, case_name, index, ...} : info) = + let + val (_, (tname, dts, constrs)) = nth descr index; + val mk_ty = Datatype_Aux.typ_of_dtyp descr; + val T = Type (tname, map mk_ty dts); + in + {case_name = case_name, + constructors = map (fn (cname, dts') => + Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs} + end; (*Each pattern carries with it a tag i, which denotes the clause it @@ -72,7 +64,7 @@ (*Produce an instance of a constructor, plus fresh variables for its arguments.*) fun fresh_constr ty_match ty_inst colty used c = let - val (_, Ty) = dest_Const c + val (_, Ty) = dest_Const c; val Ts = binder_types Ty; val names = Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)); @@ -84,7 +76,7 @@ in (c', gvars) end; -(*Goes through a list of rows and picks out the ones beginning with a +(*Go through a list of rows and pick out the ones beginning with a pattern with constructor = name.*) fun mk_group (name, T) rows = let val k = length (binder_types T) in @@ -147,8 +139,10 @@ (* Translation of pattern terms into nested case expressions. *) -fun mk_case tab ctxt ty_match ty_inst type_of used range_ty = +fun mk_case ctxt ty_match ty_inst type_of used range_ty = let + val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt); + val name = singleton (Name.variant_list used) "a"; fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1) | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) = @@ -172,7 +166,7 @@ apfst (subst_free [(v, u)]) |>> v_to_prfx) (col0 ~~ rows); in mk us rows' end | SOME (Const (cname, cT), i) => - (case ty_info tab (cname, cT) of + (case Option.map ty_info (get_info (cname, cT)) of NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i) | SOME {case_name, constructors} => let @@ -203,17 +197,19 @@ fun case_error s = error ("Error in case expression:\n" ^ s); +local + (*Repeated variable occurrences in a pattern are not allowed.*) fun no_repeat_vars ctxt pat = fold_aterms (fn x as Free (s, _) => - (fn xs => - if member op aconv xs x then - case_error (quote s ^ " occurs repeatedly in the pattern " ^ - quote (Syntax.string_of_term ctxt pat)) - else x :: xs) + (fn xs => + if member op aconv xs x then + case_error (quote s ^ " occurs repeatedly in the pattern " ^ + quote (Syntax.string_of_term ctxt pat)) + else x :: xs) | _ => I) pat []; -fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses = +fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses = let fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs); @@ -226,7 +222,7 @@ | _ => case_error "all cases must have the same result type"); val used' = fold add_row_used rows used; val (tags, case_tm) = - mk_case tab ctxt ty_match ty_inst type_of used' rangeT [x] rows + mk_case ctxt ty_match ty_inst type_of used' rangeT [x] rows handle CASE_ERROR (msg, i) => case_error (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i))); @@ -241,17 +237,21 @@ case_tm end; -fun make_case tab ctxt = +in + +fun make_case ctxt = gen_make_case (match_type (Proof_Context.theory_of ctxt)) - Envir.subst_term_types fastype_of tab ctxt; + Envir.subst_term_types fastype_of ctxt; val make_case_untyped = gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT); +end; + (* parse translation *) -fun case_tr err tab_of ctxt [t, u] = +fun case_tr err ctxt [t, u] = let val thy = Proof_Context.theory_of ctxt; val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt); @@ -285,20 +285,27 @@ | dest_case2 t = [t]; val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u)); val case_tm = - make_case_untyped (tab_of thy) ctxt + make_case_untyped ctxt (if err then Error else Warning) [] (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT) (flat cnstrts) t) cases; in case_tm end - | case_tr _ _ _ ts = case_error "case_tr"; + | case_tr _ _ _ = case_error "case_tr"; + +val trfun_setup = + Sign.add_advanced_trfuns ([], + [(@{syntax_const "_case_syntax"}, case_tr true)], + [], []); (* Pretty printing of nested case expressions *) (* destruct one level of pattern matching *) +local + (* FIXME proper name context!? *) -fun gen_dest_case name_of type_of tab d used t = +fun gen_dest_case name_of type_of ctxt d used t = (case apfst name_of (strip_comb t) of (SOME cname, ts as _ :: _) => let @@ -320,9 +327,10 @@ | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c); val is_undefined = name_of #> equal (SOME @{const_name undefined}); fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body); + val get_info = Datatype_Data.info_of_case (Proof_Context.theory_of ctxt); in - (case ty_info tab cname of - SOME {constructors, case_name} => + (case Option.map ty_info (get_info cname) of + SOME {constructors, ...} => if length fs = length constructors then let val cases = map (fn (Const (s, U), t) => @@ -362,12 +370,18 @@ end | _ => NONE); +in + val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of; val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT); +end; + (* destruct nested patterns *) +local + fun strip_case'' dest (pat, rhs) = (case dest (Term.add_free_names pat []) rhs of SOME (exp as Free _, clauses) => @@ -385,15 +399,18 @@ SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses) | NONE => NONE); +in + val strip_case = gen_strip_case oo dest_case; val strip_case' = gen_strip_case oo dest_case'; +end; + (* print translation *) -fun case_tr' tab_of cname ctxt ts = +fun case_tr' cname ctxt ts = let - val thy = Proof_Context.theory_of ctxt; fun mk_clause (pat, rhs) = let val xs = Term.add_frees pat [] in Syntax.const @{syntax_const "_case1"} $ @@ -406,7 +423,7 @@ | t => t) rhs end; in - (case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of + (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of SOME (x, clauses) => Syntax.const @{syntax_const "_case_syntax"} $ x $ foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u) @@ -414,4 +431,15 @@ | NONE => raise Match) end; +fun add_case_tr' case_names thy = + Sign.add_advanced_trfuns ([], [], + map (fn case_name => + let val case_name' = Lexicon.mark_const case_name + in (case_name', case_tr' case_name') end) case_names, []) thy; + + +(* theory setup *) + +val setup = trfun_setup; + end; diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Dec 15 21:46:52 2011 +0100 @@ -79,8 +79,7 @@ val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index); fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) = [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)]; - val distincts = - maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index)); + val distincts = maps prep_distinct (nth (Datatype_Prop.make_distincts [descr]) index); val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty))); val simpset = Simplifier.global_context thy diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 21:46:52 2011 +0100 @@ -1,35 +1,29 @@ (* Title: HOL/Tools/Datatype/datatype_data.ML Author: Stefan Berghofer, TU Muenchen -Datatype package: bookkeeping; interpretation of existing types as datatypes. +Datatype package bookkeeping. *) signature DATATYPE_DATA = sig include DATATYPE_COMMON - val derive_datatype_props : config -> string list -> descr list -> - thm -> thm list list -> thm list list -> theory -> string list * theory - val rep_datatype : config -> (string list -> Proof.context -> Proof.context) -> - term list -> theory -> Proof.state - val rep_datatype_cmd : config -> (string list -> Proof.context -> Proof.context) -> - string list -> theory -> Proof.state + val get_all : theory -> info Symtab.table val get_info : theory -> string -> info option val the_info : theory -> string -> info + val info_of_constr : theory -> string * typ -> info option + val info_of_constr_permissive : theory -> string * typ -> info option + val info_of_case : theory -> string -> info option + val register: (string * info) list -> theory -> theory + val the_spec : theory -> string -> (string * sort) list * (string * typ list) list val the_descr : theory -> string list -> descr * (string * sort) list * string list * string * (string list * string list) * (typ list * typ list) - val the_spec : theory -> string -> (string * sort) list * (string * typ list) list val all_distincts : theory -> typ list -> thm list list val get_constrs : theory -> string -> (string * typ) list option - val get_all : theory -> info Symtab.table - val info_of_constr : theory -> string * typ -> info option - val info_of_constr_permissive : theory -> string * typ -> info option - val info_of_case : theory -> string -> info option + val mk_case_names_induct: descr -> attribute + val mk_case_names_exhausts: descr -> string list -> attribute list val interpretation : (config -> string list -> theory -> theory) -> theory -> theory - val make_case : Proof.context -> Datatype_Case.config -> string list -> term -> - (term * term) list -> term - val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option - val mk_case_names_induct: descr -> attribute + val interpretation_data : config * string list -> theory -> theory val setup: theory -> theory end; @@ -40,7 +34,7 @@ (* data management *) -structure DatatypesData = Theory_Data +structure Data = Theory_Data ( type T = {types: Datatype_Aux.info Symtab.table, @@ -58,7 +52,7 @@ cases = Symtab.merge (K true) (cases1, cases2)}; ); -val get_all = #types o DatatypesData.get; +val get_all = #types o Data.get; val get_info = Symtab.lookup o get_all; fun the_info thy name = @@ -68,7 +62,7 @@ fun info_of_constr thy (c, T) = let - val tab = Symtab.lookup_list (#constrs (DatatypesData.get thy)) c; + val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; in (case body_type T of Type (tyco, _) => AList.lookup (op =) tab tyco @@ -77,7 +71,7 @@ fun info_of_constr_permissive thy (c, T) = let - val tab = Symtab.lookup_list (#constrs (DatatypesData.get thy)) c; + val tab = Symtab.lookup_list (#constrs (Data.get thy)) c; val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE); val default = if null tab then NONE else SOME (snd (List.last tab)); (*conservative wrt. overloaded constructors*) @@ -90,10 +84,10 @@ | SOME info => SOME info)) end; -val info_of_case = Symtab.lookup o #cases o DatatypesData.get; +val info_of_case = Symtab.lookup o #cases o Data.get; fun register (dt_infos : (string * Datatype_Aux.info) list) = - DatatypesData.map (fn {types, constrs, cases} => + Data.map (fn {types, constrs, cases} => {types = types |> fold Symtab.update dt_infos, constrs = constrs |> fold (fn (constr, dtname_info) => Symtab.map_default (constr, []) (cons dtname_info)) @@ -200,27 +194,6 @@ end; -(* translation rules for case *) - -fun make_case ctxt = - Datatype_Case.make_case (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt; - -fun strip_case ctxt = - Datatype_Case.strip_case (info_of_case (Proof_Context.theory_of ctxt)); - -fun add_case_tr' case_names thy = - Sign.add_advanced_trfuns ([], [], - map (fn case_name => - let val case_name' = Lexicon.mark_const case_name in - (case_name', Datatype_Case.case_tr' info_of_case case_name') - end) case_names, []) thy; - -val trfun_setup = - Sign.add_advanced_trfuns ([], - [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)], - [], []); - - (** document antiquotation **) @@ -257,205 +230,16 @@ val eq: T * T -> bool = eq_snd (op =); ); fun interpretation f = Datatype_Interpretation.interpretation (uncurry f); - -fun make_dt_info descr induct inducts rec_names rec_rewrites - (index, (((((((((((_, (tname, _, _))), inject), distinct), - exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), - (split, split_asm))) = - (tname, - {index = index, - descr = descr, - inject = inject, - distinct = distinct, - induct = induct, - inducts = inducts, - exhaust = exhaust, - nchotomy = nchotomy, - rec_names = rec_names, - rec_rewrites = rec_rewrites, - case_name = case_name, - case_rewrites = case_rewrites, - case_cong = case_cong, - weak_case_cong = weak_case_cong, - split = split, - split_asm = split_asm}); - -fun derive_datatype_props config dt_names descr induct inject distinct thy1 = - let - val thy2 = thy1 |> Theory.checkpoint; - val flat_descr = flat descr; - val new_type_names = map Long_Name.base_name dt_names; - val _ = - Datatype_Aux.message config - ("Deriving properties for datatype(s) " ^ commas_quote new_type_names); - - val (exhaust, thy3) = thy2 - |> Datatype_Abs_Proofs.prove_casedist_thms config new_type_names - descr induct (mk_case_names_exhausts flat_descr dt_names); - val (nchotomys, thy4) = thy3 - |> Datatype_Abs_Proofs.prove_nchotomys config new_type_names descr exhaust; - val ((rec_names, rec_rewrites), thy5) = thy4 - |> Datatype_Abs_Proofs.prove_primrec_thms - config new_type_names descr (#inject o the o Symtab.lookup (get_all thy4)) - inject (distinct, all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr)) induct; - val ((case_rewrites, case_names), thy6) = thy5 - |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites; - val (case_congs, thy7) = thy6 - |> Datatype_Abs_Proofs.prove_case_congs new_type_names case_names descr - nchotomys case_rewrites; - val (weak_case_congs, thy8) = thy7 - |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names case_names descr; - val (splits, thy9) = thy8 - |> Datatype_Abs_Proofs.prove_split_thms - config new_type_names case_names descr inject distinct exhaust case_rewrites; - - val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct; - val dt_infos = map_index - (make_dt_info flat_descr induct inducts rec_names rec_rewrites) - (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~ - case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits); - val dt_names = map fst dt_infos; - val prfx = Binding.qualify true (space_implode "_" new_type_names); - val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites; - val named_rules = flat (map_index (fn (index, tname) => - [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]), - ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names); - val unnamed_rules = map (fn induct => - ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""])) - (drop (length dt_names) inducts); - in - thy9 - |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []), - ((prfx (Binding.name "inducts"), inducts), []), - ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []), - ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites), - [Simplifier.simp_add]), - ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]), - ((Binding.empty, flat inject), [iff_add]), - ((Binding.empty, map (fn th => th RS notE) (flat distinct)), - [Classical.safe_elim NONE]), - ((Binding.empty, weak_case_congs), [Simplifier.cong_add]), - ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @ - named_rules @ unnamed_rules) - |> snd - |> add_case_tr' case_names - |> register dt_infos - |> Datatype_Interpretation.data (config, dt_names) - |> pair dt_names - end; +val interpretation_data = Datatype_Interpretation.data; -(** declare existing type as datatype **) - -fun prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct thy1 = - let - val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct; - val new_type_names = map Long_Name.base_name dt_names; - val prfx = Binding.qualify true (space_implode "_" new_type_names); - val (((inject, distinct), [induct]), thy2) = - thy1 - |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject - ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct - ||>> Global_Theory.add_thms - [((prfx (Binding.name "induct"), raw_induct), - [mk_case_names_induct descr])]; - in - thy2 - |> derive_datatype_props config dt_names [descr] induct inject distinct - end; - -fun gen_rep_datatype prep_term config after_qed raw_ts thy = - let - val ctxt = Proof_Context.init_global thy; - - fun constr_of_term (Const (c, T)) = (c, T) - | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t); - fun no_constr (c, T) = - error ("Bad constructor: " ^ Proof_Context.extern_const ctxt c ^ "::" ^ - Syntax.string_of_typ ctxt T); - fun type_of_constr (cT as (_, T)) = - let - val frees = Term.add_tfreesT T []; - val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T)) - handle TYPE _ => no_constr cT - val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else (); - val _ = if length frees <> length vs then no_constr cT else (); - in (tyco, (vs, cT)) end; - - val raw_cs = - AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts); - val _ = - (case map_filter (fn (tyco, _) => - if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs of - [] => () - | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductivly")); - val raw_vss = maps (map (map snd o fst) o snd) raw_cs; - val ms = - (case distinct (op =) (map length raw_vss) of - [n] => 0 upto n - 1 - | _ => error "Different types in given constructors"); - fun inter_sort m = - map (fn xs => nth xs m) raw_vss - |> foldr1 (Sorts.inter_sort (Sign.classes_of thy)); - val sorts = map inter_sort ms; - val vs = Name.invent_names Name.context Name.aT sorts; - - fun norm_constr (raw_vs, (c, T)) = - (c, map_atyps - (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T); - - val cs = map (apsnd (map norm_constr)) raw_cs; - val dtyps_of_typ = map (Datatype_Aux.dtyp_of_typ (map (rpair vs o fst) cs)) o binder_types; - val dt_names = map fst cs; - - fun mk_spec (i, (tyco, constr)) = - (i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr)); - val descr = map_index mk_spec cs; - val injs = Datatype_Prop.make_injs [descr]; - val half_distincts = map snd (Datatype_Prop.make_distincts [descr]); - val ind = Datatype_Prop.make_ind [descr]; - val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts]; - - fun after_qed' raw_thms = - let - val [[[raw_induct]], raw_inject, half_distinct] = - unflat rules (map Drule.zero_var_indexes_list raw_thms); - (*FIXME somehow dubious*) - in - Proof_Context.background_theory_result (* FIXME !? *) - (prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct) - #-> after_qed - end; - in - ctxt - |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules)) - end; - -val rep_datatype = gen_rep_datatype Sign.cert_term; -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global; - - - -(** package setup **) - -(* setup theory *) +(** setup theory **) val setup = - trfun_setup #> antiq_setup #> Datatype_Interpretation.init; - -(* outer syntax *) - -val _ = - Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal - (Scan.repeat1 Parse.term >> (fn ts => - Toplevel.print o - Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts))); - - open Datatype_Aux; end; diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 21:46:52 2011 +0100 @@ -10,7 +10,7 @@ val indexify_names: string list -> string list val make_tnames: typ list -> string list val make_injs : descr list -> term list list - val make_distincts : descr list -> (int * term list) list (*no symmetric inequalities*) + val make_distincts : descr list -> term list list (*no symmetric inequalities*) val make_ind : descr list -> term val make_casedists : descr list -> term list val make_primrec_Ts : descr list -> string list -> typ list * typ list @@ -99,7 +99,7 @@ in map make_distincts'' constrs @ make_distincts' T constrs end; in map2 (fn ((_, (_, _, constrs))) => fn T => - (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs + make_distincts' T (map prep_constr constrs)) (hd descr) newTs end; diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Datatype/rep_datatype.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Thu Dec 15 21:46:52 2011 +0100 @@ -0,0 +1,214 @@ +(* Title: HOL/Tools/Datatype/rep_datatype.ML + Author: Stefan Berghofer, TU Muenchen + +Representation of existing types as datatypes. +*) + +signature REP_DATATYPE = +sig + val derive_datatype_props : Datatype_Aux.config -> string list -> Datatype_Aux.descr list -> + thm -> thm list list -> thm list list -> theory -> string list * theory + val rep_datatype : Datatype_Aux.config -> (string list -> Proof.context -> Proof.context) -> + term list -> theory -> Proof.state + val rep_datatype_cmd : Datatype_Aux.config -> (string list -> Proof.context -> Proof.context) -> + string list -> theory -> Proof.state +end; + +structure Rep_Datatype: REP_DATATYPE = +struct + +fun make_dt_info descr induct inducts rec_names rec_rewrites + (index, (((((((((((_, (tname, _, _))), inject), distinct), + exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong), + (split, split_asm))) = + (tname, + {index = index, + descr = descr, + inject = inject, + distinct = distinct, + induct = induct, + inducts = inducts, + exhaust = exhaust, + nchotomy = nchotomy, + rec_names = rec_names, + rec_rewrites = rec_rewrites, + case_name = case_name, + case_rewrites = case_rewrites, + case_cong = case_cong, + weak_case_cong = weak_case_cong, + split = split, + split_asm = split_asm}); + +fun derive_datatype_props config dt_names descr induct inject distinct thy1 = + let + val thy2 = thy1 |> Theory.checkpoint; + val flat_descr = flat descr; + val new_type_names = map Long_Name.base_name dt_names; + val _ = + Datatype_Aux.message config + ("Deriving properties for datatype(s) " ^ commas_quote new_type_names); + + val (exhaust, thy3) = thy2 + |> Datatype_Abs_Proofs.prove_casedist_thms config new_type_names + descr induct (Datatype_Data.mk_case_names_exhausts flat_descr dt_names); + val (nchotomys, thy4) = thy3 + |> Datatype_Abs_Proofs.prove_nchotomys config new_type_names descr exhaust; + val ((rec_names, rec_rewrites), thy5) = thy4 + |> Datatype_Abs_Proofs.prove_primrec_thms + config new_type_names descr (#inject o the o Symtab.lookup (Datatype_Data.get_all thy4)) + inject (distinct, Datatype_Data.all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr)) + induct; + val ((case_rewrites, case_names), thy6) = thy5 + |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites; + val (case_congs, thy7) = thy6 + |> Datatype_Abs_Proofs.prove_case_congs new_type_names case_names descr + nchotomys case_rewrites; + val (weak_case_congs, thy8) = thy7 + |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names case_names descr; + val (splits, thy9) = thy8 + |> Datatype_Abs_Proofs.prove_split_thms + config new_type_names case_names descr inject distinct exhaust case_rewrites; + + val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct; + val dt_infos = + map_index + (make_dt_info flat_descr induct inducts rec_names rec_rewrites) + (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~ + case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits); + val dt_names = map fst dt_infos; + val prfx = Binding.qualify true (space_implode "_" new_type_names); + val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites; + val named_rules = flat (map_index (fn (index, tname) => + [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]), + ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names); + val unnamed_rules = map (fn induct => + ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""])) + (drop (length dt_names) inducts); + in + thy9 + |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []), + ((prfx (Binding.name "inducts"), inducts), []), + ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []), + ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites), + [Simplifier.simp_add]), + ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]), + ((Binding.empty, flat inject), [iff_add]), + ((Binding.empty, map (fn th => th RS notE) (flat distinct)), + [Classical.safe_elim NONE]), + ((Binding.empty, weak_case_congs), [Simplifier.cong_add]), + ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @ + named_rules @ unnamed_rules) + |> snd + |> Datatype_Data.register dt_infos + |> Datatype_Data.interpretation_data (config, dt_names) + |> Datatype_Case.add_case_tr' case_names + |> pair dt_names + end; + + + +(** declare existing type as datatype **) + +local + +fun prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct thy1 = + let + val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct; + val new_type_names = map Long_Name.base_name dt_names; + val prfx = Binding.qualify true (space_implode "_" new_type_names); + val (((inject, distinct), [induct]), thy2) = + thy1 + |> Datatype_Aux.store_thmss "inject" new_type_names raw_inject + ||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct + ||>> Global_Theory.add_thms + [((prfx (Binding.name "induct"), raw_induct), + [Datatype_Data.mk_case_names_induct descr])]; + in + thy2 + |> derive_datatype_props config dt_names [descr] induct inject distinct + end; + +fun gen_rep_datatype prep_term config after_qed raw_ts thy = + let + val ctxt = Proof_Context.init_global thy; + + fun constr_of_term (Const (c, T)) = (c, T) + | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t); + fun no_constr (c, T) = + error ("Bad constructor: " ^ Proof_Context.extern_const ctxt c ^ "::" ^ + Syntax.string_of_typ ctxt T); + fun type_of_constr (cT as (_, T)) = + let + val frees = Term.add_tfreesT T []; + val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T)) + handle TYPE _ => no_constr cT + val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else (); + val _ = if length frees <> length vs then no_constr cT else (); + in (tyco, (vs, cT)) end; + + val raw_cs = + AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts); + val _ = + (case map_filter (fn (tyco, _) => + if Symtab.defined (Datatype_Data.get_all thy) tyco then SOME tyco else NONE) raw_cs of + [] => () + | tycos => error ("Type(s) " ^ commas_quote tycos ^ " already represented inductivly")); + val raw_vss = maps (map (map snd o fst) o snd) raw_cs; + val ms = + (case distinct (op =) (map length raw_vss) of + [n] => 0 upto n - 1 + | _ => error "Different types in given constructors"); + fun inter_sort m = + map (fn xs => nth xs m) raw_vss + |> foldr1 (Sorts.inter_sort (Sign.classes_of thy)); + val sorts = map inter_sort ms; + val vs = Name.invent_names Name.context Name.aT sorts; + + fun norm_constr (raw_vs, (c, T)) = + (c, map_atyps + (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T); + + val cs = map (apsnd (map norm_constr)) raw_cs; + val dtyps_of_typ = map (Datatype_Aux.dtyp_of_typ (map (rpair vs o fst) cs)) o binder_types; + val dt_names = map fst cs; + + fun mk_spec (i, (tyco, constr)) = + (i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr)); + val descr = map_index mk_spec cs; + val injs = Datatype_Prop.make_injs [descr]; + val half_distincts = Datatype_Prop.make_distincts [descr]; + val ind = Datatype_Prop.make_ind [descr]; + val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts]; + + fun after_qed' raw_thms = + let + val [[[raw_induct]], raw_inject, half_distinct] = + unflat rules (map Drule.zero_var_indexes_list raw_thms); + (*FIXME somehow dubious*) + in + Proof_Context.background_theory_result (* FIXME !? *) + (prove_rep_datatype config dt_names descr raw_inject half_distinct raw_induct) + #-> after_qed + end; + in + ctxt + |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules)) + end; + +in + +val rep_datatype = gen_rep_datatype Sign.cert_term; +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global; + +end; + + +(* outer syntax *) + +val _ = + Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal + (Scan.repeat1 Parse.term >> (fn ts => + Toplevel.print o + Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts))); + +end; diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Dec 15 21:46:52 2011 +0100 @@ -663,7 +663,7 @@ val v = Free (name, T); val v' = Free (name', T); in - lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v + lambda v (Datatype_Case.make_case ctxt Datatype_Case.Quiet [] v [(HOLogic.mk_tuple out_ts, if null eqs'' then success_t else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $ @@ -949,7 +949,7 @@ in (pattern, compilation) end - val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var + val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] inp_var ((map compile_single_case switched_clauses) @ [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))]) in diff -r e7dbb27c1308 -r 36f3f0010b7d src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 15 16:10:44 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 15 21:46:52 2011 +0100 @@ -412,7 +412,7 @@ end fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = - Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => + Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => (t, mk_case_term ctxt (p - 1) qs' c)) cs) | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) = if p = 0 then t else mk_case_term ctxt (p - 1) qs' c