# HG changeset patch # User haftmann # Date 1213104633 -7200 # Node ID 791607529f6d6c0c357a6cca454087d8d43071de # Parent d8549f4d900b0f36e73ba454631928c31e3cdd21 rep_datatype command now takes list of constructors as input arguments diff -r d8549f4d900b -r 791607529f6d NEWS --- a/NEWS Tue Jun 10 15:30:06 2008 +0200 +++ b/NEWS Tue Jun 10 15:30:33 2008 +0200 @@ -1,6 +1,41 @@ Isabelle NEWS -- history user-relevant changes ============================================== +New +--- + +*** Pure *** + +* 'instance': attached definitions now longer accepted. INCOMPATIBILITY. + +* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. + + +*** HOL *** + +* 'rep_datatype': instead of theorem names the command now takes a list of terms +denoting the constructors of the type to be represented as datatype. The +characteristic theorems have to be proven. INCOMPATIBILITY. Also observe that +the following theorems have disappeared in favour of existing ones: + unit_induct ~> unit.induct + prod_induct ~> prod.induct + sum_induct ~> sum.induct + Suc_Suc_eq ~> nat.inject + Suc_not_Zero Zero_not_Suc ~> nat.distinct + +* Tactics induct_tac and thm_induct_tac now take explicit context as arguments; +type-specific induction rules are identified by the 'induct' attribute rather +than querying the datatype package directly. INCOMPATIBILITY. + +* 'Least' operator now restricted to class 'order' (and subclasses). +INCOMPATIBILITY. + +* Library/Nat_Infinity: added addition, numeral syntax and more instantiations +for algebraic structures. Removed some duplicate theorems. Changes in simp +rules. INCOMPATIBILITY. + + + New in Isabelle2008 (June 2008) ------------------------------- @@ -150,7 +185,7 @@ reconstruction_modulus, reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY. -* Method "induction_scheme" derives user-specified induction rules +* Method "induct_scheme" derives user-specified induction rules from well-founded induction and completeness of patterns. This factors out some operations that are done internally by the function package and makes them available separately. See diff -r d8549f4d900b -r 791607529f6d src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Datatype.thy Tue Jun 10 15:30:33 2008 +0200 @@ -533,10 +533,13 @@ subsection {* Representing sums *} -rep_datatype sum - distinct Inl_not_Inr Inr_not_Inl - inject Inl_eq Inr_eq - induction sum_induct +rep_datatype (sum) Inl Inr +proof - + fix P + fix s :: "'a + 'b" + assume x: "\x\'a. P (Inl x)" and y: "\y\'b. P (Inr y)" + then show "P s" by (auto intro: sumE [of s]) +qed simp_all lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)" by (rule ext) (simp split: sum.split) diff -r d8549f4d900b -r 791607529f6d src/HOL/HoareParallel/OG_Tactics.thy --- a/src/HOL/HoareParallel/OG_Tactics.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/HoareParallel/OG_Tactics.thy Tue Jun 10 15:30:33 2008 +0200 @@ -1,6 +1,7 @@ header {* \section{Generation of Verification Conditions} *} -theory OG_Tactics imports OG_Hoare +theory OG_Tactics +imports OG_Hoare begin lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq @@ -268,7 +269,7 @@ by auto lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps" lemmas my_simp_list = list_lemmas fst_conv snd_conv -not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc Suc_Suc_eq +not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject Collect_mem_eq ball_simps option.simps primrecdef_list lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length diff -r d8549f4d900b -r 791607529f6d src/HOL/Library/Code_Index.thy --- a/src/HOL/Library/Code_Index.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Library/Code_Index.thy Tue Jun 10 15:30:33 2008 +0200 @@ -10,7 +10,7 @@ text {* Indices are isomorphic to HOL @{typ nat} but - mapped to target-language builtin integers + mapped to target-language builtin integers. *} subsection {* Datatype of indices *} @@ -74,35 +74,23 @@ definition [simp]: "Suc_index k = index_of_nat (Suc (nat_of_index k))" -lemma index_induct: "P 0 \ (\k. P k \ P (Suc_index k)) \ P k" +rep_datatype "0 \ index" Suc_index proof - + fix P :: "index \ bool" + fix k :: index assume "P 0" then have init: "P (index_of_nat 0)" by simp assume "\k. P k \ P (Suc_index k)" - then have "\n. P (index_of_nat n) \ P (Suc_index (index_of_nat (n)))" . + then have "\n. P (index_of_nat n) \ P (Suc_index (index_of_nat n))" . then have step: "\n. P (index_of_nat n) \ P (index_of_nat (Suc n))" by simp from init step have "P (index_of_nat (nat_of_index k))" by (induct "nat_of_index k") simp_all then show "P k" by simp -qed - -lemma Suc_not_Zero_index: "Suc_index k \ 0" - by simp - -lemma Zero_not_Suc_index: "0 \ Suc_index k" - by simp - -lemma Suc_Suc_index_eq: "Suc_index k = Suc_index l \ k = l" - by simp - -rep_datatype index - distinct Suc_not_Zero_index Zero_not_Suc_index - inject Suc_Suc_index_eq - induction index_induct +qed simp_all lemmas [code func del] = index.recs index.cases declare index_case [case_names nat, cases type: index] -declare index_induct [case_names nat, induct type: index] +declare index.induct [case_names nat, induct type: index] lemma [code func]: "index_size = nat_of_index" diff -r d8549f4d900b -r 791607529f6d src/HOL/MetisExamples/BT.thy --- a/src/HOL/MetisExamples/BT.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/MetisExamples/BT.thy Tue Jun 10 15:30:33 2008 +0200 @@ -7,7 +7,9 @@ header {* Binary trees *} -theory BT imports Main begin +theory BT +imports Main +begin datatype 'a bt = @@ -100,7 +102,7 @@ lemma reflect_reflect_ident: "reflect (reflect t) = t" apply (induct t) apply (metis add_right_cancel reflect.simps(1)); - apply (metis Suc_Suc_eq reflect.simps(2)) + apply (metis reflect.simps(2)) done ML {*ResAtp.problem_name := "BT__bt_map_ident"*} diff -r d8549f4d900b -r 791607529f6d src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Nat.thy Tue Jun 10 15:30:33 2008 +0200 @@ -43,12 +43,12 @@ global typedef (open Nat) - nat = "Collect Nat" - by (rule exI, rule CollectI, rule Nat.Zero_RepI) + nat = Nat + by (rule exI, unfold mem_def, rule Nat.Zero_RepI) constdefs - Suc :: "nat => nat" - Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" + Suc :: "nat => nat" + Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" local @@ -62,34 +62,32 @@ end -lemma nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" - apply (unfold Zero_nat_def Suc_def) - apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} - apply (erule Rep_Nat [THEN CollectD, THEN Nat.induct]) - apply (iprover elim: Abs_Nat_inverse [OF CollectI, THEN subst]) - done +lemma Suc_not_Zero: "Suc m \ 0" +apply (simp add: Zero_nat_def Suc_def Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]) +done -lemma Suc_not_Zero [iff]: "Suc m \ 0" - by (simp add: Zero_nat_def Suc_def - Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI Zero_RepI - Suc_Rep_not_Zero_Rep) - -lemma Zero_not_Suc [iff]: "0 \ Suc m" +lemma Zero_not_Suc: "0 \ Suc m" by (rule not_sym, rule Suc_not_Zero not_sym) -lemma inj_Suc[simp]: "inj_on Suc N" - by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI - inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) - -lemma Suc_Suc_eq [iff]: "Suc m = Suc n \ m = n" - by (rule inj_Suc [THEN inj_eq]) +rep_datatype "0 \ nat" Suc +apply (unfold Zero_nat_def Suc_def) +apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} +apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct]) +apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst]) +apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def] + Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def] + Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric] + inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) +done -rep_datatype nat - distinct Suc_not_Zero Zero_not_Suc - inject Suc_Suc_eq - induction nat_induct +lemma nat_induct [case_names 0 Suc, induct type: nat]: + -- {* for backward compatibility -- naming of variables differs *} + fixes n + assumes "P 0" + and "\n. P n \ P (Suc n)" + shows "P n" + using assms by (rule nat.induct) -declare nat.induct [case_names 0 Suc, induct type: nat] declare nat.exhaust [case_names 0 Suc, cases type: nat] lemmas nat_rec_0 = nat.recs(1) @@ -97,10 +95,13 @@ lemmas nat_case_0 = nat.cases(1) and nat_case_Suc = nat.cases(2) - + text {* Injectiveness and distinctness lemmas *} +lemma inj_Suc[simp]: "inj_on Suc N" + by (simp add: inj_on_def) + lemma Suc_neq_Zero: "Suc m = 0 \ R" by (rule notE, rule Suc_not_Zero) @@ -1245,7 +1246,7 @@ definition Nats :: "'a set" where - "Nats = range of_nat" + [code func del]: "Nats = range of_nat" notation (xsymbols) Nats ("\") diff -r d8549f4d900b -r 791607529f6d src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Product_Type.thy Tue Jun 10 15:30:33 2008 +0200 @@ -17,9 +17,7 @@ subsection {* @{typ bool} is a datatype *} -rep_datatype bool - distinct True_not_False False_not_True - induction bool_induct +rep_datatype True False by (auto intro: bool_induct) declare case_split [cases type: bool] -- "prefer plain propositional version" @@ -67,11 +65,7 @@ Addsimprocs [unit_eq_proc]; *} -lemma unit_induct [noatp,induct type: unit]: "P () ==> P x" - by simp - -rep_datatype unit - induction unit_induct +rep_datatype "()" by simp lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()" by simp @@ -252,10 +246,6 @@ obtains x y where "p = (x, y)" using surj_pair [of p] by blast - -lemma prod_induct [induct type: *]: "(\a b. P (a, b)) \ P x" - by (cases x) simp - lemma ProdI: "Pair_Rep a b \ Prod" unfolding Prod_def by rule+ @@ -276,8 +266,14 @@ apply (assumption | rule ProdI)+ done -lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')" - by (blast elim!: Pair_inject) +rep_datatype (prod) Pair +proof - + fix P p + assume "\x y. P (x, y)" + then show "P p" by (cases p) simp +qed (auto elim: Pair_inject) + +lemmas Pair_eq = prod.inject lemma fst_conv [simp, code]: "fst (a, b) = a" unfolding fst_def by blast @@ -285,10 +281,6 @@ lemma snd_conv [simp, code]: "snd (a, b) = b" unfolding snd_def by blast -rep_datatype prod - inject Pair_eq - induction prod_induct - subsubsection {* Basic rules and proof tools *} @@ -1053,7 +1045,7 @@ val PairE = thm "PairE"; val Pair_Rep_inject = thm "Pair_Rep_inject"; val Pair_def = thm "Pair_def"; -val Pair_eq = thm "Pair_eq"; +val Pair_eq = @{thm "prod.inject"}; val Pair_fst_snd_eq = thm "Pair_fst_snd_eq"; val ProdI = thm "ProdI"; val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq"; @@ -1100,7 +1092,7 @@ val prod_fun_ident = thm "prod_fun_ident"; val prod_fun_imageE = thm "prod_fun_imageE"; val prod_fun_imageI = thm "prod_fun_imageI"; -val prod_induct = thm "prod_induct"; +val prod_induct = thm "prod.induct"; val snd_conv = thm "snd_conv"; val snd_def = thm "snd_def"; val snd_eqD = thm "snd_eqD"; diff -r d8549f4d900b -r 791607529f6d src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Sum_Type.thy Tue Jun 10 15:30:33 2008 +0200 @@ -171,9 +171,6 @@ apply (auto simp add: Sum_def Inl_def Inr_def) done -lemma sum_induct: "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x" -by (rule sumE [of x], auto) - lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV" apply (rule set_ext) @@ -237,7 +234,6 @@ val InrI = thm "InrI"; val PlusE = thm "PlusE"; val sumE = thm "sumE"; -val sum_induct = thm "sum_induct"; val Part_eqI = thm "Part_eqI"; val PartI = thm "PartI"; val PartE = thm "PartE"; diff -r d8549f4d900b -r 791607529f6d src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/TLA/Action.thy Tue Jun 10 15:30:33 2008 +0200 @@ -80,7 +80,7 @@ lemma actionI [intro!]: assumes "!!s t. (s,t) |= A" shows "|- A" - apply (rule assms intI prod_induct)+ + apply (rule assms intI prod.induct)+ done lemma actionD [dest]: "|- A ==> (s,t) |= A" diff -r d8549f4d900b -r 791607529f6d src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue Jun 10 15:30:33 2008 +0200 @@ -20,36 +20,25 @@ -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a} -> (string * sort) list -> string list -> (string * (string * 'a list) list) list - val induct_tac : string -> int -> tactic - val induct_thm_tac : thm -> string -> int -> tactic + val induct_tac : Proof.context -> string -> int -> tactic + val induct_thm_tac : Proof.context -> thm -> string -> int -> tactic val case_tac : string -> int -> tactic val distinct_simproc : simproc val make_case : Proof.context -> bool -> string list -> term -> (term * term) list -> term * (term * (int * bool)) list val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option val interpretation : (string list -> theory -> theory) -> theory -> theory - val rep_datatype_i : string list option -> (thm list * attribute list) list list -> - (thm list * attribute list) list list -> (thm list * attribute list) -> - theory -> - {distinct : thm list list, + val rep_datatype : ({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, - simps : thm list} * theory - val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list -> - (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> 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, - simps : thm list} * theory - val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix * + simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list + -> theory -> Proof.state; + val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state; + val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix * (bstring * typ list * mixfix) list) list -> theory -> {distinct : thm list list, inject : thm list list, @@ -59,7 +48,7 @@ split_thms : (thm * thm) list, induction : thm, simps : thm list} * theory - val add_datatype : bool -> string list -> (string list * bstring * mixfix * + val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix * (bstring * string list * mixfix) list) list -> theory -> {distinct : thm list list, inject : thm list list, @@ -221,7 +210,7 @@ in -fun gen_induct_tac inst_tac (varss, opt_rule) i state = +fun gen_induct_tac inst_tac ctxt (varss, opt_rule) i state = SUBGOAL (fn (Bi,_) => let val (rule, rule_name) = @@ -230,7 +219,9 @@ | NONE => let val tn = find_tname (hd (map_filter I (flat varss))) Bi val thy = Thm.theory_of_thm state - in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn) + in case Induct.lookup_inductT ctxt tn of + SOME thm => (thm, "Induction rule for type " ^ tn) + | NONE => error ("No induction rule for type " ^ tn) end val concls = HOLogic.dest_concls (Thm.concl_of rule); val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths => @@ -238,12 +229,12 @@ in occs_in_prems (inst_tac insts rule) (map #2 insts) i end) i state; -fun induct_tac s = - gen_induct_tac Tactic.res_inst_tac' +fun induct_tac ctxt s = + gen_induct_tac Tactic.res_inst_tac' ctxt (map (single o SOME) (Syntax.read_idents s), NONE); -fun induct_thm_tac th s = - gen_induct_tac Tactic.res_inst_tac' +fun induct_thm_tac ctxt th s = + gen_induct_tac Tactic.res_inst_tac' ctxt ([map SOME (Syntax.read_idents s)], SOME th); end; @@ -284,7 +275,7 @@ val inst_tac = RuleInsts.bires_inst_tac false; fun induct_meth ctxt (varss, opt_rule) = - gen_induct_tac (inst_tac ctxt) (varss, opt_rule); + gen_induct_tac (inst_tac ctxt) ctxt (varss, opt_rule); fun case_meth ctxt (varss, opt_rule) = gen_case_tac (inst_tac ctxt) (varss, opt_rule); @@ -545,57 +536,32 @@ (*********************** declare existing type as datatype *********************) -fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 = +fun prove_rep_datatype alt_names new_type_names descr sorts induct inject distinct thy = let - val (((distinct, inject), [induction]), thy1) = - thy0 - |> fold_map apply_theorems raw_distinct - ||>> fold_map apply_theorems raw_inject - ||>> apply_theorems [raw_induction]; - - val ((_, [induction']), _) = - Variable.importT_thms [induction] (Variable.thm_context induction); + val ((_, [induct']), _) = + Variable.importT_thms [induct] (Variable.thm_context induct); fun err t = error ("Ill-formed predicate in induction rule: " ^ - Syntax.string_of_term_global thy1 t); + Syntax.string_of_term_global thy t); fun get_typ (t as _ $ Var (_, Type (tname, Ts))) = ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t) | get_typ t = err t; - - val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction'))); - val new_type_names = getOpt (alt_names, map fst dtnames); + val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct'))); - 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 thy1; + val dt_info = get_datatypes thy; val (case_names_induct, case_names_exhausts) = (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames)); val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); - val (casedist_thms, thy2) = thy1 |> - DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction + val (casedist_thms, thy2) = thy |> + DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct case_names_exhausts; val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms false new_type_names [descr] sorts dt_info inject distinct - (Simplifier.theory_context thy2 dist_ss) induction thy2; + (Simplifier.theory_context thy2 dist_ss) induct thy2; val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false new_type_names [descr] sorts reccomb_names rec_thms thy3; val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms @@ -607,14 +573,14 @@ val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names [descr] sorts thy7; - val ((_, [induction']), thy10) = + val ((_, [induct']), thy10) = thy8 |> store_thmss "inject" new_type_names inject ||>> store_thmss "distinct" new_type_names distinct ||> Sign.add_path (space_implode "_" new_type_names) - ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])]; + ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])]; - val dt_infos = map (make_dt_info alt_names descr sorts induction' reccomb_names rec_thms) + val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms) ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); @@ -626,7 +592,7 @@ |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs)) |> put_dt_infos dt_infos - |> add_cases_induct dt_infos induction' + |> add_cases_induct dt_infos induct' |> Sign.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd @@ -638,12 +604,77 @@ rec_thms = rec_thms, case_thms = case_thms, split_thms = split_thms, - induction = induction', + induction = induct', simps = simps}, thy11) end; -val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems; -val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i; +fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy = + let + fun constr_of_term (Const (c, T)) = (c, T) + | constr_of_term t = + error ("Not a constant: " ^ Syntax.string_of_term_global thy t); + fun no_constr (c, T) = error ("Bad constructor: " + ^ Sign.extern_const thy c ^ "::" + ^ Syntax.string_of_typ_global thy T); + fun type_of_constr (cT as (_, T)) = + let + val frees = typ_tfrees T; + val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_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_datatypes thy) tyco then SOME tyco else NONE) raw_cs + of [] => () + | tycos => error ("Type(s) " ^ commas (map 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 + |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy)) + val sorts = map inter_sort ms; + val vs = Name.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 (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) + o fst o strip_type; + val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names); + + fun mk_spec (i, (tyco, constr)) = (i, (tyco, + map (DtTFree o fst) vs, + (map o apsnd) dtyps_of_typ constr)) + val descr = map_index mk_spec cs; + val injs = DatatypeProp.make_injs [descr] vs; + val distincts = map snd (DatatypeProp.make_distincts [descr] vs); + val ind = DatatypeProp.make_ind [descr] vs; + val rules = (map o map o map) Logic.close_form [[[ind]], injs, distincts]; + + fun after_qed' raw_thms = + let + val [[[induct]], injs, distincts] = + unflat rules (map Drule.zero_var_indexes_list raw_thms); + (*FIXME somehow dubious*) + in + ProofContext.theory_result + (prove_rep_datatype alt_names new_type_names descr vs induct injs distincts) + #-> after_qed + end; + in + thy + |> ProofContext.init + |> Proof.theorem_i 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 Sign.read_term (K I); @@ -719,8 +750,8 @@ case_names_induct case_names_exhausts thy end; -val add_datatype_i = gen_add_datatype cert_typ; -val add_datatype = gen_add_datatype read_typ true; +val add_datatype = gen_add_datatype cert_typ; +val add_datatype_cmd = gen_add_datatype read_typ true; (** a datatype antiquotation **) @@ -786,8 +817,6 @@ local structure P = OuterParse and K = OuterKeyword in -val _ = OuterSyntax.keywords ["distinct", "inject", "induction"]; - val datatype_decl = Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix -- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix)); @@ -797,24 +826,17 @@ val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args; val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in snd o add_datatype false names specs end; + in snd o add_datatype_cmd false names specs end; val _ = OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype)); - -val rep_datatype_decl = - Scan.option (Scan.repeat1 P.name) -- - Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] -- - Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] -- - (P.$$$ "induction" |-- P.!!! SpecParse.xthm); - -fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind; - val _ = - OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl - (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype)); + OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal + (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term + >> (fn (alt_names, ts) => Toplevel.print + o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts))); val _ = ThyOutput.add_commands [("datatype", @@ -822,6 +844,5 @@ end; - end; diff -r d8549f4d900b -r 791607529f6d src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Jun 10 15:30:33 2008 +0200 @@ -57,7 +57,7 @@ val eq_reflection = thm "eq_reflection"; val rec_UNIV_I = thm "rec_UNIV_I"; val rec_True_simp = thm "rec_True_simp"; -val Pair_eq = thm "Product_Type.Pair_eq"; +val Pair_eq = thm "Product_Type.prod.inject"; val atomize_all = thm "HOL.atomize_all"; val atomize_imp = thm "HOL.atomize_imp"; val meta_allE = thm "Pure.meta_allE"; @@ -2057,7 +2057,7 @@ in prove_standard [assm] concl (fn {prems, ...} => try_param_tac rN induct_scheme 1 - THEN try_param_tac "more" @{thm unit_induct} 1 + THEN try_param_tac "more" @{thm unit.induct} 1 THEN resolve_tac prems 1) end; val induct = timeit_msg "record induct proof:" induct_prf; diff -r d8549f4d900b -r 791607529f6d src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Tue Jun 10 15:30:06 2008 +0200 +++ b/src/HOLCF/Lift.thy Tue Jun 10 15:30:33 2008 +0200 @@ -25,15 +25,6 @@ subsection {* Lift as a datatype *} -lemma lift_distinct1: "\ \ Def x" -by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) - -lemma lift_distinct2: "Def x \ \" -by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) - -lemma Def_inject: "(Def x = Def y) = (x = y)" -by (simp add: Def_def Abs_lift_inject lift_def) - lemma lift_induct: "\P \; \x. P (Def x)\ \ P y" apply (induct y) apply (rule_tac p=y in upE) @@ -42,13 +33,13 @@ apply (simp add: Def_def) done -rep_datatype lift - distinct lift_distinct1 lift_distinct2 - inject Def_inject - induction lift_induct +rep_datatype "\\'a lift" Def + by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo) -lemma Def_not_UU: "Def a \ UU" - by simp +lemmas lift_distinct1 = lift.distinct(1) +lemmas lift_distinct2 = lift.distinct(2) +lemmas Def_not_UU = lift.distinct(2) +lemmas Def_inject = lift.inject text {* @{term UU} and @{term Def} *}