# Theory IntFact

Up to index of Isabelle/HOL/NumberTheory

theory IntFact
imports IntPrimes
begin

    (*  Title:      HOL/NumberTheory/IntFact.thy
        ID:         $Id: IntFact.thy,v 1.12 2005/06/17 14:13:09 haftmann Exp $
        Author:     Thomas M. Rasmussen
        Copyright   2000  University of Cambridge
    *)

    header {* Factorial on integers *}

    theory IntFact imports IntPrimes begin

    text {*
      Factorial on integers and recursively defined set including all
      Integers from @{text 2} up to @{text a}.  Plus definition of product
      of finite set.

      \bigskip
    *}

    consts
      zfact :: "int => int"
      d22set :: "int => int set"

    recdef zfact  "measure ((λn. nat n) :: int => nat)"
      "zfact n = (if n ≤ 0 then 1 else n * zfact (n - 1))"

    recdef d22set  "measure ((λa. nat a) :: int => nat)"
      "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"

    text {*
      \medskip @{term d22set} --- recursively defined set including all
      integers from @{text 2} up to @{text a}
    *}

    declare d22set.simps [simp del]

    lemma d22set_induct:
      "(!!a. P {} a) ==>
        (!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1)
          ==> P (d22set a) a)
        ==> P (d22set u) u"
    proof -
      case rule_context
      show ?thesis
        apply (rule d22set.induct)
        apply safe
         apply (case_tac [2] "1 < a")
          apply (rule_tac [2] rule_context)
           apply (simp_all (no_asm_simp))
         apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
        done
    qed

    lemma d22set_g_1 [rule_format]: "b ∈ d22set a --> 1 < b"
      apply (induct a rule: d22set_induct)
       prefer 2
       apply (subst d22set.simps)
       apply auto
      done

    lemma d22set_le [rule_format]: "b ∈ d22set a --> b ≤ a"
      apply (induct a rule: d22set_induct)
       prefer 2
       apply (subst d22set.simps)
       apply auto
      done

    lemma d22set_le_swap: "a < b ==> b ∉ d22set a"
      apply (auto dest: d22set_le)
      done

    lemma d22set_mem [rule_format]: "1 < b --> b ≤ a --> b ∈ d22set a"
      apply (induct a rule: d22set.induct)
      apply auto
       apply (simp_all add: d22set.simps)
      done

    lemma d22set_fin: "finite (d22set a)"
      apply (induct a rule: d22set_induct)
       prefer 2
       apply (subst d22set.simps)
       apply auto
      done

    declare zfact.simps [simp del]

    lemma d22set_prod_zfact: "∏(d22set a) = zfact a"
      apply (induct a rule: d22set.induct)
      apply safe
       apply (simp add: d22set.simps zfact.simps)
      apply (subst d22set.simps)
      apply (subst zfact.simps)
      apply (case_tac "1 < a")
       prefer 2
       apply (simp add: d22set.simps zfact.simps)
      apply (simp add: d22set_fin d22set_le_swap)
      done

    end

lemma d22set_induct:

      [| !!a. P {} a;
         !!a. [| 1 < a; P (d22set (a - 1)) (a - 1) |] ==> P (d22set a) a |]
      ==> P (d22set u) u

lemma d22set_g_1:

      b ∈ d22set a ==> 1 < b

lemma d22set_le:

      b ∈ d22set a ==> b ≤ a

lemma d22set_le_swap:

      a < b ==> b ∉ d22set a

lemma d22set_mem:

      [| 1 < b; b ≤ a |] ==> b ∈ d22set a

lemma d22set_fin:

      finite (d22set a)

lemma d22set_prod_zfact:

      ∏(d22set a) = zfact a