equal
deleted
inserted
replaced
8 theory Abstract_Rat |
8 theory Abstract_Rat |
9 imports GCD |
9 imports GCD |
10 begin |
10 begin |
11 |
11 |
12 types Num = "int \<times> int" |
12 types Num = "int \<times> int" |
13 syntax "_Num0" :: "Num" ("0\<^sub>N") |
13 |
14 translations "0\<^sub>N" \<rightleftharpoons> "(0, 0)" |
14 abbreviation |
15 syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N") |
15 Num0_syn :: Num ("0\<^sub>N") |
16 translations "i\<^sub>N" \<rightleftharpoons> "(i, 1) \<Colon> Num" |
16 where "0\<^sub>N \<equiv> (0, 0)" |
|
17 |
|
18 abbreviation |
|
19 Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N") |
|
20 where "i\<^sub>N \<equiv> (i, 1)" |
17 |
21 |
18 definition |
22 definition |
19 isnormNum :: "Num \<Rightarrow> bool" |
23 isnormNum :: "Num \<Rightarrow> bool" |
20 where |
24 where |
21 "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1))" |
25 "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> igcd a b = 1))" |
129 hence ?thesis by simp} |
133 hence ?thesis by simp} |
130 ultimately show ?thesis by blast |
134 ultimately show ?thesis by blast |
131 qed |
135 qed |
132 |
136 |
133 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)" |
137 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)" |
134 by (simp add: Ninv_def isnormNum_def split_def) |
138 by (simp add: Ninv_def isnormNum_def split_def) |
135 (cases "fst x = 0",auto simp add: igcd_commute) |
139 (cases "fst x = 0", auto simp add: igcd_commute) |
136 |
140 |
137 lemma isnormNum_int[simp]: |
141 lemma isnormNum_int[simp]: |
138 "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N" |
142 "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N" |
139 by (simp_all add: isnormNum_def igcd_def) |
143 by (simp_all add: isnormNum_def igcd_def) |
140 |
144 |