src/HOL/GCD.thy
changeset 35644 d20cf282342e
parent 35368 19b340c3f1ff
child 35726 059d2f7b979f
equal deleted inserted replaced
35643:965c24dd6856 35644:d20cf282342e
    97 lemma transfer_nat_int_gcd_closures:
    97 lemma transfer_nat_int_gcd_closures:
    98   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
    98   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
    99   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
    99   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   100   by (auto simp add: gcd_int_def lcm_int_def)
   100   by (auto simp add: gcd_int_def lcm_int_def)
   101 
   101 
   102 declare TransferMorphism_nat_int[transfer add return:
   102 declare transfer_morphism_nat_int[transfer add return:
   103     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   103     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   104 
   104 
   105 lemma transfer_int_nat_gcd:
   105 lemma transfer_int_nat_gcd:
   106   "gcd (int x) (int y) = int (gcd x y)"
   106   "gcd (int x) (int y) = int (gcd x y)"
   107   "lcm (int x) (int y) = int (lcm x y)"
   107   "lcm (int x) (int y) = int (lcm x y)"
   110 lemma transfer_int_nat_gcd_closures:
   110 lemma transfer_int_nat_gcd_closures:
   111   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   111   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   112   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   112   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   113   by (auto simp add: gcd_int_def lcm_int_def)
   113   by (auto simp add: gcd_int_def lcm_int_def)
   114 
   114 
   115 declare TransferMorphism_int_nat[transfer add return:
   115 declare transfer_morphism_int_nat[transfer add return:
   116     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   116     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   117 
   117 
   118 
   118 
   119 subsection {* GCD properties *}
   119 subsection {* GCD properties *}
   120 
   120