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.
IntEx2.thy
changeset 584 97f6e5c61f03
parent 582 a082e2d138ab
parent 581 2da4fb1894d2
child 585 b16cac0b7c88
equal deleted inserted replaced
583:7414f6cb5398 584:97f6e5c61f03 
    52 fun
 
    52 fun
 
    53   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    53   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    54 where
 
    54 where
 
    55   "minus_raw (x, y) = (y, x)"
 
    55   "minus_raw (x, y) = (y, x)"
 
    56 
    56 
    57 quotient_def 
    57 quotient_def
 
    58   minus_qnt::"int \<Rightarrow> int"
 
    58   minus_qnt::"int \<Rightarrow> int"
 
    59 where
 
    59 where
 
    60   "minus_qnt \<equiv> minus_raw"
 
    60   "minus_qnt \<equiv> minus_raw"
 
    61 
    61 
    62 definition minus_int_def [code del]:
 
    62 definition minus_int_def [code del]:
 
   108 thm add_assoc
 
   108 thm add_assoc
 
   109 
   109 
   110 lemma plus_raw_rsp[quotient_rsp]:
 
   110 lemma plus_raw_rsp[quotient_rsp]:
 
   111   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 
   111   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 
   112 by auto
 
   112 by auto
 
       
   113 
       
   114 lemma minus_raw_rsp[quotient_rsp]:
 
       
   115   shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
 
       
   116   by auto
 
   113 
   117 
   114 lemma mult_raw_rsp[quotient_rsp]:
 
   118 lemma mult_raw_rsp[quotient_rsp]:
 
   115   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   119   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   116 apply(auto)
 
   120 apply(auto)
 
   117 apply(simp add: mult algebra_simps)
 
   121 apply(simp add: mult algebra_simps)
 
   154   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 
   158   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) 
   159 by (cases i, cases j, cases k) 
   156    (simp add: mult algebra_simps)
 
   160    (simp add: mult algebra_simps)
 
   157 
   161 
   158 lemma one_zero_distinct:
 
   162 lemma one_zero_distinct:
 
   159   shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
 
   163   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
 
   160   by simp
 
   164   by simp
 
   161   
   165 
   162 text{*The integers form a @{text comm_ring_1}*}
 
   166 text{*The integers form a @{text comm_ring_1}*}
 
   163 
   167 
   164 
   168 
   165 ML {* val qty = @{typ "int"} *}
 
   169 ML {* val qty = @{typ "int"} *}
 
   166 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   170 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   169 instance int :: comm_ring_1
 
   173 instance int :: comm_ring_1
 
   170 proof
 
   174 proof
 
   171   fix i j k :: int
 
   175   fix i j k :: int
 
   172   show "(i + j) + k = i + (j + k)"
 
   176   show "(i + j) + k = i + (j + k)"
 
   173     unfolding add_int_def
 
   177     unfolding add_int_def
 
   174     apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})
 
   178     apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
 
   175     done
 
   179     done
 
   176   show "i + j = j + i" 
   180   show "i + j = j + i" 
   177     unfolding add_int_def
 
   181     unfolding add_int_def
 
   178     apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
 
   182     apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
 
   179     done
 
   183     done
 
   180   show "0 + i = (i::int)"
 
   184   show "0 + i = (i::int)"
 
   181     unfolding add_int_def Zero_int_def 
   185     unfolding add_int_def Zero_int_def 
   182     apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
 
   186     apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *})
 
   183     apply(tactic {* regularize_tac @{context} 1 *})
 
   187     done
 
   184     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   185     defer
 
       
   186     apply(tactic {* clean_tac @{context} 1*})
 
       
   187     sorry
 
       
   188   show "- i + i = 0"
 
   188   show "- i + i = 0"
 
   189     unfolding add_int_def minus_int_def Zero_int_def 
   189     unfolding add_int_def minus_int_def Zero_int_def 
   190     apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
 
   190     apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *})
 
   191     apply(tactic {* regularize_tac @{context} 1 *})
 
   191     done
 
   192     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   193     defer
 
       
   194     apply(tactic {* clean_tac @{context} 1*})
 
       
   195     sorry
 
       
   196   show "i - j = i + - j"
 
   192   show "i - j = i + - j"
 
   197     by (simp add: diff_int_def)
 
   193     by (simp add: diff_int_def)
 
   198   show "(i * j) * k = i * (j * k)"
 
   194   show "(i * j) * k = i * (j * k)"
 
   199     unfolding mult_int_def 
   195     unfolding mult_int_def 
   200     apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
 
   196     apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *})
 
   201     apply(tactic {* regularize_tac @{context} 1 *})
 
   197     done
 
   202     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   203     defer
 
       
   204     apply(tactic {* clean_tac @{context} 1*})
 
       
   205     sorry
 
       
   206   show "i * j = j * i"
 
   198   show "i * j = j * i"
 
   207     unfolding mult_int_def 
   199     unfolding mult_int_def 
   208     apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
 
   200     apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *})
 
   209     apply(tactic {* regularize_tac @{context} 1 *})
 
   201     done
 
   210     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   211     defer
 
       
   212     apply(tactic {* clean_tac @{context} 1*})
 
       
   213     sorry
 
       
   214   show "1 * i = i"
 
   202   show "1 * i = i"
 
   215     unfolding mult_int_def One_int_def
 
   203     unfolding mult_int_def One_int_def
 
   216     apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
 
   204     apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *})
 
   217     apply(tactic {* regularize_tac @{context} 1 *})
 
   205     done
 
   218     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   219     defer
 
       
   220     apply(tactic {* clean_tac @{context} 1*})
 
       
   221     sorry
 
       
   222   show "(i + j) * k = i * k + j * k"
 
   206   show "(i + j) * k = i * k + j * k"
 
   223     unfolding mult_int_def add_int_def
 
   207     unfolding mult_int_def add_int_def
 
   224     apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
 
   208     apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *})
 
   225     apply(tactic {* regularize_tac @{context} 1 *})
 
   209     done
 
   226     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   227     defer
 
       
   228     apply(tactic {* clean_tac @{context} 1*})
 
       
   229     sorry
 
       
   230   show "0 \<noteq> (1::int)"
 
   210   show "0 \<noteq> (1::int)"
 
   231     unfolding Zero_int_def One_int_def
 
   211     unfolding Zero_int_def One_int_def
 
   232     apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
 
   212     apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *})
 
   233     defer
 
   213     done
 
   234     defer
 
       
   235     apply(tactic {* clean_tac @{context} 1*})
 
       
   236     sorry
 
       
   237 qed
 
   214 qed
 
   238 
   215 
   239 term of_nat
 
   216 term of_nat
 
   240 thm of_nat_def
 
   217 thm of_nat_def
 
   241 
   218 
   267 instance int :: linorder
 
   244 instance int :: linorder
 
   268 proof
 
   245 proof
 
   269   fix i j k :: int
 
   246   fix i j k :: int
 
   270   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
 
   247   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
 
   271     unfolding le_int_def
 
   248     unfolding le_int_def
 
   272     apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})
 
   249     apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
 
   273     done
 
   250     done
 
   274   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
 
   251   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
 
   275     by (auto simp add: less_int_def dest: antisym) 
   252     by (auto simp add: less_int_def dest: antisym) 
   276   show "i \<le> i"
 
   253   show "i \<le> i"
 
   277     unfolding le_int_def
 
   254     unfolding le_int_def
 
   278     apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})
 
   255     apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
 
   279     done
 
   256     done
 
   280   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
 
   257   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
 
   281     unfolding le_int_def
 
   258     unfolding le_int_def
 
   282     apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})
 
   259     apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
 
   283     done
 
   260     done
 
   284   show "i \<le> j \<or> j \<le> i"
 
   261   show "i \<le> j \<or> j \<le> i"
 
   285     unfolding le_int_def
 
   262     unfolding le_int_def
 
   286     apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
 
   263     apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
 
   287     done
 
   264     done
 
   288 qed
 
   265 qed
 
   289 
   266 
   290 instantiation int :: distrib_lattice
 
   267 instantiation int :: distrib_lattice
 
   291 begin
 
   268 begin
 
   310 instance int :: pordered_cancel_ab_semigroup_add
 
   287 instance int :: pordered_cancel_ab_semigroup_add
 
   311 proof
 
   288 proof
 
   312   fix i j k :: int
 
   289   fix i j k :: int
 
   313   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
 
   290   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
 
   314     unfolding le_int_def add_int_def
 
   291     unfolding le_int_def add_int_def
 
   315     apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})
 
   292     apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
 
   316     done
 
   293     done
 
   317 qed
 
   294 qed
 
   318 
   295 
   319 lemma test:
 
   296 lemma test:
 
   320   "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
 
   297   "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
 
   321     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
 
   298     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
 
   322 apply(cases i, cases j, cases k)
 
   299 apply(cases i, cases j, cases k)
 
   323 apply(auto simp add: mult algebra_simps)
 
   300 apply(auto simp add: mult algebra_simps)
 
   324 sorry
 
   301 sorry
 
   325 
   302 
   326 
   303 
   328 instance int :: ordered_idom
 
   305 instance int :: ordered_idom
 
   329 proof
 
   306 proof
 
   330   fix i j k :: int
 
   307   fix i j k :: int
 
   331   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
 
   308   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
 
   332     unfolding mult_int_def le_int_def less_int_def Zero_int_def
 
   309     unfolding mult_int_def le_int_def less_int_def Zero_int_def
 
   333     apply(tactic {* procedure_tac @{context} @{thm test} 1 *})
 
   310     apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *})
 
   334     defer
 
   311     done
 
   335     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   336     defer
 
       
   337     apply(tactic {* clean_tac @{context} 1*})
 
       
   338     sorry
 
       
   339   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
 
   312   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
 
   340     by (simp only: zabs_def)
 
   313     by (simp only: zabs_def)
 
   341   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
 
   314   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
 
   342     by (simp only: zsgn_def)
 
   315     by (simp only: zsgn_def)
 
   343 qed
 
   316 qed
nominal2