--- a/QuotMain.thy Fri Oct 30 15:52:47 2009 +0100
+++ b/QuotMain.thy Fri Oct 30 16:24:07 2009 +0100
@@ -447,106 +447,6 @@
*}
ML {*
-(* trm \<Rightarrow> new_trm *)
-fun regularise trm rty rel lthy =
- case trm of
- Abs (x, T, t) =>
- if (needs_lift rty T) then let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term;
- val sub_res_term = tyRel T rty rel lthy;
- val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
- val res_term = respects $ sub_res_term;
- val ty = fastype_of trm;
- val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
- val rabs_term = (rabs $ res_term) $ lam_term;
- in
- rabs_term
- end else let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- in
- Term.lambda_name (x, v) rec_term
- end
- | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
- if (needs_lift rty T) then let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term;
- val sub_res_term = tyRel T rty rel lthy;
- val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
- val res_term = respects $ sub_res_term;
- val ty = fastype_of lam_term;
- val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
- val rall_term = (rall $ res_term) $ lam_term;
- in
- rall_term
- end else let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term
- in
- Const(@{const_name "All"}, at) $ lam_term
- end
- | ((Const (@{const_name "All"}, at)) $ P) =>
- let
- val (_, [al, _]) = dest_Type (fastype_of P);
- val ([x], lthy2) = Variable.variant_fixes [""] lthy;
- val v = (Free (x, al));
- val abs = Term.lambda_name (x, v) (P $ v);
- in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
- | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
- if (needs_lift rty T) then let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term;
- val sub_res_term = tyRel T rty rel lthy;
- val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
- val res_term = respects $ sub_res_term;
- val ty = fastype_of lam_term;
- val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
- val rall_term = (rall $ res_term) $ lam_term;
- in
- rall_term
- end else let
- val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
- val v = Free (x', T);
- val t' = subst_bound (v, t);
- val rec_term = regularise t' rty rel lthy2;
- val lam_term = Term.lambda_name (x, v) rec_term
- in
- Const(@{const_name "Ex"}, at) $ lam_term
- end
- | ((Const (@{const_name "Ex"}, at)) $ P) =>
- let
- val (_, [al, _]) = dest_Type (fastype_of P);
- val ([x], lthy2) = Variable.variant_fixes [""] lthy;
- val v = (Free (x, al));
- val abs = Term.lambda_name (x, v) (P $ v);
- in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
- | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
- | _ => trm
-
-*}
-
-(* my version of regularise *)
-(****************************)
-
-(* some helper functions *)
-
-
-ML {*
fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
@@ -566,47 +466,51 @@
| _ => f trm
*}
-
-(* FIXME: assumes always the typ is qty! *)
(* FIXME: if there are more than one quotient, then you have to look up the relation *)
ML {*
-fun my_reg rel trm =
+fun my_reg lthy rel rty trm =
case trm of
Abs (x, T, t) =>
- let
- val ty1 = fastype_of trm
- in
- (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm)
- end
- | Const (@{const_name "All"}, ty) $ t =>
- let
+ if (needs_lift rty T) then
+ let
+ val rrel = tyRel T rty rel lthy
+ in
+ (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
+ end
+ else
+ Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
+ | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
+ let
val ty1 = domain_type ty
val ty2 = domain_type ty1
+ val rrel = tyRel T rty rel lthy
in
- (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
+ if (needs_lift rty T) then
+ (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+ else
+ Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
end
- | Const (@{const_name "Ex"}, ty) $ t =>
- let
+ | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
+ let
val ty1 = domain_type ty
val ty2 = domain_type ty1
+ val rrel = tyRel T rty rel lthy
in
- (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)
+ if (needs_lift rty T) then
+ (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
+ else
+ Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
end
- | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
+ | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
| _ => trm
*}
-
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
- trm == new_trm
-*)
-
text {* Assumes that the given theorem is atomized *}
ML {*
fun build_regularize_goal thm rty rel lthy =
Logic.mk_implies
((prop_of thm),
- (regularise (prop_of thm) rty rel lthy))
+ (my_reg lthy rel rty (prop_of thm)))
*}
ML {*