<commit_before>(*  Title:      HOL/NumberTheory/IntFact.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   2000  University of Cambridge
*)

header {* Factorial on integers *}

theory IntFact = IntPrimes:

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"
  setprod :: "int set => int"
  d22set :: "int => int set"

recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
  "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"

defs
  setprod_def: "setprod A == (if finite A then fold (op *) 1 A else 1)"

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


text {* \medskip @{term setprod} --- product of finite set *}

lemma setprod_empty [simp]: "setprod {} = 1"
  apply (simp add: setprod_def)
  done

lemma setprod_insert [simp]:
    "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
  apply (unfold setprod_def)
  apply (simp add: zmult_left_commute LC.fold_insert [OF LC_axioms.intro])
  done


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)<commit_msg>*** empty log message ***<commit_after>(*  Title:      HOL/NumberTheory/IntFact.thy
    ID:         $Id$
    Author:     <NAME>
    Copyright   2000  University of Cambridge
*)

header {* Factorial on integers *}

theory IntFact = IntPrimes:

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"
  setprod :: "int set => int"
  d22set :: "int => int set"

recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
  "zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"

defs
  setprod_def: "setprod A == (if finite A then fold (op *) 1 A else 1)"

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


text {* \medskip @{term setprod} --- product of finite set *}

lemma setprod_empty [simp]: "setprod {} = 1"
  apply (simp add: setprod_def)
  done

lemma setprod_insert [simp]:
    "finite A ==> a \<notin> A ==> setprod (insert a A) = a * setprod A"
  by (simp add: setprod_def zmult_left_commute LC.fold_insert [OF LC.intro, OF LC_axioms.intro])

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)
{'fraction_non_alphanumeric': 0.15500170706725844, 'fraction_numerical': 0.023898941618299762, 'mean_word_length': 2.9594594594594597, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 33, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2209465', 'n_tokens_mistral': 1187, 'n_tokens_neox': 1112, 'n_words': 392}