1 theory IntEx

     2 imports QuotMain

     3 begin

     4 

     5 fun

     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)

     7 where

     8   "intrel (x, y) (u, v) = (x + v = u + y)"

     9 

    10 quotient my_int = "nat \<times> nat" / intrel

    11   apply(unfold equivp_def)

    12   apply(auto simp add: mem_def expand_fun_eq)

    13   done

    14 

    15 thm quotient_equiv

    16 

    17 thm quotient_thm

    18 

    19 thm my_int_equivp

    20 

    21 print_theorems

    22 print_quotients

    23 

    24 quotient_def 

    25   ZERO::"my_int"

    26 where

    27   "ZERO \<equiv> (0::nat, 0::nat)"

    28 

    29 ML {* print_qconstinfo @{context} *}

    30 

    31 term ZERO

    32 thm ZERO_def

    33 

    34 ML {* prop_of @{thm ZERO_def} *}

    35 

    36 ML {* separate *}

    37 

    38 quotient_def 

    39   ONE::"my_int"

    40 where

    41   "ONE \<equiv> (1::nat, 0::nat)"

    42 

    43 ML {* print_qconstinfo @{context} *}

    44 

    45 term ONE

    46 thm ONE_def

    47 

    48 fun

    49   my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    50 where

    51   "my_plus (x, y) (u, v) = (x + u, y + v)"

    52 

    53 quotient_def 

    54   PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"

    55 where

    56   "PLUS \<equiv> my_plus"

    57 

    58 term my_plus

    59 term PLUS

    60 thm PLUS_def

    61 

    62 fun

    63   my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    64 where

    65   "my_neg (x, y) = (y, x)"

    66 

    67 quotient_def 

    68   NEG::"my_int \<Rightarrow> my_int"

    69 where

    70   "NEG \<equiv> my_neg"

    71 

    72 term NEG

    73 thm NEG_def

    74 

    75 definition

    76   MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int"

    77 where

    78   "MINUS z w = PLUS z (NEG w)"

    79 

    80 fun

    81   my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"

    82 where

    83   "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)"

    84 

    85 quotient_def 

    86   MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int"

    87 where

    88   "MULT \<equiv> my_mult"

    89 

    90 term MULT

    91 thm MULT_def

    92 

    93 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *)

    94 fun

    95   my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"

    96 where

    97   "my_le (x, y) (u, v) = (x+v \<le> u+y)"

    98 

    99 quotient_def 

   100   LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"

   101 where

   102   "LE \<equiv> my_le"

   103 

   104 term LE

   105 thm LE_def

   106 

   107 

   108 definition

   109   LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"

   110 where

   111   "LESS z w = (LE z w \<and> z \<noteq> w)"

   112 

   113 term LESS

   114 thm LESS_def

   115 

   116 definition

   117   ABS :: "my_int \<Rightarrow> my_int"

   118 where

   119   "ABS i = (if (LESS i ZERO) then (NEG i) else i)"

   120 

   121 definition

   122   SIGN :: "my_int \<Rightarrow> my_int"

   123 where

   124  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"

   125 

   126 ML {* print_qconstinfo @{context} *}

   127 

   128 lemma plus_sym_pre:

   129   shows "my_plus a b \<approx> my_plus b a"

   130   apply(cases a)

   131   apply(cases b)

   132   apply(auto)

   133   done

   134 

   135 lemma plus_rsp[quotient_rsp]:

   136   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"

   137 by (simp)

   138 

   139 ML {* val qty = @{typ "my_int"} *}

   140 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}

   141 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}

   142 

   143 ML {* fun lift_tac_intex lthy t = lift_tac lthy t *}

   144 

   145 ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}

   146 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}

   147 

   148 lemma test1: "my_plus a b = my_plus a b"

   149 apply(rule refl)

   150 done

   151 

   152 lemma "PLUS a b = PLUS a b"

   153 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})

   154 apply(tactic {* regularize_tac @{context} 1 *})

   155 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   156 apply(tactic {* clean_tac @{context} 1 *}) 

   157 done

   158 

   159 thm lambda_prs

   160 

   161 lemma test2: "my_plus a = my_plus a"

   162 apply(rule refl)

   163 done

   164 

   165 lemma "PLUS a = PLUS a"

   166 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})

   167 apply(rule ballI)

   168 apply(rule apply_rsp[OF Quotient_my_int plus_rsp])

   169 apply(simp only: in_respects)

   170 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   171 apply(tactic {* clean_tac @{context} 1 *})

   172 done

   173 

   174 lemma test3: "my_plus = my_plus"

   175 apply(rule refl)

   176 done

   177 

   178 lemma "PLUS = PLUS"

   179 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})

   180 apply(rule plus_rsp)

   181 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   182 apply(tactic {* clean_tac @{context} 1 *})

   183 done

   184 

   185 

   186 lemma "PLUS a b = PLUS b a"

   187 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})

   188 apply(tactic {* regularize_tac @{context} 1 *})

   189 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   190 apply(tactic {* clean_tac @{context} 1 *})

   191 done

   192 

   193 lemma plus_assoc_pre:

   194   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"

   195   apply (cases i)

   196   apply (cases j)

   197   apply (cases k)

   198   apply (simp)

   199   done

   200 

   201 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"

   202 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})

   203 apply(tactic {* regularize_tac @{context} 1 *})

   204 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   205 apply(tactic {* clean_tac @{context} 1 *})

   206 done

   207 

   208 lemma ho_tst: "foldl my_plus x [] = x"

   209 apply simp

   210 done

   211 

   212 lemma "foldl PLUS x [] = x"

   213 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})

   214 apply(tactic {* regularize_tac @{context} 1 *})

   215 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   216 apply(tactic {* clean_tac @{context} 1 *})

   217 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])

   218 done

   219 

   220 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"

   221 sorry

   222 

   223 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"

   224 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})

   225 apply(tactic {* regularize_tac @{context} 1 *})

   226 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   227 apply(tactic {* clean_tac @{context} 1 *})

   228 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])

   229 done

   230 

   231 lemma ho_tst3: "foldl f (s::nat \<times> nat) ([]::(nat \<times> nat) list) = s"

   232 by simp

   233 

   234 lemma "foldl f (x::my_int) ([]::my_int list) = x"

   235 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})

   236 apply(tactic {* regularize_tac @{context} 1 *})

   237 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   238 (* TODO: does not work when this is added *)

   239 (* apply(tactic {* lambda_prs_tac @{context} 1 *})*)

   240 apply(tactic {* clean_tac @{context} 1 *})

   241 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])

   242 done

   243 

   244 lemma lam_tst: "(\<lambda>x. (x, x)) y = (y, (y :: nat \<times> nat))"

   245 by simp

   246 

   247 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"

   248 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})

   249 apply(tactic {* regularize_tac @{context} 1 *})

   250 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   251 apply(tactic {* clean_tac @{context} 1 *})

   252 apply(simp add: pair_prs)

   253 done

   254 

   255 lemma lam_tst2: "(\<lambda>(y :: nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat). x)"

   256 by simp

   257 

   258 

   259 

   260 

   261 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"

   262 apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *})

   263 defer

   264 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   265 (*apply(tactic {* lambda_prs_tac  @{context} 1 *})*)

   266 sorry

   267 

   268 lemma lam_tst3: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"

   269 by auto

   270 

   271 lemma "(\<lambda>(y :: my_int \<Rightarrow> my_int). y) = (\<lambda>(x :: my_int \<Rightarrow> my_int). x)"

   272 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *})

   273 defer

   274 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   275 apply(tactic {* lambda_prs_tac  @{context} 1 *})

   276 sorry