author  wenzelm 
Sat, 10 Oct 2015 16:26:23 +0200  
changeset 61382  efac889fccbc 
parent 58889  5b7a9633cfa8 
child 63167  0909deb8059b 
permissions  rwrr 
38159  1 
(* Title: HOL/Old_Number_Theory/IntFact.thy 
2 
Author: Thomas M. Rasmussen 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

3 
Copyright 2000 University of Cambridge 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

4 
*) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

5 

61382  6 
section \<open>Factorial on integers\<close> 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

7 

38159  8 
theory IntFact 
9 
imports IntPrimes 

10 
begin 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

11 

61382  12 
text \<open> 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

13 
Factorial on integers and recursively defined set including all 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11549
diff
changeset

14 
Integers from @{text 2} up to @{text a}. Plus definition of product 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

15 
of finite set. 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

16 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

17 
\bigskip 
61382  18 
\<close> 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

19 

38159  20 
fun zfact :: "int => int" 
21 
where "zfact n = (if n \<le> 0 then 1 else n * zfact (n  1))" 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

22 

38159  23 
fun d22set :: "int => int set" 
24 
where "d22set a = (if 1 < a then insert a (d22set (a  1)) else {})" 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

25 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

26 

61382  27 
text \<open> 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

28 
\medskip @{term d22set}  recursively defined set including all 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11549
diff
changeset

29 
integers from @{text 2} up to @{text a} 
61382  30 
\<close> 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

31 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

32 
declare d22set.simps [simp del] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

33 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

34 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

35 
lemma d22set_induct: 
18369  36 
assumes "!!a. P {} a" 
37 
and "!!a. 1 < (a::int) ==> P (d22set (a  1)) (a  1) ==> P (d22set a) a" 

38 
shows "P (d22set u) u" 

39 
apply (rule d22set.induct) 

35440  40 
apply (case_tac "1 < a") 
41 
apply (rule_tac assms) 

42 
apply (simp_all (no_asm_simp)) 

43 
apply (simp_all (no_asm_simp) add: d22set.simps assms) 

18369  44 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

45 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

46 
lemma d22set_g_1 [rule_format]: "b \<in> d22set a > 1 < b" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

47 
apply (induct a rule: d22set_induct) 
18369  48 
apply simp 
49 
apply (subst d22set.simps) 

50 
apply auto 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

51 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

52 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

53 
lemma d22set_le [rule_format]: "b \<in> d22set a > b \<le> a" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

54 
apply (induct a rule: d22set_induct) 
18369  55 
apply simp 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

56 
apply (subst d22set.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

57 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

58 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

59 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

60 
lemma d22set_le_swap: "a < b ==> b \<notin> d22set a" 
18369  61 
by (auto dest: d22set_le) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

62 

18369  63 
lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

64 
apply (induct a rule: d22set.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

65 
apply auto 
35440  66 
apply (subst d22set.simps) 
67 
apply (case_tac "b < a", auto) 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

68 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

69 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

70 
lemma d22set_fin: "finite (d22set a)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

71 
apply (induct a rule: d22set_induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

72 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

73 
apply (subst d22set.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

74 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

75 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

76 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

77 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

78 
declare zfact.simps [simp del] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

79 

15392  80 
lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

81 
apply (induct a rule: d22set.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

82 
apply (subst d22set.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

83 
apply (subst zfact.simps) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

84 
apply (case_tac "1 < a") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

85 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

86 
apply (simp add: d22set.simps zfact.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

87 
apply (simp add: d22set_fin d22set_le_swap) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

88 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

89 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
9508
diff
changeset

90 
end 