# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1263567085 -3600
# Node ID 7bac7dffadebfedc555f0d741f64c97826df65af
# Parent  0f920b62fb7b27d28f64b298c20860f1700c9436
hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.

diff -r 0f920b62fb7b -r 7bac7dffadeb Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Fri Jan 15 12:17:30 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Jan 15 15:51: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
+
diff -r 0f920b62fb7b -r 7bac7dffadeb Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Fri Jan 15 12:17:30 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 15 15:51: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)
diff -r 0f920b62fb7b -r 7bac7dffadeb Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Fri Jan 15 12:17:30 2010 +0100
+++ b/Quot/quotient_term.ML	Fri Jan 15 15:51: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