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.
IntEx.thy
changeset 330 1a0f0b758071
parent 329 5d06e1dba69a
child 334 5a7024be9083
equal deleted inserted replaced
329:5d06e1dba69a 330:1a0f0b758071 
   116 
   116 
   117 definition
 
   117 definition
 
   118   SIGN :: "my_int \<Rightarrow> my_int"
 
   118   SIGN :: "my_int \<Rightarrow> my_int"
 
   119 where
 
   119 where
 
   120  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
   120  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
   121 
       
   122 
       
   123 
       
   124 ML {* print_qconstinfo @{context} *}
 
       
   125 
   121 
   126 ML {* print_qconstinfo @{context} *}
 
   122 ML {* print_qconstinfo @{context} *}
 
   127 
   123 
   128 lemma plus_sym_pre:
 
   124 lemma plus_sym_pre:
 
   129   shows "my_plus a b \<approx> my_plus b a"
 
   125   shows "my_plus a b \<approx> my_plus b a"
 
   163 prove {* reg_artm  *}
 
   159 prove {* reg_artm  *}
 
   164 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 
   160 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 
   165 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
 
   161 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
 
   166 done
 
   162 done
 
   167 
   163 
   168 ML {*
 
   164 (* rep-abs injection *)
 
       
   165 
       
   166 ML {*
 
       
   167 (* FIXME: is this the right get_fun function for rep-abs injection *)
 
   169 fun mk_repabs lthy (T, T') trm = 
   168 fun mk_repabs lthy (T, T') trm = 
   170   Quotient_Def.get_fun repF lthy (T, T') 
   169   Quotient_Def.get_fun repF lthy (T, T') 
   171   $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
 
   170   $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
 
   172 *}
 
   171 *}
 
   173 
   172 
   174 ML {*
 
   173 ML {*
 
       
   174 (* replaces a term for the bound variable, *)
 
       
   175 (* possible capture                        *)
 
   175 fun replace_bnd0 (trm, Abs (x, T, t)) =
 
   176 fun replace_bnd0 (trm, Abs (x, T, t)) =
 
   176   Abs (x, T, subst_bound (trm, t))
 
   177   Abs (x, T, subst_bound (trm, t))
 
   177 *}
 
   178 *}
 
   178 
   179 
   179 ML {*
 
   180 ML {*
 
       
   181 (* bound variables need to be treated properly,  *)
 
       
   182 (* as the type of subterms need to be calculated *)
 
       
   183 
   180 fun inj_REPABS lthy (rtrm, qtrm) =
 
   184 fun inj_REPABS lthy (rtrm, qtrm) =
 
   181 let
 
   185 let
 
   182   val rty = fastype_of rtrm
 
   186   val rty = fastype_of rtrm
 
   183   val qty = fastype_of qtrm
 
   187   val qty = fastype_of qtrm
 
   184 in
 
   188 in
 
   185   case (rtrm, qtrm) of
 
   189   case (rtrm, qtrm) of
 
   186     (Abs (x, T, t), Abs (x', T', t')) =>
 
   190     (Abs (x, T, t), Abs (x', T', t')) =>
 
   187     let
 
   191       let
 
   188       val (y, s) = Term.dest_abs (x, T, t)
 
   192         val (y, s) = Term.dest_abs (x, T, t)
 
   189       val (y', s') = Term.dest_abs (x', T', t')
 
   193         val (y', s') = Term.dest_abs (x', T', t')
 
   190       val yvar = Free (y, T)
 
   194         val yvar = Free (y, T)
 
   191       val res = lambda yvar (inj_REPABS lthy (s, s'))
 
   195         val res = lambda yvar (inj_REPABS lthy (s, s'))
 
   192     in
 
   196       in
 
   193       if T = T'
 
   197         if T = T'
 
   194       then res
 
   198         then res
 
   195       else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
 
   199         else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
 
   196     end
 
   200       end
 
   197   (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) 
   201   (* FIXME: Does one have to look at the abstraction or have to go under the lambda? *) 
   198   | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
 
   202   | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
 
   199       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
 
   203        Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
 
   200   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
 
   204   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
 
   201       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
 
   205        Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
 
   202   | (rtrm as _ $ _, qtrm as _ $ _) => 
   206   | (_ $ _, _ $ _) => 
   203     let
 
   207       let
 
   204       val (rhead, rargs) = Term.strip_comb rtrm
 
   208         val (rhead, rargs) = strip_comb rtrm
 
   205       val (qhead, qargs) = Term.strip_comb qtrm
 
   209         val (qhead, qargs) = strip_comb qtrm
 
   206       val rhead' = inj_REPABS lthy (rhead, qhead)
 
   210         val rhead' = inj_REPABS lthy (rhead, qhead)
 
   207       val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
 
   211         val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
 
   208       val res = list_comb (rhead', rargs')
 
   212         val result = list_comb (rhead', rargs')
 
   209     in
 
   213       in
 
   210       if rty = qty
 
   214         if rty = qty
 
   211       then res
 
   215         then result
 
   212       else mk_repabs lthy (rty, qty) res
 
   216         else mk_repabs lthy (rty, qty) res
 
   213     end
 
   217       end
 
   214   (* FIXME: cases for frees and vars *)
 
   218   (* FIXME: cases for frees and vars? *)
 
   215   | _ => rtrm
 
   219   | _ => rtrm
 
   216 end
 
   220 end
 
   217 *}
 
   221 *}
 
   218 
   222 
   219 ML {*
 
   223 ML {*
 
   276 *}
 
   280 *}
 
   277 
   281 
   278 ML {* cprem_of *}
 
   282 ML {* cprem_of *}
 
   279 
   283 
   280 ML {* 
   284 ML {* 
   281 (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
   285 mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
   282   |> Syntax.check_term @{context})
 
   286   |> Syntax.check_term @{context}
 
   283 *}
 
   287 *}
 
   284 
   288 
   285 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
 
   289 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
 
   286 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 
   290 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 
   287 (* does not work *)
 
   291 (* does not work *)
 
   291 ML {*
 
   295 ML {*
 
   292 inj_REPABS @{context} (reg_atrm, aqtrm)  
   296 inj_REPABS @{context} (reg_atrm, aqtrm)  
   293 |> Syntax.string_of_term @{context}
 
   297 |> Syntax.string_of_term @{context}
 
   294 |> writeln
 
   298 |> writeln
 
   295 *}
 
   299 *}
 
   296 
       
   297 
       
   298 
       
   299 
       
   300 
       
   301 
       
   302 
   300 
   303 
   301 
   304 lemma ho_tst: "foldl my_plus x [] = x"
 
   302 lemma ho_tst: "foldl my_plus x [] = x"
 
   305 apply simp
 
   303 apply simp
 
   306 done
 
   304 done
nominal2