--- 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
--- 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: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'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)
--- 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
--- 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 \<Longrightarrow> (\<And>k. P k \<Longrightarrow> P (Suc_index k)) \<Longrightarrow> P k"
+rep_datatype "0 \<Colon> index" Suc_index
proof -
+ fix P :: "index \<Rightarrow> bool"
+ fix k :: index
assume "P 0" then have init: "P (index_of_nat 0)" by simp
assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
- then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat (n)))" .
+ then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" .
then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> 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 \<noteq> 0"
- by simp
-
-lemma Zero_not_Suc_index: "0 \<noteq> Suc_index k"
- by simp
-
-lemma Suc_Suc_index_eq: "Suc_index k = Suc_index l \<longleftrightarrow> 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"
--- 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"*}
--- 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 \<noteq> 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 \<noteq> 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 \<noteq> Suc m"
+lemma Zero_not_Suc: "0 \<noteq> 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 \<longleftrightarrow> m = n"
- by (rule inj_Suc [THEN inj_eq])
+rep_datatype "0 \<Colon> 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 "\<And>n. P n \<Longrightarrow> 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 \<Longrightarrow> 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 ("\<nat>")
--- 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: *]: "(\<And>a b. P (a, b)) \<Longrightarrow> P x"
- by (cases x) simp
-
lemma ProdI: "Pair_Rep a b \<in> 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 "\<And>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";
--- 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";
--- 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"
--- 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;
--- 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;
--- 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: "\<bottom> \<noteq> Def x"
-by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
-
-lemma lift_distinct2: "Def x \<noteq> \<bottom>"
-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: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> 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 "\<bottom>\<Colon>'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 \<noteq> 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} *}