# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264067709 -3600
# Node ID 3e7a6ec549d1646d3d7a6071985605c8530766eb
# Parent  1bf4337919d36ea706787063d786822f7f8b8c67
Using Bexeq_rsp, and manually lifted lemma with Ex1.

diff -r 1bf4337919d3 -r 3e7a6ec549d1 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 10:55:09 2010 +0100
@@ -186,14 +186,19 @@
   using a b c
   by (lifting int_induct_raw)
 
-lemma ex1tst: "\<exists>! (x :: nat \<times> nat) \<in> Respects (op \<approx>). True"
+lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)"
 sorry
 
-lemma ex1tst': "\<exists>! (x :: my_int). True"
+lemma ex1tst': "\<exists>! (x :: my_int). x = x"
 apply(lifting ex1tst)
+
+apply injection
+apply (rule quot_respect(9))
+apply (rule Quotient_my_int)
+
 apply(cleaning)
-apply simp
-sorry
+apply (simp add: ex1_prs[OF Quotient_my_int])
+done
 
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
diff -r 1bf4337919d3 -r 3e7a6ec549d1 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/QuotMain.thy	Thu Jan 21 10:55:09 2010 +0100
@@ -100,8 +100,8 @@
 
 declare [[map "fun" = (fun_map, fun_rel)]]
 
-lemmas [quot_thm] = fun_quotient 
-lemmas [quot_respect] = quot_rel_rsp
+lemmas [quot_thm] = fun_quotient
+lemmas [quot_respect] = quot_rel_rsp bexeq_rsp
 lemmas [quot_equiv] = identity_equivp
 
 (* Lemmas about simplifying id's. *)
diff -r 1bf4337919d3 -r 3e7a6ec549d1 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 10:55:09 2010 +0100
@@ -372,6 +372,46 @@
   using a 
 by (simp add: Ex1_def Bex1_def in_respects) auto
 
+(* TODO/FIXME: simplify the repetitions in this proof *)
+lemma bexeq_rsp:
+assumes a: "Quotient R absf repf"
+shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)"
+apply simp
+unfolding Bexeq_def
+apply rule
+apply rule
+apply rule
+apply rule
+apply (erule conjE)+
+apply (erule bexE)
+apply rule
+apply (rule_tac x="xa" in bexI)
+apply metis
+apply metis
+apply rule+
+apply (erule_tac x="xb" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (erule_tac x="ya" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (metis in_respects)
+apply (erule conjE)+
+apply (erule bexE)
+apply rule
+apply (rule_tac x="xa" in bexI)
+apply metis
+apply metis
+apply rule+
+apply (erule_tac x="xb" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (erule_tac x="ya" in ballE)
+prefer 2
+apply (metis in_respects)
+apply (metis in_respects)
+done
+
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
diff -r 1bf4337919d3 -r 3e7a6ec549d1 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Jan 21 09:55:05 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 21 10:55:09 2010 +0100
@@ -367,6 +367,7 @@
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
 val mk_bex1 = Const (@{const_name Bex1}, dummyT)
+val mk_bexeq = Const (@{const_name Bexeq}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 
 (* - applies f to the subterm of an abstraction, 
@@ -466,17 +467,17 @@
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
        in
          if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
-         else mk_bex1 $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+         else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
          val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
        in
          if resrel <> needrel
          then term_mismatch "regularize(bex1)" ctxt resrel needrel
-         else mk_bex1 $ (mk_resp $ resrel) $ subtrm
+         else mk_bexeq $ resrel $ subtrm
        end
 
   | (* equalities need to be replaced by appropriate equivalence relations *)