adjustions to due to instance target
authorhaftmann
Fri Nov 30 20:13:03 2007 +0100 (2007-11-30)
changeset 2551038c15efe603b
parent 25509 e537c91b043d
child 25511 54db9b5080b8
adjustions to due to instance target
NEWS
src/HOL/Inductive.thy
src/HOL/Lattices.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Set.thy
src/HOL/Tools/inductive_package.ML
     1.1 --- a/NEWS	Fri Nov 30 16:23:52 2007 +0100
     1.2 +++ b/NEWS	Fri Nov 30 20:13:03 2007 +0100
     1.3 @@ -16,7 +16,13 @@
     1.4  
     1.5  * Library/Multiset: {#a, b, c#} is new short syntax for {#a#} + {#b#} + {#c#}.
     1.6  
     1.7 -* Constant "card" now with authentic syntax.
     1.8 +* Constants "card", "internal_split",  "option_map" now with authentic syntax.
     1.9 +
    1.10 +* Definitions subset_def, psubset_def, set_diff_def, Compl_def, le_bool_def,
    1.11 +less_bool_def, le_fun_def, less_fun_def, inf_bool_def, sup_bool_def,
    1.12 +Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, Inf_fun_def, Sup_fun_def,
    1.13 +inf_set_def, sup_set_def, Inf_set_def, Sup_set_def, le_def, less_def,
    1.14 +option_map_def now with object equality.
    1.15  
    1.16  
    1.17  
     2.1 --- a/src/HOL/Inductive.thy	Fri Nov 30 16:23:52 2007 +0100
     2.2 +++ b/src/HOL/Inductive.thy	Fri Nov 30 20:13:03 2007 +0100
     2.3 @@ -290,8 +290,10 @@
     2.4  val def_gfp_unfold = @{thm def_gfp_unfold}
     2.5  val def_lfp_induct = @{thm def_lfp_induct}
     2.6  val def_coinduct = @{thm def_coinduct}
     2.7 -val inf_bool_eq = @{thm inf_bool_eq}
     2.8 -val inf_fun_eq = @{thm inf_fun_eq}
     2.9 +val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
    2.10 +val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
    2.11 +val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
    2.12 +val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
    2.13  val le_boolI = @{thm le_boolI}
    2.14  val le_boolI' = @{thm le_boolI'}
    2.15  val le_funI = @{thm le_funI}
    2.16 @@ -299,8 +301,8 @@
    2.17  val le_funE = @{thm le_funE}
    2.18  val le_boolD = @{thm le_boolD}
    2.19  val le_funD = @{thm le_funD}
    2.20 -val le_bool_def = @{thm le_bool_def}
    2.21 -val le_fun_def = @{thm le_fun_def}
    2.22 +val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
    2.23 +val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
    2.24  *}
    2.25  
    2.26  use "Tools/inductive_package.ML"
     3.1 --- a/src/HOL/Lattices.thy	Fri Nov 30 16:23:52 2007 +0100
     3.2 +++ b/src/HOL/Lattices.thy	Fri Nov 30 20:13:03 2007 +0100
     3.3 @@ -479,16 +479,34 @@
     3.4  
     3.5  subsection {* Bool as lattice *}
     3.6  
     3.7 -instance bool :: distrib_lattice
     3.8 -  inf_bool_eq: "P \<sqinter> Q \<equiv> P \<and> Q"
     3.9 -  sup_bool_eq: "P \<squnion> Q \<equiv> P \<or> Q"
    3.10 +instantiation bool :: distrib_lattice
    3.11 +begin
    3.12 +
    3.13 +definition
    3.14 +  inf_bool_eq: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
    3.15 +
    3.16 +definition
    3.17 +  sup_bool_eq: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
    3.18 +
    3.19 +instance
    3.20    by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
    3.21  
    3.22 -instance bool :: complete_lattice
    3.23 -  Inf_bool_def: "\<Sqinter>A \<equiv> \<forall>x\<in>A. x"
    3.24 -  Sup_bool_def: "\<Squnion>A \<equiv> \<exists>x\<in>A. x"
    3.25 +end
    3.26 +
    3.27 +instantiation bool :: complete_lattice
    3.28 +begin
    3.29 +
    3.30 +definition
    3.31 +  Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    3.32 +
    3.33 +definition
    3.34 +  Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    3.35 +
    3.36 +instance
    3.37    by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
    3.38  
    3.39 +end
    3.40 +
    3.41  lemma Inf_empty_bool [simp]:
    3.42    "\<Sqinter>{}"
    3.43    unfolding Inf_bool_def by auto
    3.44 @@ -506,12 +524,19 @@
    3.45  
    3.46  subsection {* Set as lattice *}
    3.47  
    3.48 -instance set :: (type) distrib_lattice
    3.49 -  inf_set_eq: "A \<sqinter> B \<equiv> A \<inter> B"
    3.50 -  sup_set_eq: "A \<squnion> B \<equiv> A \<union> B"
    3.51 +instantiation set :: (type) distrib_lattice
    3.52 +begin
    3.53 +
    3.54 +definition
    3.55 +  inf_set_eq [code func del]: "A \<sqinter> B = A \<inter> B"
    3.56 +
    3.57 +definition
    3.58 +  sup_set_eq [code func del]: "A \<squnion> B = A \<union> B"
    3.59 +
    3.60 +instance
    3.61    by intro_classes (auto simp add: inf_set_eq sup_set_eq)
    3.62  
    3.63 -lemmas [code func del] = inf_set_eq sup_set_eq
    3.64 +end
    3.65  
    3.66  lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
    3.67    apply (fold inf_set_eq sup_set_eq)
    3.68 @@ -523,12 +548,19 @@
    3.69    apply (erule mono_sup)
    3.70    done
    3.71  
    3.72 -instance set :: (type) complete_lattice
    3.73 -  Inf_set_def: "\<Sqinter>S \<equiv> \<Inter>S"
    3.74 -  Sup_set_def: "\<Squnion>S \<equiv> \<Union>S"
    3.75 +instantiation set :: (type) complete_lattice
    3.76 +begin
    3.77 +
    3.78 +definition
    3.79 +  Inf_set_def [code func del]: "\<Sqinter>S \<equiv> \<Inter>S"
    3.80 +
    3.81 +definition
    3.82 +  Sup_set_def [code func del]: "\<Squnion>S \<equiv> \<Union>S"
    3.83 +
    3.84 +instance
    3.85    by intro_classes (auto simp add: Inf_set_def Sup_set_def)
    3.86  
    3.87 -lemmas [code func del] = Inf_set_def Sup_set_def
    3.88 +end
    3.89  
    3.90  lemma top_set_eq: "top = UNIV"
    3.91    by (iprover intro!: subset_antisym subset_UNIV top_greatest)
    3.92 @@ -539,9 +571,16 @@
    3.93  
    3.94  subsection {* Fun as lattice *}
    3.95  
    3.96 -instance "fun" :: (type, lattice) lattice
    3.97 -  inf_fun_eq: "f \<sqinter> g \<equiv> (\<lambda>x. f x \<sqinter> g x)"
    3.98 -  sup_fun_eq: "f \<squnion> g \<equiv> (\<lambda>x. f x \<squnion> g x)"
    3.99 +instantiation "fun" :: (type, lattice) lattice
   3.100 +begin
   3.101 +
   3.102 +definition
   3.103 +  inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   3.104 +
   3.105 +definition
   3.106 +  sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   3.107 +
   3.108 +instance
   3.109  apply intro_classes
   3.110  unfolding inf_fun_eq sup_fun_eq
   3.111  apply (auto intro: le_funI)
   3.112 @@ -551,19 +590,26 @@
   3.113  apply (auto dest: le_funD)
   3.114  done
   3.115  
   3.116 -lemmas [code func del] = inf_fun_eq sup_fun_eq
   3.117 +end
   3.118  
   3.119  instance "fun" :: (type, distrib_lattice) distrib_lattice
   3.120    by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
   3.121  
   3.122 -instance "fun" :: (type, complete_lattice) complete_lattice
   3.123 -  Inf_fun_def: "\<Sqinter>A \<equiv> (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   3.124 -  Sup_fun_def: "\<Squnion>A \<equiv> (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   3.125 +instantiation "fun" :: (type, complete_lattice) complete_lattice
   3.126 +begin
   3.127 +
   3.128 +definition
   3.129 +  Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
   3.130 +
   3.131 +definition
   3.132 +  Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
   3.133 +
   3.134 +instance
   3.135    by intro_classes
   3.136      (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
   3.137        intro: Inf_lower Sup_upper Inf_greatest Sup_least)
   3.138  
   3.139 -lemmas [code func del] = Inf_fun_def Sup_fun_def
   3.140 +end
   3.141  
   3.142  lemma Inf_empty_fun:
   3.143    "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
     4.1 --- a/src/HOL/Nat.thy	Fri Nov 30 16:23:52 2007 +0100
     4.2 +++ b/src/HOL/Nat.thy	Fri Nov 30 20:13:03 2007 +0100
     4.3 @@ -54,9 +54,15 @@
     4.4  
     4.5  local
     4.6  
     4.7 -instance nat :: zero
     4.8 -  Zero_nat_def: "0 == Abs_Nat Zero_Rep" ..
     4.9 -lemmas [code func del] = Zero_nat_def
    4.10 +instantiation nat :: zero
    4.11 +begin
    4.12 +
    4.13 +definition Zero_nat_def [code func del]:
    4.14 +  "0 = Abs_Nat Zero_Rep"
    4.15 +
    4.16 +instance ..
    4.17 +
    4.18 +end
    4.19  
    4.20  defs
    4.21    Suc_def:      "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))"
    4.22 @@ -155,11 +161,18 @@
    4.23    pred_nat :: "(nat * nat) set" where
    4.24    "pred_nat = {(m, n). n = Suc m}"
    4.25  
    4.26 -instance nat :: ord
    4.27 -  less_def: "m < n == (m, n) : pred_nat^+"
    4.28 -  le_def:   "m \<le> (n::nat) == ~ (n < m)" ..
    4.29 +instantiation nat :: ord
    4.30 +begin
    4.31 +
    4.32 +definition
    4.33 +  less_def [code func del]: "m < n \<longleftrightarrow> (m, n) : pred_nat^+"
    4.34  
    4.35 -lemmas [code func del] = less_def le_def
    4.36 +definition
    4.37 +  le_def [code func del]:   "m \<le> (n\<Colon>nat) \<longleftrightarrow> \<not> n < m"
    4.38 +
    4.39 +instance ..
    4.40 +
    4.41 +end
    4.42  
    4.43  lemma wf_pred_nat: "wf pred_nat"
    4.44    apply (unfold wf_def pred_nat_def, clarify)
    4.45 @@ -1488,8 +1501,8 @@
    4.46  text {* the lattice order on @{typ nat} *}
    4.47  
    4.48  instance nat :: distrib_lattice
    4.49 -  "inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> min"
    4.50 -  "sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat \<equiv> max"
    4.51 +  "(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
    4.52 +  "(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
    4.53    by intro_classes
    4.54      (simp_all add: inf_nat_def sup_nat_def)
    4.55  
     5.1 --- a/src/HOL/Orderings.thy	Fri Nov 30 16:23:52 2007 +0100
     5.2 +++ b/src/HOL/Orderings.thy	Fri Nov 30 20:13:03 2007 +0100
     5.3 @@ -928,11 +928,19 @@
     5.4  
     5.5  subsection {* Order on bool *}
     5.6  
     5.7 -instance bool :: order 
     5.8 -  le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
     5.9 -  less_bool_def: "(P\<Colon>bool) < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
    5.10 +instantiation bool :: order 
    5.11 +begin
    5.12 +
    5.13 +definition
    5.14 +  le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    5.15 +
    5.16 +definition
    5.17 +  less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
    5.18 +
    5.19 +instance
    5.20    by intro_classes (auto simp add: le_bool_def less_bool_def)
    5.21 -lemmas [code func del] = le_bool_def less_bool_def
    5.22 +
    5.23 +end
    5.24  
    5.25  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
    5.26  by (simp add: le_bool_def)
    5.27 @@ -966,11 +974,18 @@
    5.28  
    5.29  subsection {* Order on functions *}
    5.30  
    5.31 -instance "fun" :: (type, ord) ord
    5.32 -  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
    5.33 -  less_fun_def: "(f\<Colon>'a \<Rightarrow> 'b) < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
    5.34 +instantiation "fun" :: (type, ord) ord
    5.35 +begin
    5.36 +
    5.37 +definition
    5.38 +  le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    5.39  
    5.40 -lemmas [code func del] = le_fun_def less_fun_def
    5.41 +definition
    5.42 +  less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
    5.43 +
    5.44 +instance ..
    5.45 +
    5.46 +end
    5.47  
    5.48  instance "fun" :: (type, order) order
    5.49    by default
     6.1 --- a/src/HOL/Set.thy	Fri Nov 30 16:23:52 2007 +0100
     6.2 +++ b/src/HOL/Set.thy	Fri Nov 30 20:13:03 2007 +0100
     6.3 @@ -143,10 +143,18 @@
     6.4    union/intersection symbol because this leads to problems with nested
     6.5    subscripts in Proof General. *}
     6.6  
     6.7 -instance set :: (type) ord
     6.8 -  subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
     6.9 -  psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
    6.10 -lemmas [code func del] = subset_def psubset_def
    6.11 +instantiation set :: (type) ord
    6.12 +begin
    6.13 +
    6.14 +definition
    6.15 +  subset_def [code func del]: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
    6.16 +
    6.17 +definition
    6.18 +  psubset_def [code func del]: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B"
    6.19 +
    6.20 +instance ..
    6.21 +
    6.22 +end
    6.23  
    6.24  abbreviation
    6.25    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    6.26 @@ -340,11 +348,18 @@
    6.27    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    6.28    Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
    6.29  
    6.30 -instance set :: (type) minus
    6.31 -  Compl_def:    "- A            == {x. ~x:A}"
    6.32 -  set_diff_def: "A - B          == {x. x:A & ~x:B}" ..
    6.33 -
    6.34 -lemmas [code func del] = Compl_def set_diff_def
    6.35 +instantiation set :: (type) minus
    6.36 +begin
    6.37 +
    6.38 +definition
    6.39 +  Compl_def [code func del]:    "- A   = {x. ~x:A}"
    6.40 +
    6.41 +definition
    6.42 +  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
    6.43 +
    6.44 +instance ..
    6.45 +
    6.46 +end
    6.47  
    6.48  defs
    6.49    Un_def:       "A Un B         == {x. x:A | x:B}"
     7.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Nov 30 16:23:52 2007 +0100
     7.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 30 20:13:03 2007 +0100
     7.3 @@ -746,7 +746,7 @@
     7.4           singleton (ProofContext.export
     7.5             (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
     7.6             (rotate_prems ~1 (ObjectLogic.rulify (rule_by_tactic
     7.7 -             (rewrite_tac [le_fun_def, le_bool_def, @{thm sup_fun_eq}, @{thm sup_bool_eq}] THEN
     7.8 +             (rewrite_tac [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq] THEN
     7.9                 fold_tac rec_preds_defs) (mono RS (fp_def RS def_coinduct)))))
    7.10         else
    7.11           prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def