IntEx.thy
changeset 321 f46dc0ca08c3
parent 320 7d3d86beacd6
child 324 bdbb52979790
equal deleted inserted replaced
320:7d3d86beacd6 321:f46dc0ca08c3
     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
     6   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
     7 where
     7 where
     8   "intrel (x, y) (u, v) = (x + v = u + y)"
     8   "intrel (x, y) (u, v) = (x + v = u + y)"
     9 
     9 
    10 quotient my_int = "nat \<times> nat" / intrel
    10 quotient my_int = "nat \<times> nat" / intrel
       
    11   and    my_int' = "nat \<times> nat" / intrel
    11   apply(unfold EQUIV_def)
    12   apply(unfold EQUIV_def)
    12   apply(auto simp add: mem_def expand_fun_eq)
    13   apply(auto simp add: mem_def expand_fun_eq)
    13   done
    14   done
    14 
    15 
       
    16 thm my_int_equiv
       
    17 
    15 print_theorems
    18 print_theorems
    16 print_quotients
    19 print_quotients
    17 
    20 
    18 quotient_def 
    21 quotient_def 
    19   ZERO::"my_int"
    22   ZERO::"my_int"
    95 where
    98 where
    96   "LE \<equiv> my_le"
    99   "LE \<equiv> my_le"
    97 
   100 
    98 term LE
   101 term LE
    99 thm LE_def
   102 thm LE_def
       
   103 
   100 
   104 
   101 definition
   105 definition
   102   LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
   106   LESS :: "my_int \<Rightarrow> my_int \<Rightarrow> bool"
   103 where
   107 where
   104   "LESS z w = (LE z w \<and> z \<noteq> w)"
   108   "LESS z w = (LE z w \<and> z \<noteq> w)"
   147 
   151 
   148 ML {* 
   152 ML {* 
   149   val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
   153   val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
   150 *}
   154 *}
   151 
   155 
   152 
   156 ML {*
   153 ML {*
   157   val aqtrm = (prop_of (atomize_thm test))
   154   val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test))
   158   val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) 
   155   val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) 
   159   val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm
   156 *}
   160 *}
   157 
   161 
       
   162 prove {* reg_artm  *}
       
   163 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
       
   164 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
       
   165 done
       
   166 
       
   167 (*
       
   168 ML {*
       
   169 fun inj_REPABS lthy rtrm qtrm =
       
   170   case (rtrm, qtrm) of
       
   171     (Abs (x, T, t), Abs (x', T', t')) =>
       
   172     if T = T'
       
   173     then Abs (x, T, inj_REPABS lthy t t')
       
   174     else 
       
   175       let 
       
   176          
       
   177       in
       
   178 
       
   179       end
       
   180   | _ => rtrm
       
   181 *}
       
   182 *)
   158 
   183 
   159 lemma plus_assoc_pre:
   184 lemma plus_assoc_pre:
   160   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
   185   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
   161   apply (cases i)
   186   apply (cases i)
   162   apply (cases j)
   187   apply (cases j)
   163   apply (cases k)
   188   apply (cases k)
   164   apply (simp)
   189   apply (simp)
   165   done
   190   done
   166 
   191 
   167 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
   192 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
   168 
   193 
       
   194 ML {*
       
   195   val aqtrm = (prop_of (atomize_thm test2))
       
   196   val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) 
       
   197 *}
       
   198 
       
   199 prove {* mk_REGULARIZE_goal @{context} artrm aqtrm  *}
       
   200 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
       
   201 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
       
   202 done
   169 
   203 
   170 
   204 
   171 
   205 
   172 
   206 
   173 
   207