|
1 (* Author: Florian Haftmann, TUM |
|
2 *) |
|
3 |
|
4 section \<open>Proof of concept for residue rings over int using type numerals\<close> |
|
5 |
|
6 theory Residue_Ring |
|
7 imports Main "HOL-Library.Type_Length" |
|
8 begin |
|
9 |
|
10 class len2 = len0 + |
|
11 assumes len_ge_2 [iff]: "2 \<le> LENGTH('a)" |
|
12 begin |
|
13 |
|
14 subclass len |
|
15 proof |
|
16 show "0 < LENGTH('a)" using len_ge_2 |
|
17 by arith |
|
18 qed |
|
19 |
|
20 lemma len_not_eq_Suc_0 [simp]: |
|
21 "LENGTH('a) \<noteq> Suc 0" |
|
22 using len_ge_2 by arith |
|
23 |
|
24 end |
|
25 |
|
26 instance bit0 and bit1 :: (len) len2 |
|
27 by standard (simp_all add: Suc_le_eq) |
|
28 |
|
29 quotient_type (overloaded) 'a residue_ring = int / "\<lambda>k l. k mod int (LENGTH('a)) = l mod int (LENGTH('a::len2))" |
|
30 by (auto intro!: equivpI reflpI sympI transpI) |
|
31 |
|
32 context semiring_1 |
|
33 begin |
|
34 |
|
35 lift_definition repr :: "'b::len2 residue_ring \<Rightarrow> 'a" |
|
36 is "\<lambda>k. of_nat (nat (k mod int (LENGTH('b))))" |
|
37 by simp |
|
38 |
|
39 end |
|
40 |
|
41 instantiation residue_ring :: (len2) comm_ring_1 |
|
42 begin |
|
43 |
|
44 lift_definition zero_residue_ring :: "'a residue_ring" |
|
45 is 0 . |
|
46 |
|
47 lift_definition one_residue_ring :: "'a residue_ring" |
|
48 is 1 . |
|
49 |
|
50 lift_definition plus_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring \<Rightarrow> 'a residue_ring" |
|
51 is plus |
|
52 by (fact mod_add_cong) |
|
53 |
|
54 lift_definition uminus_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring" |
|
55 is uminus |
|
56 by (fact mod_minus_cong) |
|
57 |
|
58 lift_definition minus_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring \<Rightarrow> 'a residue_ring" |
|
59 is minus |
|
60 by (fact mod_diff_cong) |
|
61 |
|
62 lift_definition times_residue_ring :: "'a residue_ring \<Rightarrow> 'a residue_ring \<Rightarrow> 'a residue_ring" |
|
63 is times |
|
64 by (fact mod_mult_cong) |
|
65 |
|
66 instance |
|
67 by (standard; transfer) (simp_all add: algebra_simps mod_eq_0_iff_dvd) |
|
68 |
|
69 end |
|
70 |
|
71 context |
|
72 includes lifting_syntax |
|
73 begin |
|
74 |
|
75 lemma [transfer_rule]: |
|
76 "((\<longleftrightarrow>) ===> pcr_residue_ring) of_bool of_bool" |
|
77 by (unfold of_bool_def [abs_def]; transfer_prover) |
|
78 |
|
79 lemma [transfer_rule]: |
|
80 "((=) ===> pcr_residue_ring) numeral numeral" |
|
81 by (rule transfer_rule_numeral; transfer_prover) |
|
82 |
|
83 lemma [transfer_rule]: |
|
84 "((=) ===> pcr_residue_ring) int of_nat" |
|
85 by (rule transfer_rule_of_nat; transfer_prover) |
|
86 |
|
87 end |
|
88 |
|
89 end |