# HG changeset patch # User Cezary Kaliszyk # 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 \ bool) \ ('a \ 'b) \ 'a \ 'b" -where - "(x \ p) \ (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 @@ "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" by auto -(* 2 lemmas needed for proving repabs_inj *) +(* Bounded abstraction *) +definition + Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" +where + "(x \ p) \ (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 \ Respects R1 \ y \ 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"