1.1 --- a/src/HOL/Set.thy	Wed May 26 11:43:50 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed May 26 14:57:06 2004 +0200
     1.3 @@ -138,7 +138,6 @@
     1.4    "op \<subseteq>" => "op <= :: _ set => _ set => bool"
     1.5    "op \<subset>" => "op <  :: _ set => _ set => bool"
     1.6  
     1.7 -
     1.8  typed_print_translation {*
     1.9    let
    1.10      fun le_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
    1.11 @@ -151,6 +150,73 @@
    1.12    in [("op <=", le_tr'), ("op <", less_tr')] end
    1.13  *}
    1.14  
    1.15 +
    1.16 +subsubsection "Bounded quantifiers"
    1.17 +
    1.18 +syntax
    1.19 +  "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
    1.20 +  "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
    1.21 +  "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
    1.22 +  "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
    1.23 +
    1.24 +syntax (xsymbols)
    1.25 +  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
    1.26 +  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
    1.27 +  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
    1.28 +  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
    1.29 +
    1.30 +syntax (HOL)
    1.31 +  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
    1.32 +  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
    1.33 +  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
    1.34 +  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
    1.35 +
    1.36 +syntax (HTML output)
    1.37 +  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
    1.38 +  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
    1.39 +  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
    1.40 +  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
    1.41 +
    1.42 +translations
    1.43 + "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
    1.44 + "\<exists>A\<subset>B. P"    =>  "EX A. A \<subset> B & P"
    1.45 + "\<forall>A\<subseteq>B. P"  =>  "ALL A. A \<subseteq> B --> P"
    1.46 + "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
    1.47 +
    1.48 +print_translation {*
    1.49 +let
    1.50 +  fun
    1.51 +    all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
    1.52 +             Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.53 +  (if v=v' andalso T="set"
    1.54 +   then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
    1.55 +   else raise Match)
    1.56 +
    1.57 +  | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
    1.58 +             Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.59 +  (if v=v' andalso T="set"
    1.60 +   then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
    1.61 +   else raise Match);
    1.62 +
    1.63 +  fun
    1.64 +    ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
    1.65 +            Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.66 +  (if v=v' andalso T="set"
    1.67 +   then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
    1.68 +   else raise Match)
    1.69 +
    1.70 +  | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
    1.71 +            Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
    1.72 +  (if v=v' andalso T="set"
    1.73 +   then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
    1.74 +   else raise Match)
    1.75 +in
    1.76 +[("ALL ", all_tr'), ("EX ", ex_tr')]
    1.77 +end
    1.78 +*}
    1.79 +
    1.80 +
    1.81 +
    1.82  text {*
    1.83    \medskip Translate between @{text "{e | x1...xn. P}"} and @{text
    1.84    "{u. EX x1..xn. u = e & P}"}; @{text "{y. EX x1..xn. y = e & P}"} is