src/HOL/Fact.thy
changeset 35644 d20cf282342e
parent 35028 108662d50512
child 40033 84200d970bf0
equal deleted inserted replaced
35643:965c24dd6856 35644:d20cf282342e
    56 
    56 
    57 lemma transfer_nat_int_factorial_closure:
    57 lemma transfer_nat_int_factorial_closure:
    58   "x >= (0::int) \<Longrightarrow> fact x >= 0"
    58   "x >= (0::int) \<Longrightarrow> fact x >= 0"
    59   by (auto simp add: fact_int_def)
    59   by (auto simp add: fact_int_def)
    60 
    60 
    61 declare TransferMorphism_nat_int[transfer add return: 
    61 declare transfer_morphism_nat_int[transfer add return: 
    62     transfer_nat_int_factorial transfer_nat_int_factorial_closure]
    62     transfer_nat_int_factorial transfer_nat_int_factorial_closure]
    63 
    63 
    64 lemma transfer_int_nat_factorial:
    64 lemma transfer_int_nat_factorial:
    65   "fact (int x) = int (fact x)"
    65   "fact (int x) = int (fact x)"
    66   unfolding fact_int_def by auto
    66   unfolding fact_int_def by auto
    67 
    67 
    68 lemma transfer_int_nat_factorial_closure:
    68 lemma transfer_int_nat_factorial_closure:
    69   "is_nat x \<Longrightarrow> fact x >= 0"
    69   "is_nat x \<Longrightarrow> fact x >= 0"
    70   by (auto simp add: fact_int_def)
    70   by (auto simp add: fact_int_def)
    71 
    71 
    72 declare TransferMorphism_int_nat[transfer add return: 
    72 declare transfer_morphism_int_nat[transfer add return: 
    73     transfer_int_nat_factorial transfer_int_nat_factorial_closure]
    73     transfer_int_nat_factorial transfer_int_nat_factorial_closure]
    74 
    74 
    75 
    75 
    76 subsection {* Factorial *}
    76 subsection {* Factorial *}
    77 
    77