src/HOL/Set.thy
changeset 35115 446c5063e4fd
parent 34999 5312d2ffee3b
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Set.thy	Thu Feb 11 22:55:16 2010 +0100
     1.2 +++ b/src/HOL/Set.thy	Thu Feb 11 23:00:22 2010 +0100
     1.3 @@ -48,20 +48,16 @@
     1.4  text {* Set comprehensions *}
     1.5  
     1.6  syntax
     1.7 -  "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")
     1.8 -
     1.9 +  "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")
    1.10  translations
    1.11 -  "{x. P}"      == "Collect (%x. P)"
    1.12 +  "{x. P}" == "CONST Collect (%x. P)"
    1.13  
    1.14  syntax
    1.15 -  "@SetCompr"   :: "'a => idts => bool => 'a set"         ("(1{_ |/_./ _})")
    1.16 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ :/ _./ _})")
    1.17 -
    1.18 +  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
    1.19  syntax (xsymbols)
    1.20 -  "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
    1.21 -
    1.22 +  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
    1.23  translations
    1.24 -  "{x:A. P}"    => "{x. x:A & P}"
    1.25 +  "{x:A. P}" => "{x. x:A & P}"
    1.26  
    1.27  lemma mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
    1.28    by (simp add: Collect_def mem_def)
    1.29 @@ -107,11 +103,10 @@
    1.30    insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
    1.31  
    1.32  syntax
    1.33 -  "@Finset"     :: "args => 'a set"                       ("{(_)}")
    1.34 -
    1.35 +  "_Finset" :: "args => 'a set"    ("{(_)}")
    1.36  translations
    1.37 -  "{x, xs}"     == "CONST insert x {xs}"
    1.38 -  "{x}"         == "CONST insert x {}"
    1.39 +  "{x, xs}" == "CONST insert x {xs}"
    1.40 +  "{x}" == "CONST insert x {}"
    1.41  
    1.42  
    1.43  subsection {* Subsets and bounded quantifiers *}
    1.44 @@ -191,9 +186,9 @@
    1.45    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
    1.46  
    1.47  translations
    1.48 -  "ALL x:A. P"  == "Ball A (%x. P)"
    1.49 -  "EX x:A. P"   == "Bex A (%x. P)"
    1.50 -  "EX! x:A. P"  => "EX! x. x:A & P"
    1.51 +  "ALL x:A. P" == "CONST Ball A (%x. P)"
    1.52 +  "EX x:A. P" == "CONST Bex A (%x. P)"
    1.53 +  "EX! x:A. P" => "EX! x. x:A & P"
    1.54    "LEAST x:A. P" => "LEAST x. x:A & P"
    1.55  
    1.56  syntax (output)
    1.57 @@ -233,31 +228,34 @@
    1.58  
    1.59  print_translation {*
    1.60  let
    1.61 -  val Type (set_type, _) = @{typ "'a set"};
    1.62 -  val All_binder = Syntax.binder_name @{const_syntax "All"};
    1.63 -  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
    1.64 +  val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
    1.65 +  val All_binder = Syntax.binder_name @{const_syntax All};
    1.66 +  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
    1.67    val impl = @{const_syntax "op -->"};
    1.68    val conj = @{const_syntax "op &"};
    1.69 -  val sbset = @{const_syntax "subset"};
    1.70 -  val sbset_eq = @{const_syntax "subset_eq"};
    1.71 +  val sbset = @{const_syntax subset};
    1.72 +  val sbset_eq = @{const_syntax subset_eq};
    1.73  
    1.74    val trans =
    1.75 -   [((All_binder, impl, sbset), "_setlessAll"),
    1.76 -    ((All_binder, impl, sbset_eq), "_setleAll"),
    1.77 -    ((Ex_binder, conj, sbset), "_setlessEx"),
    1.78 -    ((Ex_binder, conj, sbset_eq), "_setleEx")];
    1.79 +   [((All_binder, impl, sbset), @{syntax_const "_setlessAll"}),
    1.80 +    ((All_binder, impl, sbset_eq), @{syntax_const "_setleAll"}),
    1.81 +    ((Ex_binder, conj, sbset), @{syntax_const "_setlessEx"}),
    1.82 +    ((Ex_binder, conj, sbset_eq), @{syntax_const "_setleEx"})];
    1.83  
    1.84    fun mk v v' c n P =
    1.85      if v = v' andalso not (Term.exists_subterm (fn Free (x, _) => x = v | _ => false) n)
    1.86      then Syntax.const c $ Syntax.mark_bound v' $ n $ P else raise Match;
    1.87  
    1.88    fun tr' q = (q,
    1.89 -    fn [Const ("_bound", _) $ Free (v, Type (T, _)), Const (c, _) $ (Const (d, _) $ (Const ("_bound", _) $ Free (v', _)) $ n) $ P] =>
    1.90 -         if T = (set_type) then case AList.lookup (op =) trans (q, c, d)
    1.91 -          of NONE => raise Match
    1.92 -           | SOME l => mk v v' l n P
    1.93 -         else raise Match
    1.94 -     | _ => raise Match);
    1.95 +        fn [Const (@{syntax_const "_bound"}, _) $ Free (v, Type (T, _)),
    1.96 +            Const (c, _) $
    1.97 +              (Const (d, _) $ (Const (@{syntax_const "_bound"}, _) $ Free (v', _)) $ n) $ P] =>
    1.98 +            if T = set_type then
    1.99 +              (case AList.lookup (op =) trans (q, c, d) of
   1.100 +                NONE => raise Match
   1.101 +              | SOME l => mk v v' l n P)
   1.102 +            else raise Match
   1.103 +         | _ => raise Match);
   1.104  in
   1.105    [tr' All_binder, tr' Ex_binder]
   1.106  end
   1.107 @@ -270,55 +268,63 @@
   1.108    only translated if @{text "[0..n] subset bvs(e)"}.
   1.109  *}
   1.110  
   1.111 +syntax
   1.112 +  "_Setcompr" :: "'a => idts => bool => 'a set"    ("(1{_ |/_./ _})")
   1.113 +
   1.114  parse_translation {*
   1.115    let
   1.116 -    val ex_tr = snd (mk_binder_tr ("EX ", "Ex"));
   1.117 +    val ex_tr = snd (mk_binder_tr ("EX ", @{const_syntax Ex}));
   1.118  
   1.119 -    fun nvars (Const ("_idts", _) $ _ $ idts) = nvars idts + 1
   1.120 +    fun nvars (Const (@{syntax_const "_idts"}, _) $ _ $ idts) = nvars idts + 1
   1.121        | nvars _ = 1;
   1.122  
   1.123      fun setcompr_tr [e, idts, b] =
   1.124        let
   1.125 -        val eq = Syntax.const "op =" $ Bound (nvars idts) $ e;
   1.126 -        val P = Syntax.const "op &" $ eq $ b;
   1.127 +        val eq = Syntax.const @{const_syntax "op ="} $ Bound (nvars idts) $ e;
   1.128 +        val P = Syntax.const @{const_syntax "op &"} $ eq $ b;
   1.129          val exP = ex_tr [idts, P];
   1.130 -      in Syntax.const "Collect" $ Term.absdummy (dummyT, exP) end;
   1.131 +      in Syntax.const @{const_syntax Collect} $ Term.absdummy (dummyT, exP) end;
   1.132  
   1.133 -  in [("@SetCompr", setcompr_tr)] end;
   1.134 +  in [(@{syntax_const "_Setcompr"}, setcompr_tr)] end;
   1.135  *}
   1.136  
   1.137 -print_translation {* [
   1.138 -Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball",
   1.139 -Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex"
   1.140 -] *} -- {* to avoid eta-contraction of body *}
   1.141 +print_translation {*
   1.142 + [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"},
   1.143 +  Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}]
   1.144 +*} -- {* to avoid eta-contraction of body *}
   1.145  
   1.146  print_translation {*
   1.147  let
   1.148 -  val ex_tr' = snd (mk_binder_tr' ("Ex", "DUMMY"));
   1.149 +  val ex_tr' = snd (mk_binder_tr' (@{const_syntax Ex}, "DUMMY"));
   1.150  
   1.151    fun setcompr_tr' [Abs (abs as (_, _, P))] =
   1.152      let
   1.153 -      fun check (Const ("Ex", _) $ Abs (_, _, P), n) = check (P, n + 1)
   1.154 -        | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
   1.155 +      fun check (Const (@{const_syntax Ex}, _) $ Abs (_, _, P), n) = check (P, n + 1)
   1.156 +        | check (Const (@{const_syntax "op &"}, _) $
   1.157 +              (Const (@{const_syntax "op ="}, _) $ Bound m $ e) $ P, n) =
   1.158              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
   1.159              subset (op =) (0 upto (n - 1), add_loose_bnos (e, 0, []))
   1.160 -        | check _ = false
   1.161 +        | check _ = false;
   1.162  
   1.163          fun tr' (_ $ abs) =
   1.164            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]
   1.165 -          in Syntax.const "@SetCompr" $ e $ idts $ Q end;
   1.166 -    in if check (P, 0) then tr' P
   1.167 -       else let val (x as _ $ Free(xN,_), t) = atomic_abs_tr' abs
   1.168 -                val M = Syntax.const "@Coll" $ x $ t
   1.169 -            in case t of
   1.170 -                 Const("op &",_)
   1.171 -                   $ (Const("op :",_) $ (Const("_bound",_) $ Free(yN,_)) $ A)
   1.172 -                   $ P =>
   1.173 -                   if xN=yN then Syntax.const "@Collect" $ x $ A $ P else M
   1.174 -               | _ => M
   1.175 -            end
   1.176 +          in Syntax.const @{syntax_const "_Setcompr"} $ e $ idts $ Q end;
   1.177 +    in
   1.178 +      if check (P, 0) then tr' P
   1.179 +      else
   1.180 +        let
   1.181 +          val (x as _ $ Free(xN, _), t) = atomic_abs_tr' abs;
   1.182 +          val M = Syntax.const @{syntax_const "_Coll"} $ x $ t;
   1.183 +        in
   1.184 +          case t of
   1.185 +            Const (@{const_syntax "op &"}, _) $
   1.186 +              (Const (@{const_syntax "op :"}, _) $
   1.187 +                (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
   1.188 +            if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
   1.189 +          | _ => M
   1.190 +        end
   1.191      end;
   1.192 -  in [("Collect", setcompr_tr')] end;
   1.193 +  in [(@{const_syntax Collect}, setcompr_tr')] end;
   1.194  *}
   1.195  
   1.196  setup {*