# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260184465 -3600
# Node ID a2f2214dc88120775c88f5a1ad99f456da5020eb
# Parent  6346745532f4a0a9c1b8b699ab089e7f754b295b
Fix of regularize for babs and proof of babs_rsp.

diff -r 6346745532f4 -r a2f2214dc881 QuotMain.thy
--- a/QuotMain.thy	Mon Dec 07 11:14:21 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 12:14:25 2009 +0100
@@ -172,13 +172,6 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
-section {* Bounded abstraction *}
-
-definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-
 section {* Simset setup *}
 
 (* since HOL_basic_ss is too "big", we need to set up *)
@@ -418,10 +411,10 @@
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (x', ty', t')) =>
        let
-         val subtrm = regularize_trm lthy t t'
-       in     
+         val subtrm = Abs(x, ty, regularize_trm lthy t t')
+       in
          if ty = ty'
-         then Abs (x, ty, subtrm)
+         then subtrm
          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
        end
 
diff -r 6346745532f4 -r a2f2214dc881 QuotScript.thy
--- a/QuotScript.thy	Mon Dec 07 11:14:21 2009 +0100
+++ b/QuotScript.thy	Mon Dec 07 12:14:25 2009 +0100
@@ -310,7 +310,13 @@
   "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
 by auto
 
-(* 2 lemmas needed for proving repabs_inj *)
+(* Bounded abstraction *)
+definition
+  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+
+(* 3 lemmas needed for proving repabs_inj *)
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
   shows "Ball (Respects R) f = Ball (Respects R) g"
@@ -321,6 +327,17 @@
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
   using a by (simp add: Bex_def in_respects)
 
+lemma babs_rsp:
+  assumes q: "Quotient R1 Abs1 Rep1"
+  and     a: "(R1 ===> R2) f g"
+  shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
+  apply (auto simp add: Babs_def)
+  apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+  using a apply (simp add: Babs_def)
+  apply (simp add: in_respects)
+  using Quotient_rel[OF q]
+  by metis
+
 (* 2 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"