avoid odd foundational terms after interpretation;
authorhaftmann
Tue Mar 26 22:09:39 2013 +0100 (2013-03-26)
changeset 51547604d73671fa7
parent 51546 2e26df807dc7
child 51548 757fa47af981
avoid odd foundational terms after interpretation;
more uniform code setup
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Tue Mar 26 21:53:56 2013 +0100
     1.2 +++ b/src/HOL/GCD.thy	Tue Mar 26 22:09:39 2013 +0100
     1.3 @@ -1545,24 +1545,30 @@
     1.4  qed simp
     1.5  
     1.6  interpretation gcd_lcm_complete_lattice_nat:
     1.7 -  complete_lattice Gcd Lcm gcd "op dvd" "\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m" lcm 1 0
     1.8 -proof
     1.9 -  case goal1 show ?case by simp
    1.10 -next
    1.11 -  case goal2 show ?case by simp
    1.12 -next
    1.13 -  case goal5 thus ?case by (rule dvd_Lcm_nat)
    1.14 -next
    1.15 -  case goal6 thus ?case by simp
    1.16 -next
    1.17 -  case goal3 thus ?case by (simp add: Gcd_nat_def)
    1.18 -next
    1.19 -  case goal4 thus ?case by (simp add: Gcd_nat_def)
    1.20 +  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
    1.21 +where
    1.22 +  "complete_lattice.INFI Gcd A f = Gcd (f ` A :: nat set)"
    1.23 +  and "complete_lattice.SUPR Lcm A f = Lcm (f ` A)"
    1.24 +proof -
    1.25 +  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.26 +  proof
    1.27 +    case goal1 show ?case by simp
    1.28 +  next
    1.29 +    case goal2 show ?case by simp
    1.30 +  next
    1.31 +    case goal5 thus ?case by (rule dvd_Lcm_nat)
    1.32 +  next
    1.33 +    case goal6 thus ?case by simp
    1.34 +  next
    1.35 +    case goal3 thus ?case by (simp add: Gcd_nat_def)
    1.36 +  next
    1.37 +    case goal4 thus ?case by (simp add: Gcd_nat_def)
    1.38 +  qed
    1.39 +  then interpret gcd_lcm_complete_lattice_nat:
    1.40 +    complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
    1.41 +  from gcd_lcm_complete_lattice_nat.INF_def show "complete_lattice.INFI Gcd A f = Gcd (f ` A)" .
    1.42 +  from gcd_lcm_complete_lattice_nat.SUP_def show "complete_lattice.SUPR Lcm A f = Lcm (f ` A)" .
    1.43  qed
    1.44 -(* bh: This interpretation generates many lemmas about
    1.45 -"complete_lattice.SUPR Lcm" and "complete_lattice.INFI Gcd".
    1.46 -Should we define binder versions of LCM and GCD to correspond
    1.47 -with these? *)
    1.48  
    1.49  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
    1.50    by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
    1.51 @@ -1717,11 +1723,12 @@
    1.52    using assms by (simp add: Gcd_int_def dvd_int_iff)
    1.53  
    1.54  lemma Lcm_set_int [code_unfold]:
    1.55 -  "Lcm (set xs) = foldl lcm (1::int) xs"
    1.56 +  "Lcm (set xs) = fold lcm xs (1::int)"
    1.57    by (induct xs rule: rev_induct, simp_all add: lcm_commute_int)
    1.58  
    1.59  lemma Gcd_set_int [code_unfold]:
    1.60 -  "Gcd (set xs) = foldl gcd (0::int) xs"
    1.61 +  "Gcd (set xs) = fold gcd xs (0::int)"
    1.62    by (induct xs rule: rev_induct, simp_all add: gcd_commute_int)
    1.63  
    1.64  end
    1.65 +