Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Examples/LarryInt.thy
changeset 753 544b05e03ec0
parent 717 337dd914e1cb
child 766 df053507edba
equal deleted inserted replaced
752:17d06b5ec197 753:544b05e03ec0 
    20   Zero_int_def: "0::int" as "(0::nat, 0::nat)"
 
    20   Zero_int_def: "0::int" as "(0::nat, 0::nat)"
 
    21 
    21 
    22 quotient_def
 
    22 quotient_def
 
    23   One_int_def: "1::int" as "(1::nat, 0::nat)"
 
    23   One_int_def: "1::int" as "(1::nat, 0::nat)"
 
    24 
    24 
       
    25 definition
 
       
    26   "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
       
    27 
    25 quotient_def
 
    28 quotient_def
 
    26   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
    29   "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
    27 as 
    30 as 
    28   "\<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
    31   "add_raw"
 
       
    32 
       
    33 definition
 
       
    34   "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
 
    29 
    35 
    30 quotient_def
 
    36 quotient_def
 
    31   "uminus :: int \<Rightarrow> int" 
    37   "uminus :: int \<Rightarrow> int" 
    32 as 
    38 as 
    33   "\<lambda>(x, y). (y::nat, x::nat)"
 
    39   "uminus_raw"
 
    34 
    40 
    35 fun
 
    41 fun
 
    36   mult_aux::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
 
    42   mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
 
    37 where
 
    43 where
 
    38   "mult_aux (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
    44   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
    39 
    45 
    40 quotient_def
 
    46 quotient_def
 
    41   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
    47   "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
    42 as 
    48 as 
    43   "mult_aux"
 
    49   "mult_raw"
 
       
    50 
       
    51 definition
 
       
    52   "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
 
    44 
    53 
    45 quotient_def 
    54 quotient_def 
    46   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
    55   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
    47 as 
    56 as 
    48   "\<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
 
    57   "le_raw"
 
    49 
    58 
    50 definition
 
    59 definition
 
    51   less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
 
    60   less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
 
    52 
    61 
    53 definition
 
    62 definition
 
    57 
    66 
    58 end
 
    67 end
 
    59 
    68 
    60 subsection{*Construction of the Integers*}
 
    69 subsection{*Construction of the Integers*}
 
    61 
    70 
    62 abbreviation
 
    71 lemma zminus_zminus_raw:
 
    63   "uminus_aux \<equiv> \<lambda>(x, y). (y::nat, x::nat)"
 
    72   "uminus_raw (uminus_raw z) = z"
 
    64 
    73   by (cases z) (simp add: uminus_raw_def)
 
    65 lemma zminus_zminus_aux:
 
    74 
    66   "uminus_aux (uminus_aux z) = z"
 
    75 lemma [quot_respect]:
 
    67   by (cases z) (simp)
 
    76   shows "(intrel ===> intrel) uminus_raw uminus_raw"
 
    68 
    77   by (simp add: uminus_raw_def)
 
    69 lemma [quot_respect]:
 
       
    70   shows "(intrel ===> intrel) uminus_aux uminus_aux"
 
       
    71   by simp
 
       
    72   
    78   
    73 lemma zminus_zminus: 
    79 lemma zminus_zminus: 
    74   shows "- (- z) = (z::int)"
 
    80   shows "- (- z) = (z::int)"
 
    75 apply(lifting zminus_zminus_aux)
 
    81 apply(lifting zminus_zminus_raw)
 
    76 apply(injection)
 
    82 done
 
    77 apply(rule quot_respect)
 
    83 
    78 apply(rule quot_respect)
 
    84 lemma zminus_0_raw:
 
    79 done
 
    85   shows "uminus_raw (0, 0) = (0, 0::nat)"
 
    80 (* PROBLEM *)
 
    86 by (simp add: uminus_raw_def)
 
    81 
       
    82 lemma zminus_0_aux:
 
       
    83   shows "uminus_aux (0, 0) = (0, 0::nat)"
 
       
    84 by simp
 
       
    85 
    87 
    86 lemma zminus_0: "- 0 = (0::int)"
 
    88 lemma zminus_0: "- 0 = (0::int)"
 
    87 apply(lifting zminus_0_aux)
 
    89 apply(lifting zminus_0_raw)
 
    88 apply(injection)
 
    90 done
 
    89 apply(rule quot_respect)
 
       
    90 done
 
       
    91 (* PROBLEM *)
 
       
    92 
    91 
    93 subsection{*Integer Addition*}
 
    92 subsection{*Integer Addition*}
 
    94 
    93 
    95 definition
 
    94 lemma zminus_zadd_distrib_raw:
 
    96   "add_aux \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
 
    95   shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
 
    97 
       
    98 lemma zminus_zadd_distrib_aux:
 
       
    99   shows "uminus_aux (add_aux z w) = add_aux (uminus_aux z) (uminus_aux w)"
 
       
   100 by (cases z, cases w)
 
    96 by (cases z, cases w)
 
   101    (auto simp add: add_aux_def)
 
    97    (auto simp add: add_raw_def uminus_raw_def)
 
   102 
    98 
   103 lemma [quot_respect]:
 
    99 lemma [quot_respect]:
 
   104   shows "(intrel ===> intrel ===> intrel) 
   100   shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
 
   105             (\<lambda>(x, y) (u, v). (x + u, y + (v::nat)))  (\<lambda>(x, y) (u, v). (x + u, y + (v::nat)))"
 
   101 by (simp add: add_raw_def)
 
   106 by simp
 
       
   107 
   102 
   108 lemma zminus_zadd_distrib: 
   103 lemma zminus_zadd_distrib: 
   109   shows "- (z + w) = (- z) + (- w::int)"
 
   104   shows "- (z + w) = (- z) + (- w::int)"
 
   110 apply(lifting zminus_zadd_distrib_aux[simplified add_aux_def])
 
   105 apply(lifting zminus_zadd_distrib_raw)
 
   111 apply(injection)
 
   106 done
 
   112 apply(rule quot_respect)+
 
   107 
   113 done
 
   108 lemma zadd_commute_raw:
 
   114 (* PROBLEM *)
 
   109   shows "add_raw z w = add_raw w z"
 
   115 
       
   116 lemma zadd_commute_aux:
 
       
   117   shows "add_aux z w = add_aux w z"
 
       
   118 by (cases z, cases w)
 
   110 by (cases z, cases w)
 
   119    (simp add: add_aux_def)
 
   111    (simp add: add_raw_def)
 
   120 
   112 
   121 lemma zadd_commute: 
   113 lemma zadd_commute:
 
   122   shows "(z::int) + w = w + z"
 
   114   shows "(z::int) + w = w + z"
 
   123 apply(lifting zadd_commute_aux[simplified add_aux_def])
 
   115 apply(lifting zadd_commute_raw)
 
   124 apply(injection)
 
   116 done
 
   125 apply(rule quot_respect)+
 
   117 
   126 done
 
   118 lemma zadd_assoc_raw:
 
   127 (* PROBLEM *)
 
   119   shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
 
   128 
   120 by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
 
   129 lemma zadd_assoc_aux:
 
       
   130   shows "add_aux (add_aux z1 z2) z3 = add_aux z1 (add_aux z2 z3)"
 
       
   131 by (cases z1, cases z2, cases z3) (simp add: add_aux_def)
 
       
   132 
   121 
   133 lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
 
   122 lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
 
   134 apply(lifting zadd_assoc_aux[simplified add_aux_def])
 
   123 apply(lifting zadd_assoc_raw)
 
   135 apply(injection)
 
   124 done
 
   136 apply(rule quot_respect)+
 
   125 
   137 done
 
   126 lemma zadd_0_raw:
 
   138 (* PROBLEM *)
 
       
   139 
       
   140 lemma zadd_0_aux:
 
       
   141   fixes z::"nat \<times> nat"
 
   127   fixes z::"nat \<times> nat"
 
   142   shows "add_aux (0, 0) z = z"
 
   128   shows "add_raw (0, 0) z = z"
 
   143 by (simp add: add_aux_def)
 
   129 by (simp add: add_raw_def)
 
   144 
   130 
   145 
   131 
   146 (*also for the instance declaration int :: plus_ac0*)
 
   132 (*also for the instance declaration int :: plus_ac0*)
 
   147 lemma zadd_0: "(0::int) + z = z"
 
   133 lemma zadd_0: "(0::int) + z = z"
 
   148 apply(lifting zadd_0_aux[simplified add_aux_def])
 
   134 apply(lifting zadd_0_raw)
 
   149 apply(injection)
 
   135 done
 
   150 apply(rule quot_respect)+
 
   136 
   151 done
 
   137 lemma zadd_zminus_inverse_raw:
 
   152 
   138   shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
 
   153 lemma zadd_zminus_inverse_aux:
 
   139 by (cases z) (simp add: add_raw_def uminus_raw_def)
 
   154   shows "intrel (add_aux (uminus_aux z) z) (0, 0)"
 
       
   155 by (cases z) (simp add: add_aux_def)
 
       
   156 
   140 
   157 lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
 
   141 lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
 
   158 apply(lifting zadd_zminus_inverse_aux[simplified add_aux_def])
 
   142 apply(lifting zadd_zminus_inverse_raw)
 
   159 apply(injection)
 
       
   160 apply(rule quot_respect)+
 
       
   161 done
 
   143 done
 
   162 
   144 
   163 subsection{*Integer Multiplication*}
 
   145 subsection{*Integer Multiplication*}
 
   164 
   146 
   165 lemma zmult_zminus_aux:
 
   147 lemma zmult_zminus_raw:
 
   166   shows "mult_aux (uminus_aux z) w = uminus_aux (mult_aux z w)"
 
   148   shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
 
   167 apply(cases z, cases w)
 
   149 apply(cases z, cases w)
 
   168 apply(simp)
 
   150 apply(simp add:uminus_raw_def)
 
   169 done
 
   151 done
 
   170 
   152 
   171 lemma mult_aux_fst:
 
   153 lemma mult_raw_fst:
 
   172   assumes a: "intrel x z"
 
   154   assumes a: "intrel x z"
 
   173   shows "intrel (mult_aux x y) (mult_aux z y)"
 
   155   shows "intrel (mult_raw x y) (mult_raw z y)"
 
   174 using a
 
   156 using a
 
   175 apply(cases x, cases y, cases z)
 
   157 apply(cases x, cases y, cases z)
 
   176 apply(auto simp add: mult_aux.simps intrel.simps)
 
   158 apply(auto simp add: mult_raw.simps intrel.simps)
 
   177 apply(rename_tac u v w x y z)
 
   159 apply(rename_tac u v w x y z)
 
   178 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
   160 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
   179 apply(simp add: mult_ac)
 
   161 apply(simp add: mult_ac)
 
   180 apply(simp add: add_mult_distrib [symmetric])
 
   162 apply(simp add: add_mult_distrib [symmetric])
 
   181 done
 
   163 done
 
   182 
   164 
   183 lemma mult_aux_snd:
 
   165 lemma mult_raw_snd:
 
   184   assumes a: "intrel x z"
 
   166   assumes a: "intrel x z"
 
   185   shows "intrel (mult_aux y x) (mult_aux y z)"
 
   167   shows "intrel (mult_raw y x) (mult_raw y z)"
 
   186 using a
 
   168 using a
 
   187 apply(cases x, cases y, cases z)
 
   169 apply(cases x, cases y, cases z)
 
   188 apply(auto simp add: mult_aux.simps intrel.simps)
 
   170 apply(auto simp add: mult_raw.simps intrel.simps)
 
   189 apply(rename_tac u v w x y z)
 
   171 apply(rename_tac u v w x y z)
 
   190 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
   172 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
   191 apply(simp add: mult_ac)
 
   173 apply(simp add: mult_ac)
 
   192 apply(simp add: add_mult_distrib [symmetric])
 
   174 apply(simp add: add_mult_distrib [symmetric])
 
   193 done
 
   175 done
 
   194 
   176 
   195 lemma [quot_respect]:
 
   177 lemma [quot_respect]:
 
   196   shows "(intrel ===> intrel ===> intrel) mult_aux mult_aux"
 
   178   shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
 
   197 apply(simp only: fun_rel.simps)
 
   179 apply(simp only: fun_rel.simps)
 
   198 apply(rule allI | rule impI)+
 
   180 apply(rule allI | rule impI)+
 
   199 apply(rule equivp_transp[OF int_equivp])
 
   181 apply(rule equivp_transp[OF int_equivp])
 
   200 apply(rule mult_aux_fst)
 
   182 apply(rule mult_raw_fst)
 
   201 apply(assumption)
 
   183 apply(assumption)
 
   202 apply(rule mult_aux_snd)
 
   184 apply(rule mult_raw_snd)
 
   203 apply(assumption)
 
   185 apply(assumption)
 
   204 done
 
   186 done
 
   205 
   187 
   206 lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
 
   188 lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
 
   207 apply(lifting zmult_zminus_aux)
 
   189 apply(lifting zmult_zminus_raw)
 
   208 apply(injection)
 
   190 done
 
   209 apply(rule quot_respect)
 
   191 
   210 apply(rule quot_respect)
 
   192 lemma zmult_commute_raw: 
   211 done
 
   193   shows "mult_raw z w = mult_raw w z"
 
   212 
       
   213 lemma zmult_commute_aux: 
       
   214   shows "mult_aux z w = mult_aux w z"
 
       
   215 apply(cases z, cases w)
 
   194 apply(cases z, cases w)
 
   216 apply(simp add: add_ac mult_ac)
 
   195 apply(simp add: add_ac mult_ac)
 
   217 done
 
   196 done
 
   218 
   197 
   219 lemma zmult_commute: "(z::int) * w = w * z"
 
   198 lemma zmult_commute: "(z::int) * w = w * z"
 
   220 by (lifting zmult_commute_aux)
 
   199 by (lifting zmult_commute_raw)
 
   221 
   200 
   222 lemma zmult_assoc_aux:
 
   201 lemma zmult_assoc_raw:
 
   223   shows "mult_aux (mult_aux z1 z2) z3 = mult_aux z1 (mult_aux z2 z3)"
 
   202   shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
 
   224 apply(cases z1, cases z2, cases z3)
 
   203 apply(cases z1, cases z2, cases z3)
 
   225 apply(simp add: add_mult_distrib2 mult_ac)
 
   204 apply(simp add: add_mult_distrib2 mult_ac)
 
   226 done
 
   205 done
 
   227 
   206 
   228 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
 
   207 lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
 
   229 by (lifting zmult_assoc_aux)
 
   208 by (lifting zmult_assoc_raw)
 
   230 
   209 
   231 lemma zadd_mult_distrib_aux:
 
   210 lemma zadd_mult_distrib_raw:
 
   232   shows "mult_aux (add_aux z1 z2) w = add_aux (mult_aux z1 w) (mult_aux z2 w)"
 
   211   shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
 
   233 apply(cases z1, cases z2, cases w)
 
   212 apply(cases z1, cases z2, cases w)
 
   234 apply(simp add: add_mult_distrib2 mult_ac add_aux_def)
 
   213 apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
 
   235 done
 
   214 done
 
   236 
   215 
   237 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
 
   216 lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
 
   238 apply(lifting zadd_mult_distrib_aux[simplified add_aux_def])
 
   217 apply(lifting zadd_mult_distrib_raw)
 
   239 apply(injection)
 
       
   240 apply(rule quot_respect)+
 
       
   241 done
 
   218 done
 
   242 
   219 
   243 lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
 
   220 lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
 
   244 by (simp add: zmult_commute [of w] zadd_zmult_distrib)
 
   221 by (simp add: zmult_commute [of w] zadd_zmult_distrib)
 
   245 
   222 
   251 
   228 
   252 lemmas int_distrib =
 
   229 lemmas int_distrib =
 
   253   zadd_zmult_distrib zadd_zmult_distrib2
 
   230   zadd_zmult_distrib zadd_zmult_distrib2
 
   254   zdiff_zmult_distrib zdiff_zmult_distrib2
 
   231   zdiff_zmult_distrib zdiff_zmult_distrib2
 
   255 
   232 
   256 lemma zmult_1_aux:
 
   233 lemma zmult_1_raw:
 
   257   shows "mult_aux (1, 0) z = z"
 
   234   shows "mult_raw (1, 0) z = z"
 
   258 apply(cases z)
 
   235 apply(cases z)
 
   259 apply(auto)
 
   236 apply(auto)
 
   260 done
 
   237 done
 
   261 
   238 
   262 lemma zmult_1: "(1::int) * z = z"
 
   239 lemma zmult_1: "(1::int) * z = z"
 
   263 apply(lifting zmult_1_aux)
 
   240 apply(lifting zmult_1_raw)
 
   264 done
 
   241 done
 
   265 
   242 
   266 lemma zmult_1_right: "z * (1::int) = z"
 
   243 lemma zmult_1_right: "z * (1::int) = z"
 
   267 by (rule trans [OF zmult_commute zmult_1])
 
   244 by (rule trans [OF zmult_commute zmult_1])
 
   268 
   245 
   269 lemma zero_not_one:
 
   246 lemma zero_not_one:
 
   270   shows "(0, 0) \<noteq> (1::nat, 0::nat)"
 
   247   shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
 
   271 by simp
 
   248 by auto
 
   272 
   249 
   273 text{*The Integers Form A Ring*}
 
   250 text{*The Integers Form A Ring*}
 
   274 instance int :: comm_ring_1
 
   251 instance int :: comm_ring_1
 
   275 proof
 
   252 proof
 
   276   fix i j k :: int
 
   253   fix i j k :: int
 
   281   show "i - j = i + (-j)" by (simp add: diff_int_def)
 
   258   show "i - j = i + (-j)" by (simp add: diff_int_def)
 
   282   show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
 
   259   show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
 
   283   show "i * j = j * i" by (rule zmult_commute)
 
   260   show "i * j = j * i" by (rule zmult_commute)
 
   284   show "1 * i = i" by (rule zmult_1) 
   261   show "1 * i = i" by (rule zmult_1) 
   285   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
 
   262   show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
 
   286   show "0 \<noteq> (1::int)" 
   263   show "0 \<noteq> (1::int)" by (lifting zero_not_one)
 
   287     by (lifting zero_not_one) (auto) (* PROBLEM? regularize failed *)
 
       
   288 qed
 
   264 qed
 
   289 
   265 
   290 
   266 
   291 subsection{*The @{text "\<le>"} Ordering*}
 
   267 subsection{*The @{text "\<le>"} Ordering*}
 
   292 
   268 
   293 abbreviation
 
   269 lemma zle_refl_raw:
 
   294   "le_aux \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
 
   270   "le_raw w w"
 
   295 
       
   296 lemma zle_refl_aux:
 
       
   297   "le_aux w w"
 
       
   298 apply(cases w)
 
   271 apply(cases w)
 
   299 apply(simp)
 
   272 apply(simp add: le_raw_def)
 
   300 done
 
   273 done
 
   301 
   274 
   302 lemma [quot_respect]:
 
   275 lemma [quot_respect]:
 
   303   shows "(intrel ===> intrel ===> op =) le_aux le_aux"
 
   276   shows "(intrel ===> intrel ===> op =) le_raw le_raw"
 
   304 by auto
 
   277 by (auto) (simp_all add: le_raw_def)
 
   305 
   278 
   306 lemma zle_refl: "w \<le> (w::int)"
 
   279 lemma zle_refl: "w \<le> (w::int)"
 
   307 apply(lifting zle_refl_aux)
 
   280 apply(lifting zle_refl_raw)
 
   308 apply(injection)
 
   281 done
 
   309 apply(rule quot_respect)
 
   282 
   310 done
 
   283 lemma zle_trans_raw:
 
   311 (* PROBLEM *)
 
   284   shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
 
   312 
       
   313 lemma zle_trans_aux:
 
       
   314   shows "\<lbrakk>le_aux i j; le_aux j k\<rbrakk> \<Longrightarrow> le_aux i k"
 
       
   315 apply(cases i, cases j, cases k)
 
   285 apply(cases i, cases j, cases k)
 
   316 apply(auto)
 
   286 apply(auto)
 
       
   287 apply(simp add:le_raw_def)
 
   317 done
 
   288 done
 
   318 
   289 
   319 lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"
 
   290 lemma zle_trans: "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> (k::int)"
 
   320 apply(lifting zle_trans_aux)
 
   291 apply(lifting zle_trans_raw)
 
   321 apply(injection)
 
   292 done
 
   322 apply(rule quot_respect)+
 
   293 
   323 done
 
   294 lemma zle_anti_sym_raw:
 
   324 (* PROBLEM *)
 
   295   shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
 
   325 
       
   326 lemma zle_anti_sym_aux:
 
       
   327   shows "\<lbrakk>le_aux z w; le_aux w z\<rbrakk> \<Longrightarrow> intrel z w"
 
       
   328 apply(cases z, cases w)
 
   296 apply(cases z, cases w)
 
   329 apply(auto)
 
   297 apply(auto iff: le_raw_def)
 
   330 done
 
   298 done
 
   331 
   299 
   332 lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"
 
   300 lemma zle_anti_sym: "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = (w::int)"
 
   333 apply(lifting zle_anti_sym_aux)
 
   301 apply(lifting zle_anti_sym_raw)
 
   334 apply(injection)
 
   302 done
 
   335 apply(rule quot_respect)+
 
       
   336 done
 
       
   337 (* PROBLEM *)
 
       
   338 
   303 
   339 (* Axiom 'order_less_le' of class 'order': *)
 
   304 (* Axiom 'order_less_le' of class 'order': *)
 
   340 lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
 
   305 lemma zless_le: "((w::int) < z) = (w \<le> z & w \<noteq> z)"
 
   341 by (simp add: less_int_def)
 
   306 by (simp add: less_int_def)
 
   342 
   307 
   345 apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def)
 
   310 apply(auto intro: zle_refl zle_trans zle_anti_sym zless_le simp add: less_int_def)
 
   346 done
 
   311 done
 
   347 
   312 
   348 (* Axiom 'linorder_linear' of class 'linorder': *)
 
   313 (* Axiom 'linorder_linear' of class 'linorder': *)
 
   349 
   314 
   350 lemma zle_linear_aux:
 
   315 lemma zle_linear_raw:
 
   351   "le_aux z w \<or> le_aux w z"
 
   316   "le_raw z w \<or> le_raw w z"
 
   352 apply(cases w, cases z)
 
   317 apply(cases w, cases z)
 
   353 apply(auto)
 
   318 apply(auto iff: le_raw_def)
 
   354 done
 
   319 done
 
   355 
   320 
   356 
   321 
   357 lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
 
   322 lemma zle_linear: "(z::int) \<le> w \<or> w \<le> z"
 
   358 apply(lifting zle_linear_aux)
 
   323 apply(lifting zle_linear_raw)
 
   359 apply(injection)
 
       
   360 apply(rule quot_respect)+
 
       
   361 done
 
   324 done
 
   362 
   325 
   363 instance int :: linorder
 
   326 instance int :: linorder
 
   364 proof qed (rule zle_linear)
 
   327 proof qed (rule zle_linear)
 
   365 
   328 
   366 lemma zadd_left_mono_aux:
 
   329 lemma zadd_left_mono_raw:
 
   367   shows "le_aux i j \<Longrightarrow> le_aux (add_aux k i) (add_aux k j)"
 
   330   shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
 
   368 apply(cases k)
 
   331 apply(cases k)
 
   369 apply(auto simp add: add_aux_def)
 
   332 apply(auto simp add: add_raw_def le_raw_def)
 
   370 done
 
   333 done
 
   371 
   334 
   372 lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"
 
   335 lemma zadd_left_mono: "i \<le> j \<Longrightarrow> k + i \<le> k + (j::int)"
 
   373 apply(lifting zadd_left_mono_aux[simplified add_aux_def])
 
   336 apply(lifting zadd_left_mono_raw)
 
   374 apply(injection)
 
   337 done
 
   375 apply(rule quot_respect)+
 
       
   376 done
 
       
   377 (* PROBLEM *)
 
       
   378 
   338 
   379 
   339 
   380 
   340 
   381 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
 
   341 subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
 
   382 
   342 
   383 (* PROBLEM: this has to be a definition, not an abbreviation *)
 
   343 definition
 
   384 (* otherwise the lemma nat_le_eq_zle cannot be lifted        *)
 
   344   "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
 
   385 
       
   386 abbreviation
 
       
   387   "nat_aux \<equiv> \<lambda>(x, y).x - (y::nat)"
 
       
   388 
   345 
   389 quotient_def
 
   346 quotient_def
 
   390   "nat2::int\<Rightarrow>nat"
 
   347   "nat2::int\<Rightarrow>nat"
 
   391 as
 
   348 as
 
   392   "nat_aux"
 
   349   "nat_raw"
 
   393 
   350 
   394 abbreviation
 
   351 abbreviation
 
   395   "less_aux x y \<equiv> (le_aux x y \<and> \<not>(x = y))"
 
   352   "less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))"
 
   396 
   353 
   397 lemma nat_le_eq_zle_aux:
 
   354 lemma nat_le_eq_zle_raw:
 
   398   shows "less_aux (0, 0) w \<or> le_aux (0, 0) z \<Longrightarrow> (nat_aux w \<le> nat_aux z) = (le_aux w z)"
 
   355   shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
 
   399 apply(auto)
 
   356 apply(auto)
 
   400 sorry
 
   357 sorry
 
   401 
   358 
   402 lemma [quot_respect]:
 
   359 lemma [quot_respect]:
 
   403   shows "(intrel ===> op =) nat_aux nat_aux"
 
   360   shows "(intrel ===> op =) nat_raw nat_raw"
 
   404 apply(auto)
 
   361 apply(auto iff: nat_raw_def)
 
   405 done
 
   362 done
 
   406 
   363 
   407 ML {*
 
   364 ML {*
 
   408   let
 
   365   let
 
   409    val parser = Args.context -- Scan.lift Args.name_source
 
   366    val parser = Args.context -- Scan.lift Args.name_source
 
   420 consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b"
 
   377 consts test::"'b \<Rightarrow> 'b \<Rightarrow> 'b"
 
   421 
   378 
   422 
   379 
   423 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
 
   380 lemma nat_le_eq_zle: "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
 
   424 unfolding less_int_def
 
   381 unfolding less_int_def
 
   425 apply(lifting nat_le_eq_zle_aux)
 
   382 apply(lifting nat_le_eq_zle_raw)
 
   426 apply(injection)
 
       
   427 apply(simp_all only: quot_respect)
 
       
   428 done
 
   383 done
 
   429 
   384 
   430 end
 
   385 end
nominal2