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/IntEx2.thy
changeset 710 add8f7f311cd
parent 705 f51c6069cd17
child 711 810d59a3d9b0
equal deleted inserted replaced
709:596467882518 710:add8f7f311cd 
    44 
    44 
    45 definition
 
    45 definition
 
    46   minus_int_def [code del]:  "z - w = z + (-w::int)"
 
    46   minus_int_def [code del]:  "z - w = z + (-w::int)"
 
    47 
    47 
    48 fun
 
    48 fun
 
    49   times_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    49   mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    50 where
 
    50 where
 
    51   "times_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
    51   "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
 
    52 
    52 
    53 quotient_def
 
    53 quotient_def
 
    54   "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "times_raw"
 
    54   mult_int_def: "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" as "mult_raw"
 
    55 
    55 
    56 (* PROBLEM: this should be called le_int and le_raw / or odd *)
 
       
    57 fun
 
    56 fun
 
    58   less_eq_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 
    57   le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 
    59 where
 
    58 where
 
    60   "less_eq_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
    59   "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
 
    61 
    60 
    62 quotient_def
 
    61 quotient_def
 
    63   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "less_eq_raw"
 
    62   le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" as "le_raw"
 
    64 
    63 
    65 definition
 
    64 definition
 
    66   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
 
    65   less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
 
    67 
    66 
    68 definition
 
    67 definition
 
    81 
    80 
    82 lemma uminus_raw_rsp[quot_respect]:
 
    81 lemma uminus_raw_rsp[quot_respect]:
 
    83   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
 
    82   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
 
    84   by auto
 
    83   by auto
 
    85 
    84 
    86 lemma times_raw_fst:
 
    85 lemma mult_raw_fst:
 
    87   assumes a: "x \<approx> z"
 
    86   assumes a: "x \<approx> z"
 
    88   shows "times_raw x y \<approx> times_raw z y"
 
    87   shows "mult_raw x y \<approx> mult_raw z y"
 
    89 using a
 
    88 using a
 
    90 apply(cases x, cases y, cases z)
 
    89 apply(cases x, cases y, cases z)
 
    91 apply(auto simp add: times_raw.simps intrel.simps)
 
    90 apply(auto simp add: mult_raw.simps intrel.simps)
 
    92 apply(rename_tac u v w x y z)
 
    91 apply(rename_tac u v w x y z)
 
    93 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")
 
    94 apply(simp add: mult_ac)
 
    93 apply(simp add: mult_ac)
 
    95 apply(simp add: add_mult_distrib [symmetric])
 
    94 apply(simp add: add_mult_distrib [symmetric])
 
    96 done
 
    95 done
 
    97 
    96 
    98 lemma times_raw_snd:
 
    97 lemma mult_raw_snd:
 
    99   assumes a: "x \<approx> z"
 
    98   assumes a: "x \<approx> z"
 
   100   shows "times_raw y x \<approx> times_raw y z"
 
    99   shows "mult_raw y x \<approx> mult_raw y z"
 
   101 using a
 
   100 using a
 
   102 apply(cases x, cases y, cases z)
 
   101 apply(cases x, cases y, cases z)
 
   103 apply(auto simp add: times_raw.simps intrel.simps)
 
   102 apply(auto simp add: mult_raw.simps intrel.simps)
 
   104 apply(rename_tac u v w x y z)
 
   103 apply(rename_tac u v w x y z)
 
   105 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")
 
   106 apply(simp add: mult_ac)
 
   105 apply(simp add: mult_ac)
 
   107 apply(simp add: add_mult_distrib [symmetric])
 
   106 apply(simp add: add_mult_distrib [symmetric])
 
   108 done
 
   107 done
 
   109 
   108 
   110 lemma times_raw_rsp[quot_respect]:
 
   109 lemma mult_raw_rsp[quot_respect]:
 
   111   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_raw times_raw"
 
   110   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   112 apply(simp only: fun_rel.simps)
 
   111 apply(simp only: fun_rel.simps)
 
   113 apply(rule allI | rule impI)+
 
   112 apply(rule allI | rule impI)+
 
   114 apply(rule equivp_transp[OF int_equivp])
 
   113 apply(rule equivp_transp[OF int_equivp])
 
   115 apply(rule times_raw_fst)
 
   114 apply(rule mult_raw_fst)
 
   116 apply(assumption)
 
   115 apply(assumption)
 
   117 apply(rule times_raw_snd)
 
   116 apply(rule mult_raw_snd)
 
   118 apply(assumption)
 
   117 apply(assumption)
 
   119 done
 
   118 done
 
   120 
   119 
   121 lemma less_eq_raw_rsp[quot_respect]:
 
   120 lemma le_raw_rsp[quot_respect]:
 
   122   shows "(op \<approx> ===> op \<approx> ===> op =) less_eq_raw less_eq_raw"
 
   121   shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
 
   123 by auto
 
   122 by auto
 
   124 
   123 
   125 lemma plus_assoc_raw:
 
   124 lemma plus_assoc_raw:
 
   126   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)"
 
   127 by (cases i, cases j, cases k) (simp)
 
   126 by (cases i, cases j, cases k) (simp)
 
   137 lemma plus_minus_zero_raw:
 
   136 lemma plus_minus_zero_raw:
 
   138   shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
 
   137   shows "plus_raw (uminus_raw i) i \<approx> (0, 0)"
 
   139 by (cases i) (simp)
 
   138 by (cases i) (simp)
 
   140 
   139 
   141 lemma times_assoc_raw:
 
   140 lemma times_assoc_raw:
 
   142   shows "times_raw (times_raw i j) k \<approx> times_raw i (times_raw j k)"
 
   141   shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
 
   143 by (cases i, cases j, cases k) 
   142 by (cases i, cases j, cases k) 
   144    (simp add: algebra_simps)
 
   143    (simp add: algebra_simps)
 
   145 
   144 
   146 lemma times_sym_raw:
 
   145 lemma times_sym_raw:
 
   147   shows "times_raw i j \<approx> times_raw j i"
 
   146   shows "mult_raw i j \<approx> mult_raw j i"
 
   148 by (cases i, cases j) (simp add: algebra_simps)
 
   147 by (cases i, cases j) (simp add: algebra_simps)
 
   149 
   148 
   150 lemma times_one_raw:
 
   149 lemma times_one_raw:
 
   151   shows "times_raw  (1, 0) i \<approx> i"
 
   150   shows "mult_raw  (1, 0) i \<approx> i"
 
   152 by (cases i) (simp)
 
   151 by (cases i) (simp)
 
   153 
   152 
   154 lemma times_plus_comm_raw:
 
   153 lemma times_plus_comm_raw:
 
   155   shows "times_raw (plus_raw i j) k \<approx> plus_raw (times_raw i k) (times_raw j k)"
 
   154   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 
   156 by (cases i, cases j, cases k) 
   155 by (cases i, cases j, cases k) 
   157    (simp add: algebra_simps)
 
   156    (simp add: algebra_simps)
 
   158 
   157 
   159 lemma one_zero_distinct:
 
   158 lemma one_zero_distinct:
 
   160   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
 
   159   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
 
   219 apply (induct m)
 
   218 apply (induct m)
 
   220 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
 
   219 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add)
 
   221 done
 
   220 done
 
   222 
   221 
   223 lemma le_antisym_raw:
 
   222 lemma le_antisym_raw:
 
   224   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j"
 
   223   shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
 
   225 by (cases i, cases j) (simp)
 
   224 by (cases i, cases j) (simp)
 
   226 
   225 
   227 lemma le_refl_raw:
 
   226 lemma le_refl_raw:
 
   228   shows "less_eq_raw i i"
 
   227   shows "le_raw i i"
 
   229 by (cases i) (simp)
 
   228 by (cases i) (simp)
 
   230 
   229 
   231 lemma le_trans_raw:
 
   230 lemma le_trans_raw:
 
   232   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j k \<Longrightarrow> less_eq_raw i k"
 
   231   shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
 
   233 by (cases i, cases j, cases k) (simp)
 
   232 by (cases i, cases j, cases k) (simp)
 
   234 
   233 
   235 lemma le_cases_raw:
 
   234 lemma le_cases_raw:
 
   236   shows "less_eq_raw i j \<or> less_eq_raw j i"
 
   235   shows "le_raw i j \<or> le_raw j i"
 
   237 by (cases i, cases j) 
   236 by (cases i, cases j) 
   238    (simp add: linorder_linear)
 
   237    (simp add: linorder_linear)
 
   239 
   238 
   240 instance int :: linorder
 
   239 instance int :: linorder
 
   241 proof
 
   240 proof
 
   266     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
 
   265     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
 
   267 
   266 
   268 end
 
   267 end
 
   269 
   268 
   270 lemma le_plus_raw:
 
   269 lemma le_plus_raw:
 
   271   shows "less_eq_raw i j \<Longrightarrow> less_eq_raw (plus_raw k i) (plus_raw k j)"
 
   270   shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
 
   272 by (cases i, cases j, cases k) (simp)
 
   271 by (cases i, cases j, cases k) (simp)
 
   273 
   272 
   274 
   273 
   275 instance int :: pordered_cancel_ab_semigroup_add
 
   274 instance int :: pordered_cancel_ab_semigroup_add
 
   276 proof
 
   275 proof
 
   278   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
 
   277   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
 
   279     by (lifting le_plus_raw)
 
   278     by (lifting le_plus_raw)
 
   280 qed
 
   279 qed
 
   281 
   280 
   282 abbreviation
 
   281 abbreviation
 
   283   "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)"
 
   282   "less_raw i j \<equiv> le_raw i j \<and> \<not>(i \<approx> j)"
 
   284 
   283 
   285 lemma zmult_zless_mono2_lemma:
 
   284 lemma zmult_zless_mono2_lemma:
 
   286   fixes i j::int
 
   285   fixes i j::int
 
   287   and   k::nat
 
   286   and   k::nat
 
   288   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
 
   287   shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
nominal2