# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264064105 -3600
# Node ID 1bf4337919d36ea706787063d786822f7f8b8c67
# Parent  e576a97e9a3e225aab62ae3fb25dd23308068d26
Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.

diff -r e576a97e9a3e -r 1bf4337919d3 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 21 09:02:04 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 09:55:05 2010 +0100
@@ -186,6 +186,15 @@
   using a b c
   by (lifting int_induct_raw)
 
+lemma ex1tst: "\<exists>! (x :: nat \<times> nat) \<in> Respects (op \<approx>). True"
+sorry
+
+lemma ex1tst': "\<exists>! (x :: my_int). True"
+apply(lifting ex1tst)
+apply(cleaning)
+apply simp
+sorry
+
 lemma ho_tst: "foldl my_plus x [] = x"
 apply simp
 done
diff -r e576a97e9a3e -r 1bf4337919d3 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Thu Jan 21 09:02:04 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Thu Jan 21 09:55:05 2010 +0100
@@ -141,6 +141,7 @@
 )"
 apply (lifting tolift)
 apply (regularize)
+apply (simp)
 prefer 2
 apply cleaning
 apply simp
diff -r e576a97e9a3e -r 1bf4337919d3 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Jan 21 09:02:04 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 09:55:05 2010 +0100
@@ -350,6 +350,11 @@
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
+definition
+  Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+  "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+
 (* 3 lemmas needed for proving repabs_inj *)
 lemma ball_rsp:
   assumes a: "(R ===> (op =)) f g"
@@ -361,6 +366,12 @@
   shows "(Bex (Respects R) f = Bex (Respects R) g)"
   using a by (simp add: Bex_def in_respects)
 
+lemma bex1_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)"
+  using a 
+by (simp add: Ex1_def Bex1_def in_respects) auto
+
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
@@ -415,6 +426,42 @@
   using a unfolding Quotient_def
   by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply)
 
+lemma ex1_prs:
+  assumes a: "Quotient R absf repf"
+  shows "Bexeq R ((absf ---> id) f) = Ex1 f"
+apply (subst Bexeq_def)
+apply (subst Bex_def)
+apply (subst Ex1_def)
+apply simp
+apply rule
+ apply (erule conjE)+
+ apply (erule_tac exE)
+ apply (erule conjE)
+ apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
+  apply (rule_tac x="absf x" in exI)
+  apply (thin_tac "\<forall>x\<in>Respects R. \<forall>y\<in>Respects R. f (absf x) \<and> f (absf y) \<longrightarrow> R x y")
+  apply (simp)
+  apply rule+
+  using a unfolding Quotient_def
+  apply metis
+ apply rule+
+ apply (erule_tac x="x" in ballE)
+  apply (erule_tac x="y" in ballE)
+   apply simp
+  apply (simp add: in_respects)
+ apply (simp add: in_respects)
+apply (erule_tac exE)
+ apply rule
+ apply (rule_tac x="repf x" in exI)
+ apply (simp only: in_respects)
+  apply rule
+ apply (metis Quotient_rel_rep[OF a])
+using a unfolding Quotient_def apply (simp)
+apply rule+
+using a unfolding Quotient_def in_respects
+apply metis
+done
+
 lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   shows "(R1 ===> R2) f g"
diff -r e576a97e9a3e -r 1bf4337919d3 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 21 09:02:04 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 21 09:55:05 2010 +0100
@@ -323,17 +323,6 @@
   (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
-| Const (@{const_name "op ="},_) $
-    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1}
-
-(* TODO: Check why less _ are needed then in EX/ALL cases *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $
-    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _))
-      rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
-
     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
 | (Const (@{const_name "op ="},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
@@ -358,6 +347,17 @@
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
+| Const (@{const_name "op ="},_) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1}
+
+(* TODO: Check why less _ are needed then in EX/ALL cases *)
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _))
+      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
 | (_ $
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))