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.
QuotMain.thy
changeset 405 8bc7428745ad
parent 404 d676974e3c89
child 407 d387743f022b
equal deleted inserted replaced
404:d676974e3c89 405:8bc7428745ad 
   379 *}
 
   379 *}
 
   380 
   380 
   381 ML {*
 
   381 ML {*
 
   382 (* - applies f to the subterm of an abstraction,   *)
 
   382 (* - applies f to the subterm of an abstraction,   *)
 
   383 (*   otherwise to the given term,                  *)
 
   383 (*   otherwise to the given term,                  *)
 
   384 (* - used by REGULARIZE, therefore abstracted      *)
 
   384 (* - used by regularize, therefore abstracted      *)
 
   385 (*   variables do not have to be treated specially *)
 
   385 (*   variables do not have to be treated specially *)
 
   386 
   386 
   387 fun apply_subt f trm1 trm2 =
 
   387 fun apply_subt f trm1 trm2 =
 
   388   case (trm1, trm2) of
 
   388   case (trm1, trm2) of
 
   389     (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
 
   389     (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
 
   397 (* produces a regularized version of rtm      *)
 
   397 (* produces a regularized version of rtm      *)
 
   398 (* - the result is still not completely typed *)
 
   398 (* - the result is still not completely typed *)
 
   399 (* - does not need any special treatment of   *)
 
   399 (* - does not need any special treatment of   *)
 
   400 (*   bound variables                          *)
 
   400 (*   bound variables                          *)
 
   401 
   401 
   402 fun REGULARIZE_trm lthy rtrm qtrm =
 
   402 fun regularize_trm lthy rtrm qtrm =
 
   403   case (rtrm, qtrm) of
 
   403   case (rtrm, qtrm) of
 
   404     (Abs (x, ty, t), Abs (x', ty', t')) =>
 
   404     (Abs (x, ty, t), Abs (x', ty', t')) =>
 
   405        let
 
   405        let
 
   406          val subtrm = REGULARIZE_trm lthy t t'
 
   406          val subtrm = regularize_trm lthy t t'
 
   407        in     
   407        in     
   408          if ty = ty'
 
   408          if ty = ty'
 
   409          then Abs (x, ty, subtrm)
 
   409          then Abs (x, ty, subtrm)
 
   410          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
 
   410          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
 
   411        end
 
   411        end
 
   412   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
 
   412   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
 
   413        let
 
   413        let
 
   414          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
 
   414          val subtrm = apply_subt (regularize_trm lthy) t t'
 
   415        in
 
   415        in
 
   416          if ty = ty'
 
   416          if ty = ty'
 
   417          then Const (@{const_name "All"}, ty) $ subtrm
 
   417          then Const (@{const_name "All"}, ty) $ subtrm
 
   418          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
 
   418          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
 
   419        end
 
   419        end
 
   420   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
 
   420   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
 
   421        let
 
   421        let
 
   422          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
 
   422          val subtrm = apply_subt (regularize_trm lthy) t t'
 
   423        in
 
   423        in
 
   424          if ty = ty'
 
   424          if ty = ty'
 
   425          then Const (@{const_name "Ex"}, ty) $ subtrm
 
   425          then Const (@{const_name "Ex"}, ty) $ subtrm
 
   426          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
 
   426          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
 
   427        end
 
   427        end
 
   428     (* FIXME: Should = only be replaced, when fully applied? *) 
   428     (* FIXME: Should = only be replaced, when fully applied? *) 
   429     (* Then there must be a 2nd argument                     *)
 
   429     (* Then there must be a 2nd argument                     *)
 
   430   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
 
   430   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
 
   431        let
 
   431        let
 
   432          val subtrm = REGULARIZE_trm lthy t t'
 
   432          val subtrm = regularize_trm lthy t t'
 
   433        in
 
   433        in
 
   434          if ty = ty'
 
   434          if ty = ty'
 
   435          then Const (@{const_name "op ="}, ty) $ subtrm
 
   435          then Const (@{const_name "op ="}, ty) $ subtrm
 
   436          else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
 
   436          else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
 
   437        end 
   437        end 
   438   | (t1 $ t2, t1' $ t2') =>
 
   438   | (t1 $ t2, t1' $ t2') =>
 
   439        (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
 
   439        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
 
   440   | (Free (x, ty), Free (x', ty')) =>
 
   440   | (Free (x, ty), Free (x', ty')) =>
 
   441        if x = x' 
   441        if x = x' 
   442        then rtrm     (* FIXME: check whether types corresponds *)
 
   442        then rtrm     (* FIXME: check whether types corresponds *)
 
   443        else raise (LIFT_MATCH "regularize (frees)")
 
   443        else raise (LIFT_MATCH "regularize (frees)")
 
   444   | (Bound i, Bound i') =>
 
   444   | (Bound i, Bound i') =>
 
   475   assumes a: "c \<longrightarrow> a"
 
   475   assumes a: "c \<longrightarrow> a"
 
   476   assumes b: "b \<longrightarrow> d"
 
   476   assumes b: "b \<longrightarrow> d"
 
   477   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
   477   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
   478 using a b by auto
 
   478 using a b by auto
 
   479 
   479 
   480 (* version of REGULARIZE_tac including debugging information *)
 
   480 (* version of regularize_tac including debugging information *)
 
   481 ML {*
 
   481 ML {*
 
   482 fun my_print_tac ctxt s thm =
 
   482 fun my_print_tac ctxt s thm =
 
   483 let
 
   483 let
 
   484   val prems_str = prems_of thm
 
   484   val prems_str = prems_of thm
 
   485                   |> map (Syntax.string_of_term ctxt)
 
   485                   |> map (Syntax.string_of_term ctxt)
 
  1113 let
 
  1113 let
 
  1114   val thy = ProofContext.theory_of ctxt
 
  1114   val thy = ProofContext.theory_of ctxt
 
  1115   val rtrm' = HOLogic.dest_Trueprop rtrm
 
  1115   val rtrm' = HOLogic.dest_Trueprop rtrm
 
  1116   val qtrm' = HOLogic.dest_Trueprop qtrm
 
  1116   val qtrm' = HOLogic.dest_Trueprop qtrm
 
  1117   val reg_goal = 
  1117   val reg_goal = 
  1118         Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
 
  1118         Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
 
  1119         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 
  1119         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 
  1120   val inj_goal = 
  1120   val inj_goal = 
  1121         Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
 
  1121         Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
 
  1122         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 
  1122         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 
  1123 in
 
  1123 in
nominal2