rep_datatype command now takes list of constructors as input arguments
authorhaftmann
Tue Jun 10 15:30:33 2008 +0200 (2008-06-10)
changeset 27104791607529f6d
parent 27103 d8549f4d900b
child 27105 5f139027c365
rep_datatype command now takes list of constructors as input arguments
NEWS
src/HOL/Datatype.thy
src/HOL/HoareParallel/OG_Tactics.thy
src/HOL/Library/Code_Index.thy
src/HOL/MetisExamples/BT.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/TLA/Action.thy
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/record_package.ML
src/HOLCF/Lift.thy
     1.1 --- a/NEWS	Tue Jun 10 15:30:06 2008 +0200
     1.2 +++ b/NEWS	Tue Jun 10 15:30:33 2008 +0200
     1.3 @@ -1,6 +1,41 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +New
     1.8 +---
     1.9 +
    1.10 +*** Pure ***
    1.11 +
    1.12 +* 'instance': attached definitions now longer accepted.  INCOMPATIBILITY.
    1.13 +
    1.14 +* Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
    1.15 +
    1.16 +
    1.17 +*** HOL ***
    1.18 +
    1.19 +* 'rep_datatype': instead of theorem names the command now takes a list of terms
    1.20 +denoting the constructors of the type to be represented as datatype.  The
    1.21 +characteristic theorems have to be proven.  INCOMPATIBILITY.  Also observe that
    1.22 +the following theorems have disappeared in favour of existing ones:
    1.23 +    unit_induct                 ~> unit.induct
    1.24 +    prod_induct                 ~> prod.induct
    1.25 +    sum_induct                  ~> sum.induct
    1.26 +    Suc_Suc_eq                  ~> nat.inject
    1.27 +    Suc_not_Zero Zero_not_Suc   ~> nat.distinct
    1.28 +
    1.29 +* Tactics induct_tac and thm_induct_tac now take explicit context as arguments;
    1.30 +type-specific induction rules are identified by the 'induct' attribute rather
    1.31 +than querying the datatype package directly.  INCOMPATIBILITY.
    1.32 +
    1.33 +* 'Least' operator now restricted to class 'order' (and subclasses).
    1.34 +INCOMPATIBILITY.
    1.35 +
    1.36 +* Library/Nat_Infinity: added addition, numeral syntax and more instantiations
    1.37 +for algebraic structures.  Removed some duplicate theorems.  Changes in simp
    1.38 +rules.  INCOMPATIBILITY.
    1.39 +
    1.40 +
    1.41 +
    1.42  New in Isabelle2008 (June 2008)
    1.43  -------------------------------
    1.44  
    1.45 @@ -150,7 +185,7 @@
    1.46  reconstruction_modulus, reconstruction_sorts renamed
    1.47  sledgehammer_modulus, sledgehammer_sorts.  INCOMPATIBILITY.
    1.48  
    1.49 -* Method "induction_scheme" derives user-specified induction rules
    1.50 +* Method "induct_scheme" derives user-specified induction rules
    1.51  from well-founded induction and completeness of patterns. This factors
    1.52  out some operations that are done internally by the function package
    1.53  and makes them available separately.  See
     2.1 --- a/src/HOL/Datatype.thy	Tue Jun 10 15:30:06 2008 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Tue Jun 10 15:30:33 2008 +0200
     2.3 @@ -533,10 +533,13 @@
     2.4  
     2.5  subsection {* Representing sums *}
     2.6  
     2.7 -rep_datatype sum
     2.8 -  distinct Inl_not_Inr Inr_not_Inl
     2.9 -  inject Inl_eq Inr_eq
    2.10 -  induction sum_induct
    2.11 +rep_datatype (sum) Inl Inr
    2.12 +proof -
    2.13 +  fix P
    2.14 +  fix s :: "'a + 'b"
    2.15 +  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
    2.16 +  then show "P s" by (auto intro: sumE [of s])
    2.17 +qed simp_all
    2.18  
    2.19  lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    2.20    by (rule ext) (simp split: sum.split)
     3.1 --- a/src/HOL/HoareParallel/OG_Tactics.thy	Tue Jun 10 15:30:06 2008 +0200
     3.2 +++ b/src/HOL/HoareParallel/OG_Tactics.thy	Tue Jun 10 15:30:33 2008 +0200
     3.3 @@ -1,6 +1,7 @@
     3.4  header {* \section{Generation of Verification Conditions} *}
     3.5  
     3.6 -theory OG_Tactics imports OG_Hoare
     3.7 +theory OG_Tactics
     3.8 +imports OG_Hoare
     3.9  begin
    3.10  
    3.11  lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq
    3.12 @@ -268,7 +269,7 @@
    3.13  by auto
    3.14  lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
    3.15  lemmas my_simp_list = list_lemmas fst_conv snd_conv
    3.16 -not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc Suc_Suc_eq
    3.17 +not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
    3.18  Collect_mem_eq ball_simps option.simps primrecdef_list
    3.19  lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length
    3.20  
     4.1 --- a/src/HOL/Library/Code_Index.thy	Tue Jun 10 15:30:06 2008 +0200
     4.2 +++ b/src/HOL/Library/Code_Index.thy	Tue Jun 10 15:30:33 2008 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4  
     4.5  text {*
     4.6    Indices are isomorphic to HOL @{typ nat} but
     4.7 -  mapped to target-language builtin integers
     4.8 +  mapped to target-language builtin integers.
     4.9  *}
    4.10  
    4.11  subsection {* Datatype of indices *}
    4.12 @@ -74,35 +74,23 @@
    4.13  definition [simp]:
    4.14    "Suc_index k = index_of_nat (Suc (nat_of_index k))"
    4.15  
    4.16 -lemma index_induct: "P 0 \<Longrightarrow> (\<And>k. P k \<Longrightarrow> P (Suc_index k)) \<Longrightarrow> P k"
    4.17 +rep_datatype "0 \<Colon> index" Suc_index
    4.18  proof -
    4.19 +  fix P :: "index \<Rightarrow> bool"
    4.20 +  fix k :: index
    4.21    assume "P 0" then have init: "P (index_of_nat 0)" by simp
    4.22    assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
    4.23 -    then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat (n)))" .
    4.24 +    then have "\<And>n. P (index_of_nat n) \<Longrightarrow> P (Suc_index (index_of_nat n))" .
    4.25      then have step: "\<And>n. P (index_of_nat n) \<Longrightarrow> P (index_of_nat (Suc n))" by simp
    4.26    from init step have "P (index_of_nat (nat_of_index k))"
    4.27      by (induct "nat_of_index k") simp_all
    4.28    then show "P k" by simp
    4.29 -qed
    4.30 -
    4.31 -lemma Suc_not_Zero_index: "Suc_index k \<noteq> 0"
    4.32 -  by simp
    4.33 -
    4.34 -lemma Zero_not_Suc_index: "0 \<noteq> Suc_index k"
    4.35 -  by simp
    4.36 -
    4.37 -lemma Suc_Suc_index_eq: "Suc_index k = Suc_index l \<longleftrightarrow> k = l"
    4.38 -  by simp
    4.39 -
    4.40 -rep_datatype index
    4.41 -  distinct  Suc_not_Zero_index Zero_not_Suc_index
    4.42 -  inject    Suc_Suc_index_eq
    4.43 -  induction index_induct
    4.44 +qed simp_all
    4.45  
    4.46  lemmas [code func del] = index.recs index.cases
    4.47  
    4.48  declare index_case [case_names nat, cases type: index]
    4.49 -declare index_induct [case_names nat, induct type: index]
    4.50 +declare index.induct [case_names nat, induct type: index]
    4.51  
    4.52  lemma [code func]:
    4.53    "index_size = nat_of_index"
     5.1 --- a/src/HOL/MetisExamples/BT.thy	Tue Jun 10 15:30:06 2008 +0200
     5.2 +++ b/src/HOL/MetisExamples/BT.thy	Tue Jun 10 15:30:33 2008 +0200
     5.3 @@ -7,7 +7,9 @@
     5.4  
     5.5  header {* Binary trees *}
     5.6  
     5.7 -theory BT imports Main begin
     5.8 +theory BT
     5.9 +imports Main
    5.10 +begin
    5.11  
    5.12  
    5.13  datatype 'a bt =
    5.14 @@ -100,7 +102,7 @@
    5.15  lemma reflect_reflect_ident: "reflect (reflect t) = t"
    5.16    apply (induct t)
    5.17    apply (metis add_right_cancel reflect.simps(1));
    5.18 -  apply (metis Suc_Suc_eq reflect.simps(2))
    5.19 +  apply (metis reflect.simps(2))
    5.20    done
    5.21  
    5.22  ML {*ResAtp.problem_name := "BT__bt_map_ident"*}
     6.1 --- a/src/HOL/Nat.thy	Tue Jun 10 15:30:06 2008 +0200
     6.2 +++ b/src/HOL/Nat.thy	Tue Jun 10 15:30:33 2008 +0200
     6.3 @@ -43,12 +43,12 @@
     6.4  global
     6.5  
     6.6  typedef (open Nat)
     6.7 -  nat = "Collect Nat"
     6.8 -  by (rule exI, rule CollectI, rule Nat.Zero_RepI)
     6.9 +  nat = Nat
    6.10 +  by (rule exI, unfold mem_def, rule Nat.Zero_RepI)
    6.11  
    6.12  constdefs
    6.13 -  Suc :: "nat => nat"
    6.14 -  Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    6.15 +  Suc ::   "nat => nat"
    6.16 +  Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    6.17  
    6.18  local
    6.19  
    6.20 @@ -62,34 +62,32 @@
    6.21  
    6.22  end
    6.23  
    6.24 -lemma nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n"
    6.25 -  apply (unfold Zero_nat_def Suc_def)
    6.26 -  apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    6.27 -  apply (erule Rep_Nat [THEN CollectD, THEN Nat.induct])
    6.28 -  apply (iprover elim: Abs_Nat_inverse [OF CollectI, THEN subst])
    6.29 -  done
    6.30 +lemma Suc_not_Zero: "Suc m \<noteq> 0"
    6.31 +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]) 
    6.32 +done
    6.33  
    6.34 -lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
    6.35 -  by (simp add: Zero_nat_def Suc_def
    6.36 -    Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI Zero_RepI
    6.37 -      Suc_Rep_not_Zero_Rep)
    6.38 -
    6.39 -lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
    6.40 +lemma Zero_not_Suc: "0 \<noteq> Suc m"
    6.41    by (rule not_sym, rule Suc_not_Zero not_sym)
    6.42  
    6.43 -lemma inj_Suc[simp]: "inj_on Suc N"
    6.44 -  by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI
    6.45 -                inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    6.46 -
    6.47 -lemma Suc_Suc_eq [iff]: "Suc m = Suc n \<longleftrightarrow> m = n"
    6.48 -  by (rule inj_Suc [THEN inj_eq])
    6.49 +rep_datatype "0 \<Colon> nat" Suc
    6.50 +apply (unfold Zero_nat_def Suc_def)
    6.51 +apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
    6.52 +apply (erule Rep_Nat [unfolded mem_def, THEN Nat.induct])
    6.53 +apply (iprover elim: Abs_Nat_inverse [unfolded mem_def, THEN subst])
    6.54 +apply (simp_all add: Abs_Nat_inject [unfolded mem_def] Rep_Nat [unfolded mem_def]
    6.55 +  Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep [unfolded mem_def]
    6.56 +  Suc_Rep_not_Zero_Rep [unfolded mem_def, symmetric]
    6.57 +  inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject)
    6.58 +done
    6.59  
    6.60 -rep_datatype nat
    6.61 -  distinct  Suc_not_Zero Zero_not_Suc
    6.62 -  inject    Suc_Suc_eq
    6.63 -  induction nat_induct
    6.64 +lemma nat_induct [case_names 0 Suc, induct type: nat]:
    6.65 +  -- {* for backward compatibility -- naming of variables differs *}
    6.66 +  fixes n
    6.67 +  assumes "P 0"
    6.68 +    and "\<And>n. P n \<Longrightarrow> P (Suc n)"
    6.69 +  shows "P n"
    6.70 +  using assms by (rule nat.induct) 
    6.71  
    6.72 -declare nat.induct [case_names 0 Suc, induct type: nat]
    6.73  declare nat.exhaust [case_names 0 Suc, cases type: nat]
    6.74  
    6.75  lemmas nat_rec_0 = nat.recs(1)
    6.76 @@ -97,10 +95,13 @@
    6.77  
    6.78  lemmas nat_case_0 = nat.cases(1)
    6.79    and nat_case_Suc = nat.cases(2)
    6.80 -
    6.81 +   
    6.82  
    6.83  text {* Injectiveness and distinctness lemmas *}
    6.84  
    6.85 +lemma inj_Suc[simp]: "inj_on Suc N"
    6.86 +  by (simp add: inj_on_def)
    6.87 +
    6.88  lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R"
    6.89  by (rule notE, rule Suc_not_Zero)
    6.90  
    6.91 @@ -1245,7 +1246,7 @@
    6.92  
    6.93  definition
    6.94    Nats  :: "'a set" where
    6.95 -  "Nats = range of_nat"
    6.96 +  [code func del]: "Nats = range of_nat"
    6.97  
    6.98  notation (xsymbols)
    6.99    Nats  ("\<nat>")
     7.1 --- a/src/HOL/Product_Type.thy	Tue Jun 10 15:30:06 2008 +0200
     7.2 +++ b/src/HOL/Product_Type.thy	Tue Jun 10 15:30:33 2008 +0200
     7.3 @@ -17,9 +17,7 @@
     7.4  
     7.5  subsection {* @{typ bool} is a datatype *}
     7.6  
     7.7 -rep_datatype bool
     7.8 -  distinct True_not_False False_not_True
     7.9 -  induction bool_induct
    7.10 +rep_datatype True False by (auto intro: bool_induct)
    7.11  
    7.12  declare case_split [cases type: bool]
    7.13    -- "prefer plain propositional version"
    7.14 @@ -67,11 +65,7 @@
    7.15    Addsimprocs [unit_eq_proc];
    7.16  *}
    7.17  
    7.18 -lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
    7.19 -  by simp
    7.20 -
    7.21 -rep_datatype unit
    7.22 -  induction unit_induct
    7.23 +rep_datatype "()" by simp
    7.24  
    7.25  lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()"
    7.26    by simp
    7.27 @@ -252,10 +246,6 @@
    7.28    obtains x y where "p = (x, y)"
    7.29    using surj_pair [of p] by blast
    7.30  
    7.31 -
    7.32 -lemma prod_induct [induct type: *]: "(\<And>a b. P (a, b)) \<Longrightarrow> P x"
    7.33 -  by (cases x) simp
    7.34 -
    7.35  lemma ProdI: "Pair_Rep a b \<in> Prod"
    7.36    unfolding Prod_def by rule+
    7.37  
    7.38 @@ -276,8 +266,14 @@
    7.39    apply (assumption | rule ProdI)+
    7.40    done
    7.41  
    7.42 -lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')"
    7.43 -  by (blast elim!: Pair_inject)
    7.44 +rep_datatype (prod) Pair
    7.45 +proof -
    7.46 +  fix P p
    7.47 +  assume "\<And>x y. P (x, y)"
    7.48 +  then show "P p" by (cases p) simp
    7.49 +qed (auto elim: Pair_inject)
    7.50 +
    7.51 +lemmas Pair_eq = prod.inject
    7.52  
    7.53  lemma fst_conv [simp, code]: "fst (a, b) = a"
    7.54    unfolding fst_def by blast
    7.55 @@ -285,10 +281,6 @@
    7.56  lemma snd_conv [simp, code]: "snd (a, b) = b"
    7.57    unfolding snd_def by blast
    7.58  
    7.59 -rep_datatype prod
    7.60 -  inject Pair_eq
    7.61 -  induction prod_induct
    7.62 -
    7.63  
    7.64  subsubsection {* Basic rules and proof tools *}
    7.65  
    7.66 @@ -1053,7 +1045,7 @@
    7.67  val PairE = thm "PairE";
    7.68  val Pair_Rep_inject = thm "Pair_Rep_inject";
    7.69  val Pair_def = thm "Pair_def";
    7.70 -val Pair_eq = thm "Pair_eq";
    7.71 +val Pair_eq = @{thm "prod.inject"};
    7.72  val Pair_fst_snd_eq = thm "Pair_fst_snd_eq";
    7.73  val ProdI = thm "ProdI";
    7.74  val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq";
    7.75 @@ -1100,7 +1092,7 @@
    7.76  val prod_fun_ident = thm "prod_fun_ident";
    7.77  val prod_fun_imageE = thm "prod_fun_imageE";
    7.78  val prod_fun_imageI = thm "prod_fun_imageI";
    7.79 -val prod_induct = thm "prod_induct";
    7.80 +val prod_induct = thm "prod.induct";
    7.81  val snd_conv = thm "snd_conv";
    7.82  val snd_def = thm "snd_def";
    7.83  val snd_eqD = thm "snd_eqD";
     8.1 --- a/src/HOL/Sum_Type.thy	Tue Jun 10 15:30:06 2008 +0200
     8.2 +++ b/src/HOL/Sum_Type.thy	Tue Jun 10 15:30:33 2008 +0200
     8.3 @@ -171,9 +171,6 @@
     8.4  apply (auto simp add: Sum_def Inl_def Inr_def)
     8.5  done
     8.6  
     8.7 -lemma sum_induct: "[| !!x. P (Inl x); !!x. P (Inr x) |] ==> P x"
     8.8 -by (rule sumE [of x], auto)
     8.9 -
    8.10  
    8.11  lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
    8.12  apply (rule set_ext)
    8.13 @@ -237,7 +234,6 @@
    8.14  val InrI = thm "InrI";
    8.15  val PlusE = thm "PlusE";
    8.16  val sumE = thm "sumE";
    8.17 -val sum_induct = thm "sum_induct";
    8.18  val Part_eqI = thm "Part_eqI";
    8.19  val PartI = thm "PartI";
    8.20  val PartE = thm "PartE";
     9.1 --- a/src/HOL/TLA/Action.thy	Tue Jun 10 15:30:06 2008 +0200
     9.2 +++ b/src/HOL/TLA/Action.thy	Tue Jun 10 15:30:33 2008 +0200
     9.3 @@ -80,7 +80,7 @@
     9.4  lemma actionI [intro!]:
     9.5    assumes "!!s t. (s,t) |= A"
     9.6    shows "|- A"
     9.7 -  apply (rule assms intI prod_induct)+
     9.8 +  apply (rule assms intI prod.induct)+
     9.9    done
    9.10  
    9.11  lemma actionD [dest]: "|- A ==> (s,t) |= A"
    10.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 10 15:30:06 2008 +0200
    10.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 10 15:30:33 2008 +0200
    10.3 @@ -20,36 +20,25 @@
    10.4      -> {atom : typ -> 'a, dtyp : string -> 'a, rtyp : string -> 'a list -> 'a}
    10.5      -> (string * sort) list -> string list
    10.6      -> (string * (string * 'a list) list) list
    10.7 -  val induct_tac : string -> int -> tactic
    10.8 -  val induct_thm_tac : thm -> string -> int -> tactic
    10.9 +  val induct_tac : Proof.context -> string -> int -> tactic
   10.10 +  val induct_thm_tac : Proof.context -> thm -> string -> int -> tactic
   10.11    val case_tac : string -> int -> tactic
   10.12    val distinct_simproc : simproc
   10.13    val make_case :  Proof.context -> bool -> string list -> term ->
   10.14      (term * term) list -> term * (term * (int * bool)) list
   10.15    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   10.16    val interpretation : (string list -> theory -> theory) -> theory -> theory
   10.17 -  val rep_datatype_i : string list option -> (thm list * attribute list) list list ->
   10.18 -    (thm list * attribute list) list list -> (thm list * attribute list) ->
   10.19 -    theory ->
   10.20 -      {distinct : thm list list,
   10.21 +  val rep_datatype : ({distinct : thm list list,
   10.22         inject : thm list list,
   10.23         exhaustion : thm list,
   10.24         rec_thms : thm list,
   10.25         case_thms : thm list list,
   10.26         split_thms : (thm * thm) list,
   10.27         induction : thm,
   10.28 -       simps : thm list} * theory
   10.29 -  val rep_datatype : string list option -> (Facts.ref * Attrib.src list) list list ->
   10.30 -    (Facts.ref * Attrib.src list) list list -> Facts.ref * Attrib.src list -> theory ->
   10.31 -      {distinct : thm list list,
   10.32 -       inject : thm list list,
   10.33 -       exhaustion : thm list,
   10.34 -       rec_thms : thm list,
   10.35 -       case_thms : thm list list,
   10.36 -       split_thms : (thm * thm) list,
   10.37 -       induction : thm,
   10.38 -       simps : thm list} * theory
   10.39 -  val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
   10.40 +       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
   10.41 +    -> theory -> Proof.state;
   10.42 +  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
   10.43 +  val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
   10.44      (bstring * typ list * mixfix) list) list -> theory ->
   10.45        {distinct : thm list list,
   10.46         inject : thm list list,
   10.47 @@ -59,7 +48,7 @@
   10.48         split_thms : (thm * thm) list,
   10.49         induction : thm,
   10.50         simps : thm list} * theory
   10.51 -  val add_datatype : bool -> string list -> (string list * bstring * mixfix *
   10.52 +  val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
   10.53      (bstring * string list * mixfix) list) list -> theory ->
   10.54        {distinct : thm list list,
   10.55         inject : thm list list,
   10.56 @@ -221,7 +210,7 @@
   10.57  
   10.58  in
   10.59  
   10.60 -fun gen_induct_tac inst_tac (varss, opt_rule) i state =
   10.61 +fun gen_induct_tac inst_tac ctxt (varss, opt_rule) i state =
   10.62    SUBGOAL (fn (Bi,_) =>
   10.63    let
   10.64      val (rule, rule_name) =
   10.65 @@ -230,7 +219,9 @@
   10.66          | NONE =>
   10.67              let val tn = find_tname (hd (map_filter I (flat varss))) Bi
   10.68                  val thy = Thm.theory_of_thm state
   10.69 -            in (#induction (the_datatype thy tn), "Induction rule for type " ^ tn)
   10.70 +            in case Induct.lookup_inductT ctxt tn of
   10.71 +                SOME thm => (thm, "Induction rule for type " ^ tn)
   10.72 +              | NONE => error ("No induction rule for type " ^ tn)
   10.73              end
   10.74      val concls = HOLogic.dest_concls (Thm.concl_of rule);
   10.75      val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
   10.76 @@ -238,12 +229,12 @@
   10.77    in occs_in_prems (inst_tac insts rule) (map #2 insts) i end)
   10.78    i state;
   10.79  
   10.80 -fun induct_tac s =
   10.81 -  gen_induct_tac Tactic.res_inst_tac'
   10.82 +fun induct_tac ctxt s =
   10.83 +  gen_induct_tac Tactic.res_inst_tac' ctxt
   10.84      (map (single o SOME) (Syntax.read_idents s), NONE);
   10.85  
   10.86 -fun induct_thm_tac th s =
   10.87 -  gen_induct_tac Tactic.res_inst_tac'
   10.88 +fun induct_thm_tac ctxt th s =
   10.89 +  gen_induct_tac Tactic.res_inst_tac' ctxt
   10.90      ([map SOME (Syntax.read_idents s)], SOME th);
   10.91  
   10.92  end;
   10.93 @@ -284,7 +275,7 @@
   10.94  val inst_tac = RuleInsts.bires_inst_tac false;
   10.95  
   10.96  fun induct_meth ctxt (varss, opt_rule) =
   10.97 -  gen_induct_tac (inst_tac ctxt) (varss, opt_rule);
   10.98 +  gen_induct_tac (inst_tac ctxt) ctxt (varss, opt_rule);
   10.99  fun case_meth ctxt (varss, opt_rule) =
  10.100    gen_case_tac (inst_tac ctxt) (varss, opt_rule);
  10.101  
  10.102 @@ -545,57 +536,32 @@
  10.103  
  10.104  (*********************** declare existing type as datatype *********************)
  10.105  
  10.106 -fun gen_rep_datatype apply_theorems alt_names raw_distinct raw_inject raw_induction thy0 =
  10.107 +fun prove_rep_datatype alt_names new_type_names descr sorts induct inject distinct thy =
  10.108    let
  10.109 -    val (((distinct, inject), [induction]), thy1) =
  10.110 -      thy0
  10.111 -      |> fold_map apply_theorems raw_distinct
  10.112 -      ||>> fold_map apply_theorems raw_inject
  10.113 -      ||>> apply_theorems [raw_induction];
  10.114 -
  10.115 -    val ((_, [induction']), _) =
  10.116 -      Variable.importT_thms [induction] (Variable.thm_context induction);
  10.117 +    val ((_, [induct']), _) =
  10.118 +      Variable.importT_thms [induct] (Variable.thm_context induct);
  10.119  
  10.120      fun err t = error ("Ill-formed predicate in induction rule: " ^
  10.121 -      Syntax.string_of_term_global thy1 t);
  10.122 +      Syntax.string_of_term_global thy t);
  10.123  
  10.124      fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
  10.125            ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
  10.126        | get_typ t = err t;
  10.127 -
  10.128 -    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));
  10.129 -    val new_type_names = getOpt (alt_names, map fst dtnames);
  10.130 +    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
  10.131  
  10.132 -    fun get_constr t = (case Logic.strip_assums_concl t of
  10.133 -        _ $ (_ $ t') => (case head_of t' of
  10.134 -            Const (cname, cT) => (case strip_type cT of
  10.135 -                (Ts, Type (tname, _)) => (tname, (cname, map (dtyp_of_typ dtnames) Ts))
  10.136 -              | _ => err t)
  10.137 -          | _ => err t)
  10.138 -      | _ => err t);
  10.139 -
  10.140 -    fun make_dt_spec [] _ _ = []
  10.141 -      | make_dt_spec ((tname, tvs)::dtnames') i constrs =
  10.142 -          let val (constrs', constrs'') = take_prefix (equal tname o fst) constrs
  10.143 -          in (i, (tname, map DtTFree tvs, map snd constrs'))::
  10.144 -            (make_dt_spec dtnames' (i + 1) constrs'')
  10.145 -          end;
  10.146 -
  10.147 -    val descr = make_dt_spec dtnames 0 (map get_constr (prems_of induction'));
  10.148 -    val sorts = add_term_tfrees (concl_of induction', []);
  10.149 -    val dt_info = get_datatypes thy1;
  10.150 +    val dt_info = get_datatypes thy;
  10.151  
  10.152      val (case_names_induct, case_names_exhausts) =
  10.153        (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
  10.154  
  10.155      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
  10.156  
  10.157 -    val (casedist_thms, thy2) = thy1 |>
  10.158 -      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
  10.159 +    val (casedist_thms, thy2) = thy |>
  10.160 +      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
  10.161          case_names_exhausts;
  10.162      val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
  10.163        false new_type_names [descr] sorts dt_info inject distinct
  10.164 -      (Simplifier.theory_context thy2 dist_ss) induction thy2;
  10.165 +      (Simplifier.theory_context thy2 dist_ss) induct thy2;
  10.166      val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
  10.167        new_type_names [descr] sorts reccomb_names rec_thms thy3;
  10.168      val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
  10.169 @@ -607,14 +573,14 @@
  10.170      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
  10.171        [descr] sorts thy7;
  10.172  
  10.173 -    val ((_, [induction']), thy10) =
  10.174 +    val ((_, [induct']), thy10) =
  10.175        thy8
  10.176        |> store_thmss "inject" new_type_names inject
  10.177        ||>> store_thmss "distinct" new_type_names distinct
  10.178        ||> Sign.add_path (space_implode "_" new_type_names)
  10.179 -      ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
  10.180 +      ||>> PureThy.add_thms [(("induct", induct), [case_names_induct])];
  10.181  
  10.182 -    val dt_infos = map (make_dt_info alt_names descr sorts induction' reccomb_names rec_thms)
  10.183 +    val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
  10.184        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
  10.185          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
  10.186  
  10.187 @@ -626,7 +592,7 @@
  10.188        |> add_rules simps case_thms rec_thms inject distinct
  10.189             weak_case_congs (Simplifier.attrib (op addcongs))
  10.190        |> put_dt_infos dt_infos
  10.191 -      |> add_cases_induct dt_infos induction'
  10.192 +      |> add_cases_induct dt_infos induct'
  10.193        |> Sign.parent_path
  10.194        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
  10.195        |> snd
  10.196 @@ -638,12 +604,77 @@
  10.197        rec_thms = rec_thms,
  10.198        case_thms = case_thms,
  10.199        split_thms = split_thms,
  10.200 -      induction = induction',
  10.201 +      induction = induct',
  10.202        simps = simps}, thy11)
  10.203    end;
  10.204  
  10.205 -val rep_datatype = gen_rep_datatype IsarCmd.apply_theorems;
  10.206 -val rep_datatype_i = gen_rep_datatype IsarCmd.apply_theorems_i;
  10.207 +fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
  10.208 +  let
  10.209 +    fun constr_of_term (Const (c, T)) = (c, T)
  10.210 +      | constr_of_term t =
  10.211 +          error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
  10.212 +    fun no_constr (c, T) = error ("Bad constructor: "
  10.213 +      ^ Sign.extern_const thy c ^ "::"
  10.214 +      ^ Syntax.string_of_typ_global thy T);
  10.215 +    fun type_of_constr (cT as (_, T)) =
  10.216 +      let
  10.217 +        val frees = typ_tfrees T;
  10.218 +        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
  10.219 +          handle TYPE _ => no_constr cT
  10.220 +        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
  10.221 +        val _ = if length frees <> length vs then no_constr cT else ();
  10.222 +      in (tyco, (vs, cT)) end;
  10.223 +
  10.224 +    val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
  10.225 +    val _ = case map_filter (fn (tyco, _) =>
  10.226 +        if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
  10.227 +     of [] => ()
  10.228 +      | tycos => error ("Type(s) " ^ commas (map quote tycos)
  10.229 +          ^ " already represented inductivly");
  10.230 +    val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
  10.231 +    val ms = case distinct (op =) (map length raw_vss)
  10.232 +     of [n] => 0 upto n - 1
  10.233 +      | _ => error ("Different types in given constructors");
  10.234 +    fun inter_sort m = map (fn xs => nth xs m) raw_vss
  10.235 +      |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
  10.236 +    val sorts = map inter_sort ms;
  10.237 +    val vs = Name.names Name.context Name.aT sorts;
  10.238 +
  10.239 +    fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
  10.240 +      (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
  10.241 +
  10.242 +    val cs = map (apsnd (map norm_constr)) raw_cs;
  10.243 +    val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
  10.244 +      o fst o strip_type;
  10.245 +    val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names);
  10.246 +
  10.247 +    fun mk_spec (i, (tyco, constr)) = (i, (tyco,
  10.248 +      map (DtTFree o fst) vs,
  10.249 +      (map o apsnd) dtyps_of_typ constr))
  10.250 +    val descr = map_index mk_spec cs;
  10.251 +    val injs = DatatypeProp.make_injs [descr] vs;
  10.252 +    val distincts = map snd (DatatypeProp.make_distincts [descr] vs);
  10.253 +    val ind = DatatypeProp.make_ind [descr] vs;
  10.254 +    val rules = (map o map o map) Logic.close_form [[[ind]], injs, distincts];
  10.255 +
  10.256 +    fun after_qed' raw_thms =
  10.257 +      let
  10.258 +        val [[[induct]], injs, distincts] =
  10.259 +          unflat rules (map Drule.zero_var_indexes_list raw_thms);
  10.260 +            (*FIXME somehow dubious*)
  10.261 +      in
  10.262 +        ProofContext.theory_result
  10.263 +          (prove_rep_datatype alt_names new_type_names descr vs induct injs distincts)
  10.264 +        #-> after_qed
  10.265 +      end;
  10.266 +  in
  10.267 +    thy
  10.268 +    |> ProofContext.init
  10.269 +    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
  10.270 +  end;
  10.271 +
  10.272 +val rep_datatype = gen_rep_datatype Sign.cert_term;
  10.273 +val rep_datatype_cmd = gen_rep_datatype Sign.read_term (K I);
  10.274  
  10.275  
  10.276  
  10.277 @@ -719,8 +750,8 @@
  10.278        case_names_induct case_names_exhausts thy
  10.279    end;
  10.280  
  10.281 -val add_datatype_i = gen_add_datatype cert_typ;
  10.282 -val add_datatype = gen_add_datatype read_typ true;
  10.283 +val add_datatype = gen_add_datatype cert_typ;
  10.284 +val add_datatype_cmd = gen_add_datatype read_typ true;
  10.285  
  10.286  
  10.287  (** a datatype antiquotation **)
  10.288 @@ -786,8 +817,6 @@
  10.289  
  10.290  local structure P = OuterParse and K = OuterKeyword in
  10.291  
  10.292 -val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
  10.293 -
  10.294  val datatype_decl =
  10.295    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
  10.296      (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
  10.297 @@ -797,24 +826,17 @@
  10.298      val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
  10.299      val specs = map (fn ((((_, vs), t), mx), cons) =>
  10.300        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
  10.301 -  in snd o add_datatype false names specs end;
  10.302 +  in snd o add_datatype_cmd false names specs end;
  10.303  
  10.304  val _ =
  10.305    OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
  10.306      (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
  10.307  
  10.308 -
  10.309 -val rep_datatype_decl =
  10.310 -  Scan.option (Scan.repeat1 P.name) --
  10.311 -    Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
  10.312 -    Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
  10.313 -    (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
  10.314 -
  10.315 -fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
  10.316 -
  10.317  val _ =
  10.318 -  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
  10.319 -    (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
  10.320 +  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
  10.321 +    (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
  10.322 +      >> (fn (alt_names, ts) => Toplevel.print
  10.323 +           o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
  10.324  
  10.325  val _ =
  10.326    ThyOutput.add_commands [("datatype",
  10.327 @@ -822,6 +844,5 @@
  10.328  
  10.329  end;
  10.330  
  10.331 -
  10.332  end;
  10.333  
    11.1 --- a/src/HOL/Tools/record_package.ML	Tue Jun 10 15:30:06 2008 +0200
    11.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jun 10 15:30:33 2008 +0200
    11.3 @@ -57,7 +57,7 @@
    11.4  val eq_reflection = thm "eq_reflection";
    11.5  val rec_UNIV_I = thm "rec_UNIV_I";
    11.6  val rec_True_simp = thm "rec_True_simp";
    11.7 -val Pair_eq = thm "Product_Type.Pair_eq";
    11.8 +val Pair_eq = thm "Product_Type.prod.inject";
    11.9  val atomize_all = thm "HOL.atomize_all";
   11.10  val atomize_imp = thm "HOL.atomize_imp";
   11.11  val meta_allE = thm "Pure.meta_allE";
   11.12 @@ -2057,7 +2057,7 @@
   11.13        in
   11.14          prove_standard [assm] concl (fn {prems, ...} =>
   11.15            try_param_tac rN induct_scheme 1
   11.16 -          THEN try_param_tac "more" @{thm unit_induct} 1
   11.17 +          THEN try_param_tac "more" @{thm unit.induct} 1
   11.18            THEN resolve_tac prems 1)
   11.19        end;
   11.20      val induct = timeit_msg "record induct proof:" induct_prf;
    12.1 --- a/src/HOLCF/Lift.thy	Tue Jun 10 15:30:06 2008 +0200
    12.2 +++ b/src/HOLCF/Lift.thy	Tue Jun 10 15:30:33 2008 +0200
    12.3 @@ -25,15 +25,6 @@
    12.4  
    12.5  subsection {* Lift as a datatype *}
    12.6  
    12.7 -lemma lift_distinct1: "\<bottom> \<noteq> Def x"
    12.8 -by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
    12.9 -
   12.10 -lemma lift_distinct2: "Def x \<noteq> \<bottom>"
   12.11 -by (simp add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
   12.12 -
   12.13 -lemma Def_inject: "(Def x = Def y) = (x = y)"
   12.14 -by (simp add: Def_def Abs_lift_inject lift_def)
   12.15 -
   12.16  lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
   12.17  apply (induct y)
   12.18  apply (rule_tac p=y in upE)
   12.19 @@ -42,13 +33,13 @@
   12.20  apply (simp add: Def_def)
   12.21  done
   12.22  
   12.23 -rep_datatype lift
   12.24 -  distinct lift_distinct1 lift_distinct2
   12.25 -  inject Def_inject
   12.26 -  induction lift_induct
   12.27 +rep_datatype "\<bottom>\<Colon>'a lift" Def
   12.28 +  by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject lift_def inst_lift_pcpo)
   12.29  
   12.30 -lemma Def_not_UU: "Def a \<noteq> UU"
   12.31 -  by simp
   12.32 +lemmas lift_distinct1 = lift.distinct(1)
   12.33 +lemmas lift_distinct2 = lift.distinct(2)
   12.34 +lemmas Def_not_UU = lift.distinct(2)
   12.35 +lemmas Def_inject = lift.inject
   12.36  
   12.37  
   12.38  text {* @{term UU} and @{term Def} *}