src/HOL/Library/Product_Order.thy
changeset 60679 ade12ef2773c
parent 60580 7e741e22d7fc
child 61166 5976fe402824
     1.1 --- a/src/HOL/Library/Product_Order.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  qed
     1.5  
     1.6  instance prod :: (order, order) order
     1.7 -  by default auto
     1.8 +  by standard auto
     1.9  
    1.10  
    1.11  subsection \<open>Binary infimum and supremum\<close>
    1.12 @@ -57,8 +57,7 @@
    1.13  instantiation prod :: (inf, inf) inf
    1.14  begin
    1.15  
    1.16 -definition
    1.17 -  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
    1.18 +definition "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
    1.19  
    1.20  lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
    1.21    unfolding inf_prod_def by simp
    1.22 @@ -69,11 +68,12 @@
    1.23  lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
    1.24    unfolding inf_prod_def by simp
    1.25  
    1.26 -instance proof qed
    1.27 +instance ..
    1.28 +
    1.29  end
    1.30  
    1.31  instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
    1.32 -  by default auto
    1.33 +  by standard auto
    1.34  
    1.35  
    1.36  instantiation prod :: (sup, sup) sup
    1.37 @@ -91,16 +91,17 @@
    1.38  lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
    1.39    unfolding sup_prod_def by simp
    1.40  
    1.41 -instance proof qed
    1.42 +instance ..
    1.43 +
    1.44  end
    1.45  
    1.46  instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
    1.47 -  by default auto
    1.48 +  by standard auto
    1.49  
    1.50  instance prod :: (lattice, lattice) lattice ..
    1.51  
    1.52  instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
    1.53 -  by default (auto simp add: sup_inf_distrib1)
    1.54 +  by standard (auto simp add: sup_inf_distrib1)
    1.55  
    1.56  
    1.57  subsection \<open>Top and bottom elements\<close>
    1.58 @@ -125,7 +126,7 @@
    1.59    unfolding top_prod_def by simp
    1.60  
    1.61  instance prod :: (order_top, order_top) order_top
    1.62 -  by default (auto simp add: top_prod_def)
    1.63 +  by standard (auto simp add: top_prod_def)
    1.64  
    1.65  instantiation prod :: (bot, bot) bot
    1.66  begin
    1.67 @@ -147,12 +148,12 @@
    1.68    unfolding bot_prod_def by simp
    1.69  
    1.70  instance prod :: (order_bot, order_bot) order_bot
    1.71 -  by default (auto simp add: bot_prod_def)
    1.72 +  by standard (auto simp add: bot_prod_def)
    1.73  
    1.74  instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
    1.75  
    1.76  instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
    1.77 -  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
    1.78 +  by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
    1.79  
    1.80  
    1.81  subsection \<open>Complete lattice operations\<close>
    1.82 @@ -160,28 +161,28 @@
    1.83  instantiation prod :: (Inf, Inf) Inf
    1.84  begin
    1.85  
    1.86 -definition
    1.87 -  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
    1.88 +definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
    1.89  
    1.90 -instance proof qed
    1.91 +instance ..
    1.92 +
    1.93  end
    1.94  
    1.95  instantiation prod :: (Sup, Sup) Sup
    1.96  begin
    1.97  
    1.98 -definition
    1.99 -  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
   1.100 +definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
   1.101  
   1.102 -instance proof qed
   1.103 +instance ..
   1.104 +
   1.105  end
   1.106  
   1.107  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
   1.108      conditionally_complete_lattice
   1.109 -  by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
   1.110 +  by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
   1.111      INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
   1.112  
   1.113  instance prod :: (complete_lattice, complete_lattice) complete_lattice
   1.114 -  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   1.115 +  by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
   1.116      INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
   1.117  
   1.118  lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
   1.119 @@ -231,9 +232,8 @@
   1.120  
   1.121  (* Contribution: Alessandro Coglio *)
   1.122  
   1.123 -instance prod ::
   1.124 -  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   1.125 -proof (default, goals)
   1.126 +instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
   1.127 +proof (standard, goals)
   1.128    case 1
   1.129    then show ?case
   1.130      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)