--- a/src/HOL/NumberTheory/IntFact.thy Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy Fri Oct 05 21:52:39 2001 +0200
@@ -10,7 +10,7 @@
text {*
Factorial on integers and recursively defined set including all
- Integers from @{term 2} up to @{term a}. Plus definition of product
+ Integers from @{text 2} up to @{text a}. Plus definition of product
of finite set.
\bigskip
@@ -22,18 +22,18 @@
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))"
+ "zfact n = (if n \<le> Numeral0 then Numeral1 else n * zfact (n - Numeral1))"
defs
- setprod_def: "setprod A == (if finite A then fold (op *) #1 A else #1)"
+ setprod_def: "setprod A == (if finite A then fold (op *) Numeral1 A else Numeral1)"
recdef d22set "measure ((\<lambda>a. nat a) :: int => nat)"
- "d22set a = (if #1 < a then insert a (d22set (a - #1)) else {})"
+ "d22set a = (if Numeral1 < a then insert a (d22set (a - Numeral1)) else {})"
text {* \medskip @{term setprod} --- product of finite set *}
-lemma setprod_empty [simp]: "setprod {} = #1"
+lemma setprod_empty [simp]: "setprod {} = Numeral1"
apply (simp add: setprod_def)
done
@@ -46,7 +46,7 @@
text {*
\medskip @{term d22set} --- recursively defined set including all
- integers from @{term 2} up to @{term a}
+ integers from @{text 2} up to @{text a}
*}
declare d22set.simps [simp del]
@@ -54,7 +54,7 @@
lemma d22set_induct:
"(!!a. P {} a) ==>
- (!!a. #1 < (a::int) ==> P (d22set (a - #1)) (a - #1)
+ (!!a. Numeral1 < (a::int) ==> P (d22set (a - Numeral1)) (a - Numeral1)
==> P (d22set a) a)
==> P (d22set u) u"
proof -
@@ -62,14 +62,14 @@
show ?thesis
apply (rule d22set.induct)
apply safe
- apply (case_tac [2] "#1 < a")
+ apply (case_tac [2] "Numeral1 < 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 \<in> d22set a --> #1 < b"
+lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> Numeral1 < b"
apply (induct a rule: d22set_induct)
prefer 2
apply (subst d22set.simps)
@@ -87,7 +87,7 @@
apply (auto dest: d22set_le)
done
-lemma d22set_mem [rule_format]: "#1 < b --> b \<le> a --> b \<in> d22set a"
+lemma d22set_mem [rule_format]: "Numeral1 < b --> b \<le> a --> b \<in> d22set a"
apply (induct a rule: d22set.induct)
apply auto
apply (simp_all add: d22set.simps)
@@ -109,7 +109,7 @@
apply (simp add: d22set.simps zfact.simps)
apply (subst d22set.simps)
apply (subst zfact.simps)
- apply (case_tac "#1 < a")
+ apply (case_tac "Numeral1 < a")
prefer 2
apply (simp add: d22set.simps zfact.simps)
apply (simp add: d22set_fin d22set_le_swap)