src/HOL/Tools/hologic.ML
changeset 30450 7655e6533209
parent 30304 d8e4cd2ac2a1
child 30453 1e7e0d171653
     1.1 --- a/src/HOL/Tools/hologic.ML	Wed Mar 11 15:56:50 2009 +0100
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed Mar 11 15:56:51 2009 +0100
     1.3 @@ -11,13 +11,20 @@
     1.4    val typeT: typ
     1.5    val boolN: string
     1.6    val boolT: typ
     1.7 +  val Trueprop: term
     1.8 +  val mk_Trueprop: term -> term
     1.9 +  val dest_Trueprop: term -> term
    1.10    val true_const: term
    1.11    val false_const: term
    1.12    val mk_setT: typ -> typ
    1.13    val dest_setT: typ -> typ
    1.14 -  val Trueprop: term
    1.15 -  val mk_Trueprop: term -> term
    1.16 -  val dest_Trueprop: term -> term
    1.17 +  val Collect_const: typ -> term
    1.18 +  val mk_Collect: string * typ * term -> term
    1.19 +  val mk_mem: term * term -> term
    1.20 +  val dest_mem: term -> term * term
    1.21 +  val mk_set: typ -> term list -> term
    1.22 +  val dest_set: term -> term list
    1.23 +  val mk_UNIV: typ -> term
    1.24    val conj_intr: thm -> thm -> thm
    1.25    val conj_elim: thm -> thm * thm
    1.26    val conj_elims: thm -> thm list
    1.27 @@ -43,12 +50,7 @@
    1.28    val exists_const: typ -> term
    1.29    val mk_exists: string * typ * term -> term
    1.30    val choice_const: typ -> term
    1.31 -  val Collect_const: typ -> term
    1.32 -  val mk_Collect: string * typ * term -> term
    1.33    val class_eq: string
    1.34 -  val mk_mem: term * term -> term
    1.35 -  val dest_mem: term -> term * term
    1.36 -  val mk_UNIV: typ -> term
    1.37    val mk_binop: string -> term * term -> term
    1.38    val mk_binrel: string -> term * term -> term
    1.39    val dest_bin: string -> typ -> term -> term * term
    1.40 @@ -139,6 +141,30 @@
    1.41  fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
    1.42    | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
    1.43  
    1.44 +fun mk_set T ts =
    1.45 +  let
    1.46 +    val sT = mk_setT T;
    1.47 +    val empty = Const ("Orderings.bot", sT);
    1.48 +    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
    1.49 +  in fold_rev insert ts empty end;
    1.50 +
    1.51 +fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    1.52 +
    1.53 +fun dest_set (Const ("Orderings.bot", _)) = []
    1.54 +  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
    1.55 +  | dest_set t = raise TERM ("dest_set", [t]);
    1.56 +
    1.57 +fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
    1.58 +fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    1.59 +
    1.60 +fun mk_mem (x, A) =
    1.61 +  let val setT = fastype_of A in
    1.62 +    Const ("op :", dest_setT setT --> setT --> boolT) $ x $ A
    1.63 +  end;
    1.64 +
    1.65 +fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
    1.66 +  | dest_mem t = raise TERM ("dest_mem", [t]);
    1.67 +
    1.68  
    1.69  (* logic *)
    1.70  
    1.71 @@ -212,21 +238,8 @@
    1.72  
    1.73  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
    1.74  
    1.75 -fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
    1.76 -fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    1.77 -
    1.78  val class_eq = "HOL.eq";
    1.79  
    1.80 -fun mk_mem (x, A) =
    1.81 -  let val setT = fastype_of A in
    1.82 -    Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
    1.83 -  end;
    1.84 -
    1.85 -fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
    1.86 -  | dest_mem t = raise TERM ("dest_mem", [t]);
    1.87 -
    1.88 -fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    1.89 -
    1.90  
    1.91  (* binary operations and relations *)
    1.92