src/HOL/GCD.thy
changeset 42871 1c0b99f950d9
parent 41792 ff3cb0c418b7
child 44278 1220ecb81e8f
     1.1 --- a/src/HOL/GCD.thy	Fri May 20 08:16:56 2011 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri May 20 11:44:16 2011 +0200
     1.3 @@ -1436,16 +1436,16 @@
     1.4  lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
     1.5  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
     1.6  
     1.7 -lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
     1.8 +lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
     1.9  proof qed (auto simp add: gcd_ac_nat)
    1.10  
    1.11 -lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
    1.12 +lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
    1.13  proof qed (auto simp add: gcd_ac_int)
    1.14  
    1.15 -lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
    1.16 +lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
    1.17  proof qed (auto simp add: lcm_ac_nat)
    1.18  
    1.19 -lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
    1.20 +lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
    1.21  proof qed (auto simp add: lcm_ac_int)
    1.22  
    1.23  
    1.24 @@ -1516,8 +1516,8 @@
    1.25    assumes "finite N"
    1.26    shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
    1.27  proof -
    1.28 -  interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
    1.29 -    by (rule fun_left_comm_idem_lcm_nat)
    1.30 +  interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat"
    1.31 +    by (rule comp_fun_idem_lcm_nat)
    1.32    from assms show ?thesis by(simp add: Lcm_def)
    1.33  qed
    1.34  
    1.35 @@ -1525,8 +1525,8 @@
    1.36    assumes "finite N"
    1.37    shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
    1.38  proof -
    1.39 -  interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
    1.40 -    by (rule fun_left_comm_idem_lcm_int)
    1.41 +  interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int"
    1.42 +    by (rule comp_fun_idem_lcm_int)
    1.43    from assms show ?thesis by(simp add: Lcm_def)
    1.44  qed
    1.45  
    1.46 @@ -1534,8 +1534,8 @@
    1.47    assumes "finite N"
    1.48    shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
    1.49  proof -
    1.50 -  interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
    1.51 -    by (rule fun_left_comm_idem_gcd_nat)
    1.52 +  interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat"
    1.53 +    by (rule comp_fun_idem_gcd_nat)
    1.54    from assms show ?thesis by(simp add: Gcd_def)
    1.55  qed
    1.56  
    1.57 @@ -1543,8 +1543,8 @@
    1.58    assumes "finite N"
    1.59    shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
    1.60  proof -
    1.61 -  interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
    1.62 -    by (rule fun_left_comm_idem_gcd_int)
    1.63 +  interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int"
    1.64 +    by (rule comp_fun_idem_gcd_int)
    1.65    from assms show ?thesis by(simp add: Gcd_def)
    1.66  qed
    1.67  
    1.68 @@ -1685,28 +1685,28 @@
    1.69  lemma Lcm_set_nat [code_unfold]:
    1.70    "Lcm (set ns) = foldl lcm (1::nat) ns"
    1.71  proof -
    1.72 -  interpret fun_left_comm_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_lcm_nat)
    1.73 +  interpret comp_fun_idem "lcm::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_lcm_nat)
    1.74    show ?thesis by(simp add: Lcm_def fold_set lcm_commute_nat)
    1.75  qed
    1.76  
    1.77  lemma Lcm_set_int [code_unfold]:
    1.78    "Lcm (set is) = foldl lcm (1::int) is"
    1.79  proof -
    1.80 -  interpret fun_left_comm_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_lcm_int)
    1.81 +  interpret comp_fun_idem "lcm::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_lcm_int)
    1.82    show ?thesis by(simp add: Lcm_def fold_set lcm_commute_int)
    1.83  qed
    1.84  
    1.85  lemma Gcd_set_nat [code_unfold]:
    1.86    "Gcd (set ns) = foldl gcd (0::nat) ns"
    1.87  proof -
    1.88 -  interpret fun_left_comm_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule fun_left_comm_idem_gcd_nat)
    1.89 +  interpret comp_fun_idem "gcd::nat\<Rightarrow>nat\<Rightarrow>nat" by (rule comp_fun_idem_gcd_nat)
    1.90    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_nat)
    1.91  qed
    1.92  
    1.93  lemma Gcd_set_int [code_unfold]:
    1.94    "Gcd (set ns) = foldl gcd (0::int) ns"
    1.95  proof -
    1.96 -  interpret fun_left_comm_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule fun_left_comm_idem_gcd_int)
    1.97 +  interpret comp_fun_idem "gcd::int\<Rightarrow>int\<Rightarrow>int" by (rule comp_fun_idem_gcd_int)
    1.98    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
    1.99  qed
   1.100