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 579 eac2662a21ec
parent 570 6a031829319a
child 581 2da4fb1894d2
equal deleted inserted replaced
575:334b3e9ea3e0 579:eac2662a21ec 
    51 fun
 
    51 fun
 
    52   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    52   minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
 
    53 where
 
    53 where
 
    54   "minus_raw (x, y) = (y, x)"
 
    54   "minus_raw (x, y) = (y, x)"
 
    55 
    55 
    56 quotient_def 
    56 quotient_def
 
    57   minus_qnt::"int \<Rightarrow> int"
 
    57   minus_qnt::"int \<Rightarrow> int"
 
    58 where
 
    58 where
 
    59   "minus_qnt \<equiv> minus_raw"
 
    59   "minus_qnt \<equiv> minus_raw"
 
    60 
    60 
    61 definition minus_int_def [code del]:
 
    61 definition minus_int_def [code del]:
 
   107 thm add_assoc
 
   107 thm add_assoc
 
   108 
   108 
   109 lemma plus_raw_rsp[quotient_rsp]:
 
   109 lemma plus_raw_rsp[quotient_rsp]:
 
   110   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 
   110   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 
   111 by auto
 
   111 by auto
 
       
   112 
       
   113 lemma minus_raw_rsp[quotient_rsp]:
 
       
   114   shows "(op \<approx> ===> op \<approx>) minus_raw minus_raw"
 
       
   115   by auto
 
   112 
   116 
   113 lemma mult_raw_rsp[quotient_rsp]:
 
   117 lemma mult_raw_rsp[quotient_rsp]:
 
   114   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   118   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
 
   115 apply(auto)
 
   119 apply(auto)
 
   116 apply(simp add: mult algebra_simps)
 
   120 apply(simp add: mult algebra_simps)
 
   153   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 
   157   shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
 
   154 by (cases i, cases j, cases k) 
   158 by (cases i, cases j, cases k) 
   155    (simp add: mult algebra_simps)
 
   159    (simp add: mult algebra_simps)
 
   156 
   160 
   157 lemma one_zero_distinct:
 
   161 lemma one_zero_distinct:
 
   158   shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
 
   162   shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
 
   159   by simp
 
   163   by simp
 
   160   
   164 
   161 text{*The integers form a @{text comm_ring_1}*}
 
   165 text{*The integers form a @{text comm_ring_1}*}
 
   162 
   166 
   163 
   167 
   164 ML {* val qty = @{typ "int"} *}
 
   168 ML {* val qty = @{typ "int"} *}
 
   165 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   169 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   176     unfolding add_int_def
 
   180     unfolding add_int_def
 
   177     apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
 
   181     apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
 
   178     done
 
   182     done
 
   179   show "0 + i = (i::int)"
 
   183   show "0 + i = (i::int)"
 
   180     unfolding add_int_def Zero_int_def 
   184     unfolding add_int_def Zero_int_def 
   181     apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
 
   185     apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *})
 
   182     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
 
   186     done
 
   183     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   184     defer
 
       
   185     apply(tactic {* clean_tac @{context} 1*})
 
       
   186     sorry
 
       
   187   show "- i + i = 0"
 
   187   show "- i + i = 0"
 
   188     unfolding add_int_def minus_int_def Zero_int_def 
   188     unfolding add_int_def minus_int_def Zero_int_def 
   189     apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
 
   189     apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *})
 
   190     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
 
   190     done
 
   191     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   192     defer
 
       
   193     apply(tactic {* clean_tac @{context} 1*})
 
       
   194     sorry
 
       
   195   show "i - j = i + - j"
 
   191   show "i - j = i + - j"
 
   196     by (simp add: diff_int_def)
 
   192     by (simp add: diff_int_def)
 
   197   show "(i * j) * k = i * (j * k)"
 
   193   show "(i * j) * k = i * (j * k)"
 
   198     unfolding mult_int_def 
   194     unfolding mult_int_def 
   199     apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
 
   195     apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *})
 
   200     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
 
   196     done
 
   201     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   202     defer
 
       
   203     apply(tactic {* clean_tac @{context} 1*})
 
       
   204     sorry
 
       
   205   show "i * j = j * i"
 
   197   show "i * j = j * i"
 
   206     unfolding mult_int_def 
   198     unfolding mult_int_def 
   207     apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
 
   199     apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *})
 
   208     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
 
   200     done
 
   209     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   210     defer
 
       
   211     apply(tactic {* clean_tac @{context} 1*})
 
       
   212     sorry
 
       
   213   show "1 * i = i"
 
   201   show "1 * i = i"
 
   214     unfolding mult_int_def One_int_def
 
   202     unfolding mult_int_def One_int_def
 
   215     apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
 
   203     apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *})
 
   216     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
 
   204     done
 
   217     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   218     defer
 
       
   219     apply(tactic {* clean_tac @{context} 1*})
 
       
   220     sorry
 
       
   221   show "(i + j) * k = i * k + j * k"
 
   205   show "(i + j) * k = i * k + j * k"
 
   222     unfolding mult_int_def add_int_def
 
   206     unfolding mult_int_def add_int_def
 
   223     apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
 
   207     apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *})
 
   224     apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
 
   208     done
 
   225     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   226     defer
 
       
   227     apply(tactic {* clean_tac @{context} 1*})
 
       
   228     sorry
 
       
   229   show "0 \<noteq> (1::int)"
 
   209   show "0 \<noteq> (1::int)"
 
   230     unfolding Zero_int_def One_int_def
 
   210     unfolding Zero_int_def One_int_def
 
   231     apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
 
   211     apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *})
 
   232     defer
 
   212     done
 
   233     defer
 
       
   234     apply(tactic {* clean_tac @{context} 1*})
 
       
   235     sorry
 
       
   236 qed
 
   213 qed
 
   237 
   214 
   238 term of_nat
 
   215 term of_nat
 
   239 thm of_nat_def
 
   216 thm of_nat_def
 
   240 
   217 
   314     apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
 
   291     apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
 
   315     done
 
   292     done
 
   316 qed
 
   293 qed
 
   317 
   294 
   318 lemma test:
 
   295 lemma test:
 
   319   "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
 
   296   "\<lbrakk>le_raw i j \<and> \<not>i \<approx> j; le_raw (0, 0) k \<and> \<not>(0, 0) \<approx> k\<rbrakk>
 
   320     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
 
   297     \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> \<not>mult_raw k i \<approx> mult_raw k j"
 
   321 apply(cases i, cases j, cases k)
 
   298 apply(cases i, cases j, cases k)
 
   322 apply(auto simp add: mult algebra_simps)
 
   299 apply(auto simp add: mult algebra_simps)
 
   323 sorry
 
   300 sorry
 
   324 
   301 
   325 
   302 
   327 instance int :: ordered_idom
 
   304 instance int :: ordered_idom
 
   328 proof
 
   305 proof
 
   329   fix i j k :: int
 
   306   fix i j k :: int
 
   330   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
 
   307   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
 
   331     unfolding mult_int_def le_int_def less_int_def Zero_int_def
 
   308     unfolding mult_int_def le_int_def less_int_def Zero_int_def
 
   332     apply(tactic {* procedure_tac @{context} @{thm test} 1 *})
 
   309     apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *})
 
   333     defer
 
   310     done
 
   334     apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
 
       
   335     defer
 
       
   336     apply(tactic {* clean_tac @{context} 1*})
 
       
   337     sorry
 
       
   338   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
 
   311   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
 
   339     by (simp only: zabs_def)
 
   312     by (simp only: zabs_def)
 
   340   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
 
   313   show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
 
   341     by (simp only: zsgn_def)
 
   314     by (simp only: zsgn_def)
 
   342 qed
 
   315 qed
nominal2