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.
Attic/Quot/Examples/IntEx2.thy
changeset 1939 19f296e757c5
parent 1260 9df6144e281b
child 1974 13298f4b212b
equal deleted inserted replaced
1938:3641d055b260 1939:19f296e757c5 
    74 
    74 
    75 end
 
    75 end
 
    76 
    76 
    77 lemma plus_raw_rsp[quot_respect]:
 
    77 lemma plus_raw_rsp[quot_respect]:
 
    78   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 
    78   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 
    79 by auto
 
    79   by auto
 
    80 
    80 
    81 lemma uminus_raw_rsp[quot_respect]:
 
    81 lemma uminus_raw_rsp[quot_respect]:
 
    82   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
 
    82   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
 
    83   by auto
 
    83   by auto
 
    84 
    84 
    85 lemma mult_raw_fst:
 
    85 lemma mult_raw_fst:
 
    86   assumes a: "x \<approx> z"
 
    86   assumes a: "x \<approx> z"
 
    87   shows "mult_raw x y \<approx> mult_raw z y"
 
    87   shows "mult_raw x y \<approx> mult_raw z y"
 
    88 using a
 
    88   using a
 
    89 apply(cases x, cases y, cases z)
 
    89   apply(cases x, cases y, cases z)
 
    90 apply(auto simp add: mult_raw.simps intrel.simps)
 
    90   apply(auto simp add: mult_raw.simps intrel.simps)
 
    91 apply(rename_tac u v w x y z)
 
    91   apply(rename_tac u v w x y z)
 
    92 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
    92   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
    93 apply(simp add: mult_ac)
 
    93   apply(simp add: mult_ac)
 
    94 apply(simp add: add_mult_distrib [symmetric])
 
    94   apply(simp add: add_mult_distrib [symmetric])
 
    95 done
 
    95   done
 
    96 
    96 
    97 lemma mult_raw_snd:
 
    97 lemma mult_raw_snd:
 
    98   assumes a: "x \<approx> z"
 
    98   assumes a: "x \<approx> z"
 
    99   shows "mult_raw y x \<approx> mult_raw y z"
 
    99   shows "mult_raw y x \<approx> mult_raw y z"
 
   100 using a
 
   100   using a
 
   101 apply(cases x, cases y, cases z)
 
   101   apply(cases x, cases y, cases z)
 
   102 apply(auto simp add: mult_raw.simps intrel.simps)
 
   102   apply(auto simp add: mult_raw.simps intrel.simps)
 
   103 apply(rename_tac u v w x y z)
 
   103   apply(rename_tac u v w x y z)
 
   104 apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
   104   apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
 
   105 apply(simp add: mult_ac)
 
   105   apply(simp add: mult_ac)
 
   106 apply(simp add: add_mult_distrib [symmetric])
 
   106   apply(simp add: add_mult_distrib [symmetric])
 
   107 done
 
   107   done
 
   108 
   108 
   109 lemma mult_raw_rsp[quot_respect]:
 
   109 lemma mult_raw_rsp[quot_respect]:
 
   110   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   110   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   111 apply(simp only: fun_rel_def)
 
   111   apply(simp only: fun_rel_def)
 
   112 apply(rule allI | rule impI)+
 
   112   apply(rule allI | rule impI)+
 
   113 apply(rule equivp_transp[OF int_equivp])
 
   113   apply(rule equivp_transp[OF int_equivp])
 
   114 apply(rule mult_raw_fst)
 
   114   apply(rule mult_raw_fst)
 
   115 apply(assumption)
 
   115   apply(assumption)
 
   116 apply(rule mult_raw_snd)
 
   116   apply(rule mult_raw_snd)
 
   117 apply(assumption)
 
   117   apply(assumption)
 
   118 done
 
   118   done
 
   119 
   119 
   120 lemma le_raw_rsp[quot_respect]:
 
   120 lemma le_raw_rsp[quot_respect]:
 
   121   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
 
   121   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
 
   122 by auto
 
   122   by auto
 
   123 
   123 
   124 lemma plus_assoc_raw:
 
   124 lemma plus_assoc_raw:
 
   125   shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
 
   125   shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
 
   126 by (cases i, cases j, cases k) (simp)
 
   126   by (cases i, cases j, cases k) (simp)
 
   127 
   127 
   128 lemma plus_sym_raw:
 
   128 lemma plus_sym_raw:
 
   129   shows "plus_raw i j \<approx> plus_raw j i"
 
   129   shows "plus_raw i j \<approx> plus_raw j i"
 
   130 by (cases i, cases j) (simp)
 
   130   by (cases i, cases j) (simp)
 
   131 
   131 
   132 lemma plus_zero_raw:
 
   132 lemma plus_zero_raw:
 
   133   shows "plus_raw  (0, 0) i \<approx> i"
 
   133   shows "plus_raw  (0, 0) i \<approx> i"
 
   134 by (cases i) (simp)
 
   134   by (cases i) (simp)
 
   135 
   135 
   136 lemma plus_minus_zero_raw:
 
   136 lemma plus_minus_zero_raw:
 
   137   shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
 
   137   shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
 
   138 by (cases i) (simp)
 
   138   by (cases i) (simp)
 
   139 
   139 
   140 lemma times_assoc_raw:
 
   140 lemma times_assoc_raw:
 
   141   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
 
   141   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
 
   142 by (cases i, cases j, cases k) 
   142   by (cases i, cases j, cases k) 
   143    (simp add: algebra_simps)
 
   143      (simp add: algebra_simps)
 
   144 
   144 
   145 lemma times_sym_raw:
 
   145 lemma times_sym_raw:
 
   146   shows "mult_raw i j \<approx> mult_raw j i"
 
   146   shows "mult_raw i j \<approx> mult_raw j i"
 
   147 by (cases i, cases j) (simp add: algebra_simps)
 
   147   by (cases i, cases j) (simp add: algebra_simps)
 
   148 
   148 
   149 lemma times_one_raw:
 
   149 lemma times_one_raw:
 
   150   shows "mult_raw  (1, 0) i \<approx> i"
 
   150   shows "mult_raw  (1, 0) i \<approx> i"
 
   151 by (cases i) (simp)
 
   151   by (cases i) (simp)
 
   152 
   152 
   153 lemma times_plus_comm_raw:
 
   153 lemma times_plus_comm_raw:
 
   154   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 
   154   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 
   155 by (cases i, cases j, cases k) 
   155 by (cases i, cases j, cases k) 
   156    (simp add: algebra_simps)
 
   156    (simp add: algebra_simps)
 
   187 qed
 
   187 qed
 
   188 
   188 
   189 lemma plus_raw_rsp_aux:
 
   189 lemma plus_raw_rsp_aux:
 
   190   assumes a: "a \<approx> b" "c \<approx> d"
 
   190   assumes a: "a \<approx> b" "c \<approx> d"
 
   191   shows "plus_raw a c \<approx> plus_raw b d"
 
   191   shows "plus_raw a c \<approx> plus_raw b d"
 
   192 using a
 
   192   using a
 
   193 by (cases a, cases b, cases c, cases d) 
   193   by (cases a, cases b, cases c, cases d)
 
   194    (simp)
 
   194      (simp)
 
   195 
   195 
   196 lemma add:
 
   196 lemma add:
 
   197      "(abs_int (x,y)) + (abs_int (u,v)) =
 
   197   "(abs_int (x,y)) + (abs_int (u,v)) =
 
   198       (abs_int (x + u, y + v))"
 
   198    (abs_int (x + u, y + v))"
 
   199 apply(simp add: plus_int_def id_simps)
 
   199   apply(simp add: plus_int_def id_simps)
 
   200 apply(fold plus_raw.simps)
 
   200   apply(fold plus_raw.simps)
 
   201 apply(rule Quotient_rel_abs[OF Quotient_int])
 
   201   apply(rule Quotient_rel_abs[OF Quotient_int])
 
   202 apply(rule plus_raw_rsp_aux)
 
   202   apply(rule plus_raw_rsp_aux)
 
   203 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
 
   203   apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
 
   204 done
 
   204   done
 
   205 
   205 
   206 definition int_of_nat_raw: 
   206 definition int_of_nat_raw: 
   207   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
   207   "int_of_nat_raw m = (m :: nat, 0 :: nat)"
 
   208 
   208 
   209 quotient_definition
 
   209 quotient_definition
 
   210   "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
 
   210   "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
 
   211 
   211 
   212 lemma[quot_respect]: 
   212 lemma[quot_respect]: 
   213   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
 
   213   shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
 
   214 by (simp add: equivp_reflp[OF int_equivp])
 
   214   by (simp add: equivp_reflp[OF int_equivp])
 
   215 
   215 
   216 lemma int_of_nat:
 
   216 lemma int_of_nat:
 
   217   shows "of_nat m = int_of_nat m"
 
   217   shows "of_nat m = int_of_nat m"
 
   218 apply (induct m)
 
   218   by (induct m)
 
   219 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
 
   219     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
 
   220 done
 
       
   221 
   220 
   222 lemma le_antisym_raw:
 
   221 lemma le_antisym_raw:
 
   223   shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
 
   222   shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
 
   224 by (cases i, cases j) (simp)
 
   223   by (cases i, cases j) (simp)
 
   225 
   224 
   226 lemma le_refl_raw:
 
   225 lemma le_refl_raw:
 
   227   shows "le_raw i i"
 
   226   shows "le_raw i i"
 
   228 by (cases i) (simp)
 
   227   by (cases i) (simp)
 
   229 
   228 
   230 lemma le_trans_raw:
 
   229 lemma le_trans_raw:
 
   231   shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
 
   230   shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
 
   232 by (cases i, cases j, cases k) (simp)
 
   231   by (cases i, cases j, cases k) (simp)
 
   233 
   232 
   234 lemma le_cases_raw:
 
   233 lemma le_cases_raw:
 
   235   shows "le_raw i j \<or> le_raw j i"
 
   234   shows "le_raw i j \<or> le_raw j i"
 
   236 by (cases i, cases j) 
   235   by (cases i, cases j)
 
   237    (simp add: linorder_linear)
 
   236      (simp add: linorder_linear)
 
   238 
   237 
   239 instance int :: linorder
 
   238 instance int :: linorder
 
   240 proof
 
   239 proof
 
   241   fix i j k :: int
 
   240   fix i j k :: int
 
   242   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
 
   241   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
 
   266 
   265 
   267 end
 
   266 end
 
   268 
   267 
   269 lemma le_plus_raw:
 
   268 lemma le_plus_raw:
 
   270   shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
 
   269   shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
 
   271 by (cases i, cases j, cases k) (simp)
 
   270   by (cases i, cases j, cases k) (simp)
 
   272 
       
   273 
   271 
   274 instance int :: ordered_cancel_ab_semigroup_add
 
   272 instance int :: ordered_cancel_ab_semigroup_add
 
   275 proof
 
   273 proof
 
   276   fix i j k :: int
 
   274   fix i j k :: int
 
   277   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
 
   275   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
 
   283 
   281 
   284 lemma zmult_zless_mono2_lemma:
 
   282 lemma zmult_zless_mono2_lemma:
 
   285   fixes i j::int
 
   283   fixes i j::int
 
   286   and   k::nat
 
   284   and   k::nat
 
   287   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
 
   285   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
 
   288 apply(induct "k")
 
   286   apply(induct "k")
 
   289 apply(simp)
 
   287   apply(simp)
 
   290 apply(case_tac "k = 0")
 
   288   apply(case_tac "k = 0")
 
   291 apply(simp_all add: left_distrib add_strict_mono)
 
   289   apply(simp_all add: left_distrib add_strict_mono)
 
   292 done
 
   290   done
 
   293 
   291 
   294 lemma zero_le_imp_eq_int_raw:
 
   292 lemma zero_le_imp_eq_int_raw:
 
   295   fixes k::"(nat \<times> nat)"
 
   293   fixes k::"(nat \<times> nat)"
 
   296   shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
 
   294   shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
 
   297 apply(cases k)
 
   295   apply(cases k)
 
   298 apply(simp add:int_of_nat_raw)
 
   296   apply(simp add:int_of_nat_raw)
 
   299 apply(auto)
 
   297   apply(auto)
 
   300 apply(rule_tac i="b" and j="a" in less_Suc_induct)
 
   298   apply(rule_tac i="b" and j="a" in less_Suc_induct)
 
   301 apply(auto)
 
   299   apply(auto)
 
   302 done
 
   300   done
 
   303 
   301 
   304 lemma zero_le_imp_eq_int:
 
   302 lemma zero_le_imp_eq_int:
 
   305   fixes k::int
 
   303   fixes k::int
 
   306   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
 
   304   shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
 
   307   unfolding less_int_def int_of_nat
 
   305   unfolding less_int_def int_of_nat
 
   309 
   307 
   310 lemma zmult_zless_mono2: 
   308 lemma zmult_zless_mono2: 
   311   fixes i j k::int
 
   309   fixes i j k::int
 
   312   assumes a: "i < j" "0 < k"
 
   310   assumes a: "i < j" "0 < k"
 
   313   shows "k * i < k * j"
 
   311   shows "k * i < k * j"
 
   314 using a
 
   312   using a
 
   315 using a
 
   313   by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
 
   316 apply(drule_tac zero_le_imp_eq_int)
 
       
   317 apply(auto simp add: zmult_zless_mono2_lemma)
 
       
   318 done
 
       
   319 
   314 
   320 text{*The integers form an ordered integral domain*}
 
   315 text{*The integers form an ordered integral domain*}
 
   321 instance int :: linordered_idom
 
   316 instance int :: linordered_idom
 
   322 proof
 
   317 proof
 
   323   fix i j k :: int
 
   318   fix i j k :: int
 
   333   left_distrib [of "z1::int" "z2" "w", standard]
 
   328   left_distrib [of "z1::int" "z2" "w", standard]
 
   334   right_distrib [of "w::int" "z1" "z2", standard]
 
   329   right_distrib [of "w::int" "z1" "z2", standard]
 
   335   left_diff_distrib [of "z1::int" "z2" "w", standard]
 
   330   left_diff_distrib [of "z1::int" "z2" "w", standard]
 
   336   right_diff_distrib [of "w::int" "z1" "z2", standard]
 
   331   right_diff_distrib [of "w::int" "z1" "z2", standard]
 
   337 
   332 
       
   333 lemma int_induct_raw:
 
       
   334   assumes a: "P (0::nat, 0)"
 
       
   335   and     b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1, 0))"
 
       
   336   and     c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1, 0)))"
 
       
   337   shows      "P x"
 
       
   338 proof (cases x, clarify)
 
       
   339   fix a b
 
       
   340   show "P (a, b)"
 
       
   341   proof (induct a arbitrary: b rule: Nat.induct)
 
       
   342     case zero
 
       
   343     show "P (0, b)" using assms by (induct b) auto
 
       
   344   next
 
       
   345     case (Suc n)
 
       
   346     then show ?case using assms by auto
 
       
   347   qed
 
       
   348 qed
 
       
   349 
       
   350 lemma int_induct:
 
       
   351   fixes x :: int
 
       
   352   assumes a: "P 0"
 
       
   353   and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
 
       
   354   and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
 
       
   355   shows      "P x"
 
       
   356   using a b c unfolding minus_int_def
 
       
   357   by (lifting int_induct_raw)
 
   338 
   358 
   339 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
 
   359 subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
 
   340 
   360 
   341 (*
 
   361 (*
 
   342 context ring_1
 
   362 context ring_1
nominal2