--- a/Quot/Examples/LamEx.thy Fri Jan 15 15:56:06 2010 +0100
+++ b/Quot/Examples/LamEx.thy Fri Jan 15 15:56:25 2010 +0100
@@ -360,26 +360,49 @@
apply(simp add: var_supp1)
done
+(* lemma hom_reg: *)
lemma hom: "
-\<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =).
-\<forall>f_app \<in> Respects(alpha ===> alpha ===> op =).
- \<exists>hom \<in> Respects(alpha ===> op =). (
+ \<exists>hom\<in>Respects (alpha ===> op =). (
(\<forall>x. hom (rVar x) = f_var x) \<and>
(\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
(\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
)"
sorry
+lemma hom_reg:"
+(\<exists>hom\<in>Respects (alpha ===> op =).
+ (\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa)))) \<longrightarrow>
+(\<exists>hom.
+ (\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))"
+by(regularize)
+
+thm impE[OF hom_reg]
+lemma hom_pre:"
+(\<exists>hom.
+ (\<forall>x. hom (rVar x) = f_var x) \<and>
+ (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and>
+ (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))"
+apply (rule impE[OF hom_reg])
+apply (rule hom)
+apply (assumption)
+done
+
lemma hom':
-"\<forall>f_lam. \<forall>f_app. \<exists>hom. (
+"\<exists>hom. (
(\<forall>x. hom (Var x) = f_var x) \<and>
(\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and>
(\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x)))
)"
-(*apply (lifting hom)*)
-sorry
+apply (lifting hom)
+done
-thm rlam.recs
+thm bex_reg_eqv_range[OF identity_equivp, of "alpha"]
+
end
+
--- a/Quot/QuotScript.thy Fri Jan 15 15:56:06 2010 +0100
+++ b/Quot/QuotScript.thy Fri Jan 15 15:56:25 2010 +0100
@@ -301,8 +301,6 @@
done
lemma bex_reg_eqv_range:
- fixes P::"'a \<Rightarrow> bool"
- and x::"'a"
assumes a: "equivp R2"
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
apply(auto)
--- a/Quot/quotient_term.ML Fri Jan 15 15:56:06 2010 +0100
+++ b/Quot/quotient_term.ML Fri Jan 15 15:56:25 2010 +0100
@@ -378,15 +378,14 @@
(Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
| _ => f (trm1, trm2)
-fun relation_error ctxt r1 r2 =
+fun term_mismatch str ctxt t1 t2 =
let
- val r1_str = Syntax.string_of_term ctxt r1
- val r2_str = Syntax.string_of_term ctxt r2
- val r1_ty_str = Syntax.string_of_typ ctxt (fastype_of r1)
- val r2_ty_str = Syntax.string_of_typ ctxt (fastype_of r2)
+ val t1_str = Syntax.string_of_term ctxt t1
+ val t2_str = Syntax.string_of_term ctxt t2
+ val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
+ val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
in
- raise LIFT_MATCH
- (cat_lines ["regularise (relation mismatch)", r1_str ^ "::" ^ r1_ty_str, r2_str ^ "::" ^ r2_ty_str])
+ raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
end
(* the major type of All and Ex quantifiers *)
@@ -433,6 +432,15 @@
else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
+ | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ in
+ if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+ then term_mismatch "regularize(ball)" ctxt rtrm qtrm
+ else mk_ball $ (mk_resp $ resrel) $ subtrm
+ end
+
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -441,6 +449,15 @@
else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
+ | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+ in
+ if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+ then term_mismatch "regularize(bex)" ctxt rtrm qtrm
+ else mk_bex $ (mk_resp $ resrel) $ subtrm
+ end
+
| (* equalities need to be replaced by appropriate equivalence relations *)
(Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
if ty = ty' then rtrm
@@ -452,7 +469,7 @@
val rel_ty = fastype_of rel
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
in
- if rel' aconv rel then rtrm else relation_error ctxt rel rel'
+ if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
end
| (_, Const _) =>
@@ -464,13 +481,11 @@
if same_const rtrm qtrm then rtrm
else
let
- val qtrm_str = Syntax.string_of_term ctxt qtrm
- val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
- val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
- val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1
- in
- if Pattern.matches thy (rtrm', rtrm)
- then rtrm else raise exc2
+ val rtrm' = #rconst (qconsts_lookup thy qtrm)
+ handle NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
+ in
+ if Pattern.matches thy (rtrm', rtrm)
+ then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
end
end