# HG changeset patch
# User nipkow
# Date 1085576226 -7200
# Node ID 8de39d3e8eb6cd8b534ea4a7e6c77090f331b918
# Parent  f7557773cc87b84e422bf95aeb14a6faf564c84a
Corrected printer bug for bounded quantifiers Q x<=y. P

diff -r f7557773cc87 -r 8de39d3e8eb6 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed May 26 11:43:50 2004 +0200
+++ b/src/HOL/Set.thy	Wed May 26 14:57:06 2004 +0200
@@ -138,7 +138,6 @@
   "op \<subseteq>" => "op <= :: _ set => _ set => bool"
   "op \<subset>" => "op <  :: _ set => _ set => bool"
 
-
 typed_print_translation {*
   let
     fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
@@ -151,6 +150,73 @@
   in [("op <=", le_tr'), ("op <", less_tr')] end
 *}
 
+
+subsubsection "Bounded quantifiers"
+
+syntax
+  "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
+
+syntax (xsymbols)
+  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+
+syntax (HOL)
+  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
+
+syntax (HTML output)
+  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+
+translations
+ "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
+ "\<exists>A\<subset>B. P"    =>  "EX A. A \<subset> B & P"
+ "\<forall>A\<subseteq>B. P"  =>  "ALL A. A \<subseteq> B --> P"
+ "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
+
+print_translation {*
+let
+  fun
+    all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
+             Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  (if v=v' andalso T="set"
+   then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
+   else raise Match)
+
+  | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
+             Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  (if v=v' andalso T="set"
+   then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
+   else raise Match);
+
+  fun
+    ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
+            Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  (if v=v' andalso T="set"
+   then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
+   else raise Match)
+
+  | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
+            Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+  (if v=v' andalso T="set"
+   then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
+   else raise Match)
+in
+[("ALL ", all_tr'), ("EX ", ex_tr')]
+end
+*}
+
+
+
 text {*
   \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
   "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is