src/HOL/GCD.thy
changeset 60580 7e741e22d7fc
parent 60512 e0169291b31c
child 60596 54168997757f
     1.1 --- a/src/HOL/GCD.thy	Thu Jun 25 22:56:33 2015 +0200
     1.2 +++ b/src/HOL/GCD.thy	Thu Jun 25 23:33:47 2015 +0200
     1.3 @@ -1451,17 +1451,19 @@
     1.4  
     1.5  subsection {* The complete divisibility lattice *}
     1.6  
     1.7 -interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
     1.8 -proof
     1.9 -  case goal3 thus ?case by(metis gcd_unique_nat)
    1.10 +interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
    1.11 +proof (default, goals)
    1.12 +  case 3
    1.13 +  thus ?case by(metis gcd_unique_nat)
    1.14  qed auto
    1.15  
    1.16 -interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
    1.17 -proof
    1.18 -  case goal3 thus ?case by(metis lcm_unique_nat)
    1.19 +interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
    1.20 +proof (default, goals)
    1.21 +  case 3
    1.22 +  thus ?case by(metis lcm_unique_nat)
    1.23  qed auto
    1.24  
    1.25 -interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
    1.26 +interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
    1.27  
    1.28  text{* Lifting gcd and lcm to sets (Gcd/Lcm).
    1.29  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
    1.30 @@ -1522,23 +1524,28 @@
    1.31  
    1.32  interpretation gcd_lcm_complete_lattice_nat:
    1.33    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
    1.34 -where
    1.35 -  "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    1.36 +where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
    1.37    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    1.38  proof -
    1.39    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
    1.40 -  proof
    1.41 -    case goal1 thus ?case by (simp add: Gcd_nat_def)
    1.42 +  proof (default, goals)
    1.43 +    case 1
    1.44 +    thus ?case by (simp add: Gcd_nat_def)
    1.45    next
    1.46 -    case goal2 thus ?case by (simp add: Gcd_nat_def)
    1.47 +    case 2
    1.48 +    thus ?case by (simp add: Gcd_nat_def)
    1.49    next
    1.50 -    case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
    1.51 +    case 5
    1.52 +    show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
    1.53    next
    1.54 -    case goal6 show ?case by (simp add: Lcm_nat_empty)
    1.55 +    case 6
    1.56 +    show ?case by (simp add: Lcm_nat_empty)
    1.57    next
    1.58 -    case goal3 thus ?case by simp
    1.59 +    case 3
    1.60 +    thus ?case by simp
    1.61    next
    1.62 -    case goal4 thus ?case by simp
    1.63 +    case 4
    1.64 +    thus ?case by simp
    1.65    qed
    1.66    then interpret gcd_lcm_complete_lattice_nat:
    1.67      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .