"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
authorhaftmann
Thu Jul 01 16:54:42 2010 +0200 (2010-07-01)
changeset 37676f433cb9caea4
parent 37670 0ce594837524
child 37677 c5a8b612e571
"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
src/HOL/Tools/hologic.ML
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Jul 01 14:32:57 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -167,15 +167,15 @@
     1.4    | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
     1.5    | dest_set t = raise TERM ("dest_set", [t]);
     1.6  
     1.7 -fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
     1.8 +fun Collect_const T = Const ("Set.Collect", (T --> boolT) --> mk_setT T);
     1.9  fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    1.10  
    1.11  fun mk_mem (x, A) =
    1.12    let val setT = fastype_of A in
    1.13 -    Const ("op :", dest_setT setT --> setT --> boolT) $ x $ A
    1.14 +    Const ("Set.member", dest_setT setT --> setT --> boolT) $ x $ A
    1.15    end;
    1.16  
    1.17 -fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
    1.18 +fun dest_mem (Const ("Set.member", _) $ x $ A) = (x, A)
    1.19    | dest_mem t = raise TERM ("dest_mem", [t]);
    1.20  
    1.21  
    1.22 @@ -289,9 +289,9 @@
    1.23  
    1.24  (* prod *)
    1.25  
    1.26 -fun mk_prodT (T1, T2) = Type ("Product_Type.*", [T1, T2]);
    1.27 +fun mk_prodT (T1, T2) = Type ("Product_Type.prod", [T1, T2]);
    1.28  
    1.29 -fun dest_prodT (Type ("Product_Type.*", [T1, T2])) = (T1, T2)
    1.30 +fun dest_prodT (Type ("Product_Type.prod", [T1, T2])) = (T1, T2)
    1.31    | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
    1.32  
    1.33  fun pair_const T1 T2 = Const ("Product_Type.Pair", [T1, T2] ---> mk_prodT (T1, T2));
    1.34 @@ -324,7 +324,7 @@
    1.35    | _ => raise TERM ("mk_split: bad body type", [t]));
    1.36  
    1.37  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
    1.38 -fun flatten_tupleT (Type ("Product_Type.*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    1.39 +fun flatten_tupleT (Type ("Product_Type.prod", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    1.40    | flatten_tupleT T = [T];
    1.41  
    1.42  
    1.43 @@ -334,7 +334,7 @@
    1.44    | mk_tupleT Ts = foldr1 mk_prodT Ts;
    1.45  
    1.46  fun strip_tupleT (Type ("Product_Type.unit", [])) = []
    1.47 -  | strip_tupleT (Type ("Product_Type.*", [T1, T2])) = T1 :: strip_tupleT T2
    1.48 +  | strip_tupleT (Type ("Product_Type.prod", [T1, T2])) = T1 :: strip_tupleT T2
    1.49    | strip_tupleT T = [T];
    1.50  
    1.51  fun mk_tuple [] = unit
    1.52 @@ -367,14 +367,14 @@
    1.53  fun strip_ptupleT ps =
    1.54    let
    1.55      fun factors p T = if member (op =) ps p then (case T of
    1.56 -        Type ("Product_Type.*", [T1, T2]) =>
    1.57 +        Type ("Product_Type.prod", [T1, T2]) =>
    1.58            factors (1::p) T1 @ factors (2::p) T2
    1.59        | _ => ptuple_err "strip_ptupleT") else [T]
    1.60    in factors [] end;
    1.61  
    1.62  val flat_tupleT_paths =
    1.63    let
    1.64 -    fun factors p (Type ("Product_Type.*", [T1, T2])) =
    1.65 +    fun factors p (Type ("Product_Type.prod", [T1, T2])) =
    1.66            p :: factors (1::p) T1 @ factors (2::p) T2
    1.67        | factors p _ = []
    1.68    in factors [] end;
    1.69 @@ -383,7 +383,7 @@
    1.70    let
    1.71      fun mk p T ts =
    1.72        if member (op =) ps p then (case T of
    1.73 -          Type ("Product_Type.*", [T1, T2]) =>
    1.74 +          Type ("Product_Type.prod", [T1, T2]) =>
    1.75              let
    1.76                val (t, ts') = mk (1::p) T1 ts;
    1.77                val (u, ts'') = mk (2::p) T2 ts'
    1.78 @@ -414,7 +414,7 @@
    1.79    let
    1.80      fun ap ((p, T) :: pTs) =
    1.81            if member (op =) ps p then (case T of
    1.82 -              Type ("Product_Type.*", [T1, T2]) =>
    1.83 +              Type ("Product_Type.prod", [T1, T2]) =>
    1.84                  split_const (T1, T2, map snd pTs ---> T3) $
    1.85                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
    1.86              | _ => ptuple_err "mk_psplits")