src/HOL/Number_Theory/Fib.thy
changeset 35644 d20cf282342e
parent 32479 521cc9bf2958
child 36350 bc7982c54e37
equal deleted inserted replaced
35643:965c24dd6856 35644:d20cf282342e
    67 
    67 
    68 lemma transfer_nat_int_fib_closure:
    68 lemma transfer_nat_int_fib_closure:
    69   "n >= (0::int) \<Longrightarrow> fib n >= 0"
    69   "n >= (0::int) \<Longrightarrow> fib n >= 0"
    70   by (auto simp add: fib_int_def)
    70   by (auto simp add: fib_int_def)
    71 
    71 
    72 declare TransferMorphism_nat_int[transfer add return: 
    72 declare transfer_morphism_nat_int[transfer add return: 
    73     transfer_nat_int_fib transfer_nat_int_fib_closure]
    73     transfer_nat_int_fib transfer_nat_int_fib_closure]
    74 
    74 
    75 lemma transfer_int_nat_fib:
    75 lemma transfer_int_nat_fib:
    76   "fib (int n) = int (fib n)"
    76   "fib (int n) = int (fib n)"
    77   unfolding fib_int_def by auto
    77   unfolding fib_int_def by auto
    78 
    78 
    79 lemma transfer_int_nat_fib_closure:
    79 lemma transfer_int_nat_fib_closure:
    80   "is_nat n \<Longrightarrow> fib n >= 0"
    80   "is_nat n \<Longrightarrow> fib n >= 0"
    81   unfolding fib_int_def by auto
    81   unfolding fib_int_def by auto
    82 
    82 
    83 declare TransferMorphism_int_nat[transfer add return: 
    83 declare transfer_morphism_int_nat[transfer add return: 
    84     transfer_int_nat_fib transfer_int_nat_fib_closure]
    84     transfer_int_nat_fib transfer_int_nat_fib_closure]
    85 
    85 
    86 
    86 
    87 subsection {* Fibonacci numbers *}
    87 subsection {* Fibonacci numbers *}
    88 
    88