src/HOL/hologic.ML
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24630 351a308ab58d
child 24958 ff15f76741bd
permissions -rw-r--r--
moved Finite_Set before Datatype
     1 (*  Title:      HOL/hologic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 
     5 Abstract syntax operations for HOL.
     6 *)
     7 
     8 signature HOLOGIC =
     9 sig
    10   val typeS: sort
    11   val typeT: typ
    12   val boolN: string
    13   val boolT: typ
    14   val true_const: term
    15   val false_const: term
    16   val mk_setT: typ -> typ
    17   val dest_setT: typ -> typ
    18   val Trueprop: term
    19   val mk_Trueprop: term -> term
    20   val dest_Trueprop: term -> term
    21   val conj_intr: thm -> thm -> thm
    22   val conj_elim: thm -> thm * thm
    23   val conj_elims: thm -> thm list
    24   val conj: term
    25   val disj: term
    26   val imp: term
    27   val Not: term
    28   val mk_conj: term * term -> term
    29   val mk_disj: term * term -> term
    30   val mk_imp: term * term -> term
    31   val mk_not: term -> term
    32   val dest_conj: term -> term list
    33   val dest_disj: term -> term list
    34   val dest_imp: term -> term * term
    35   val dest_not: term -> term
    36   val dest_concls: term -> term list
    37   val eq_const: typ -> term
    38   val mk_eq: term * term -> term
    39   val dest_eq: term -> term * term
    40   val all_const: typ -> term
    41   val mk_all: string * typ * term -> term
    42   val list_all: (string * typ) list * term -> term
    43   val exists_const: typ -> term
    44   val mk_exists: string * typ * term -> term
    45   val choice_const: typ -> term
    46   val Collect_const: typ -> term
    47   val mk_Collect: string * typ * term -> term
    48   val class_eq: string
    49   val mk_mem: term * term -> term
    50   val dest_mem: term -> term * term
    51   val mk_UNIV: typ -> term
    52   val mk_binop: string -> term * term -> term
    53   val mk_binrel: string -> term * term -> term
    54   val dest_bin: string -> typ -> term -> term * term
    55   val unitT: typ
    56   val is_unitT: typ -> bool
    57   val unit: term
    58   val is_unit: term -> bool
    59   val mk_prodT: typ * typ -> typ
    60   val dest_prodT: typ -> typ * typ
    61   val pair_const: typ -> typ -> term
    62   val mk_prod: term * term -> term
    63   val dest_prod: term -> term * term
    64   val mk_fst: term -> term
    65   val mk_snd: term -> term
    66   val split_const: typ * typ * typ -> term
    67   val mk_split: term -> term
    68   val prodT_factors: typ -> typ list
    69   val mk_tuple: typ -> term list -> term
    70   val dest_tuple: term -> term list
    71   val ap_split: typ -> typ -> term -> term
    72   val prod_factors: term -> int list list
    73   val dest_tuple': int list list -> term -> term list
    74   val prodT_factors': int list list -> typ -> typ list
    75   val ap_split': int list list -> typ -> typ -> term -> term
    76   val mk_tuple': int list list -> typ -> term list -> term
    77   val mk_tupleT: int list list -> typ list -> typ
    78   val strip_split: term -> term * typ list * int list list
    79   val natT: typ
    80   val zero: term
    81   val is_zero: term -> bool
    82   val mk_Suc: term -> term
    83   val dest_Suc: term -> term
    84   val Suc_zero: term
    85   val mk_nat: int -> term
    86   val dest_nat: term -> int
    87   val class_size: string
    88   val size_const: typ -> term
    89   val bitT: typ
    90   val B0_const: term
    91   val B1_const: term
    92   val mk_bit: int -> term
    93   val dest_bit: term -> int
    94   val intT: typ
    95   val pls_const: term
    96   val min_const: term
    97   val bit_const: term
    98   val mk_numeral: int -> term
    99   val dest_numeral: term -> int
   100   val number_of_const: typ -> term
   101   val add_numerals: term -> (term * typ) list -> (term * typ) list
   102   val mk_number: typ -> int -> term
   103   val dest_number: term -> typ * int
   104   val realT: typ
   105   val nibbleT: typ
   106   val mk_nibble: int -> term
   107   val dest_nibble: term -> int
   108   val charT: typ
   109   val mk_char: int -> term
   110   val dest_char: term -> int
   111   val listT: typ -> typ
   112   val mk_list: typ -> term list -> term
   113   val dest_list: term -> term list
   114   val stringT: typ
   115   val mk_string: string -> term
   116   val dest_string: term -> string
   117 end;
   118 
   119 structure HOLogic: HOLOGIC =
   120 struct
   121 
   122 (* HOL syntax *)
   123 
   124 val typeS: sort = ["HOL.type"];
   125 val typeT = TypeInfer.anyT typeS;
   126 
   127 
   128 (* bool and set *)
   129 
   130 val boolN = "bool";
   131 val boolT = Type (boolN, []);
   132 
   133 val true_const =  Const ("True", boolT);
   134 val false_const = Const ("False", boolT);
   135 
   136 fun mk_setT T = Type ("set", [T]);
   137 
   138 fun dest_setT (Type ("set", [T])) = T
   139   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
   140 
   141 
   142 (* logic *)
   143 
   144 val Trueprop = Const ("Trueprop", boolT --> propT);
   145 
   146 fun mk_Trueprop P = Trueprop $ P;
   147 
   148 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   149   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   150 
   151 fun conj_intr thP thQ =
   152   let
   153     val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
   154       handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
   155     val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   156   in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
   157 
   158 fun conj_elim thPQ =
   159   let
   160     val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
   161       handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
   162     val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   163     val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
   164     val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
   165   in (thP, thQ) end;
   166 
   167 fun conj_elims th =
   168   let val (th1, th2) = conj_elim th
   169   in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
   170 
   171 val conj = @{term "op &"}
   172 and disj = @{term "op |"}
   173 and imp = @{term "op -->"}
   174 and Not = @{term "Not"};
   175 
   176 fun mk_conj (t1, t2) = conj $ t1 $ t2
   177 and mk_disj (t1, t2) = disj $ t1 $ t2
   178 and mk_imp (t1, t2) = imp $ t1 $ t2
   179 and mk_not t = Not $ t;
   180 
   181 fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
   182   | dest_conj t = [t];
   183 
   184 fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
   185   | dest_disj t = [t];
   186 
   187 fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
   188   | dest_imp  t = raise TERM ("dest_imp", [t]);
   189 
   190 fun dest_not (Const ("Not", _) $ t) = t
   191   | dest_not t = raise TERM ("dest_not", [t]);
   192 
   193 fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t;
   194 val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;
   195 
   196 fun eq_const T = Const ("op =", [T, T] ---> boolT);
   197 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   198 
   199 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   200   | dest_eq t = raise TERM ("dest_eq", [t])
   201 
   202 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
   203 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
   204 fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
   205 
   206 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
   207 fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
   208 
   209 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
   210 
   211 fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
   212 fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
   213 
   214 val class_eq = "HOL.eq";
   215 
   216 fun mk_mem (x, A) =
   217   let val setT = fastype_of A in
   218     Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
   219   end;
   220 
   221 fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
   222   | dest_mem t = raise TERM ("dest_mem", [t]);
   223 
   224 fun mk_UNIV T = Const ("UNIV", mk_setT T);
   225 
   226 
   227 (* binary operations and relations *)
   228 
   229 fun mk_binop c (t, u) =
   230   let val T = fastype_of t in
   231     Const (c, [T, T] ---> T) $ t $ u
   232   end;
   233 
   234 fun mk_binrel c (t, u) =
   235   let val T = fastype_of t in
   236     Const (c, [T, T] ---> boolT) $ t $ u
   237   end;
   238 
   239 (*destruct the application of a binary operator. The dummyT case is a crude
   240   way of handling polymorphic operators.*)
   241 fun dest_bin c T (tm as Const (c', Type ("fun", [T', _])) $ t $ u) =
   242       if c = c' andalso (T=T' orelse T=dummyT) then (t, u)
   243       else raise TERM ("dest_bin " ^ c, [tm])
   244   | dest_bin c _ tm = raise TERM ("dest_bin " ^ c, [tm]);
   245 
   246 
   247 (* unit *)
   248 
   249 val unitT = Type ("Product_Type.unit", []);
   250 
   251 fun is_unitT (Type ("Product_Type.unit", [])) = true
   252   | is_unitT _ = false;
   253 
   254 val unit = Const ("Product_Type.Unity", unitT);
   255 
   256 fun is_unit (Const ("Product_Type.Unity", _)) = true
   257   | is_unit _ = false;
   258 
   259 
   260 (* prod *)
   261 
   262 fun mk_prodT (T1, T2) = Type ("*", [T1, T2]);
   263 
   264 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
   265   | dest_prodT T = raise TYPE ("dest_prodT", [T], []);
   266 
   267 fun pair_const T1 T2 = Const ("Pair", [T1, T2] ---> mk_prodT (T1, T2));
   268 
   269 fun mk_prod (t1, t2) =
   270   let val T1 = fastype_of t1 and T2 = fastype_of t2 in
   271     pair_const T1 T2 $ t1 $ t2
   272   end;
   273 
   274 fun dest_prod (Const ("Pair", _) $ t1 $ t2) = (t1, t2)
   275   | dest_prod t = raise TERM ("dest_prod", [t]);
   276 
   277 fun mk_fst p =
   278   let val pT = fastype_of p in
   279     Const ("fst", pT --> fst (dest_prodT pT)) $ p
   280   end;
   281 
   282 fun mk_snd p =
   283   let val pT = fastype_of p in
   284     Const ("snd", pT --> snd (dest_prodT pT)) $ p
   285   end;
   286 
   287 fun split_const (A, B, C) =
   288   Const ("split", (A --> B --> C) --> mk_prodT (A, B) --> C);
   289 
   290 fun mk_split t =
   291   (case Term.fastype_of t of
   292     T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
   293       Const ("split", T --> mk_prodT (A, B) --> C) $ t
   294   | _ => raise TERM ("mk_split: bad body type", [t]));
   295 
   296 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
   297 fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
   298   | prodT_factors T = [T];
   299 
   300 (*Makes a nested tuple from a list, following the product type structure*)
   301 fun mk_tuple (Type ("*", [T1, T2])) tms =
   302         mk_prod (mk_tuple T1 tms,
   303                  mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
   304   | mk_tuple T (t::_) = t;
   305 
   306 fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
   307   | dest_tuple t = [t];
   308 
   309 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   310   with result type T.  The call creates a new term expecting one argument
   311   of type S.*)
   312 fun ap_split T T3 u =
   313   let
   314     fun ap (T :: Ts) =
   315           (case T of
   316              Type ("*", [T1, T2]) =>
   317                split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
   318            | _ => Abs ("x", T, ap Ts))
   319       | ap [] =
   320           let val k = length (prodT_factors T)
   321           in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
   322   in ap [T] end;
   323 
   324 
   325 (***********************************************************)
   326 (*       operations on tuples with specific arities        *)
   327 (*                                                         *)
   328 (* an "arity" of a tuple is a list of lists of integers    *)
   329 (* ("factors"), denoting paths to subterms that are pairs  *)
   330 (***********************************************************)
   331 
   332 fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
   333 
   334 fun prod_factors t =
   335   let
   336     fun factors p (Const ("Pair", _) $ t $ u) =
   337           p :: factors (1::p) t @ factors (2::p) u
   338       | factors p _ = []
   339   in factors [] t end;
   340 
   341 fun dest_tuple' ps =
   342   let
   343     fun dest p t = if p mem ps then (case t of
   344         Const ("Pair", _) $ t $ u =>
   345           dest (1::p) t @ dest (2::p) u
   346       | _ => prod_err "dest_tuple'") else [t]
   347   in dest [] end;
   348 
   349 fun prodT_factors' ps =
   350   let
   351     fun factors p T = if p mem ps then (case T of
   352         Type ("*", [T1, T2]) =>
   353           factors (1::p) T1 @ factors (2::p) T2
   354       | _ => prod_err "prodT_factors'") else [T]
   355   in factors [] end;
   356 
   357 (*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
   358   with result type T.  The call creates a new term expecting one argument
   359   of type S.*)
   360 fun ap_split' ps T T3 u =
   361   let
   362     fun ap ((p, T) :: pTs) =
   363           if p mem ps then (case T of
   364               Type ("*", [T1, T2]) =>
   365                 split_const (T1, T2, map snd pTs ---> T3) $
   366                   ap ((1::p, T1) :: (2::p, T2) :: pTs)
   367             | _ => prod_err "ap_split'")
   368           else Abs ("x", T, ap pTs)
   369       | ap [] =
   370           let val k = length ps
   371           in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   372   in ap [([], T)] end;
   373 
   374 fun mk_tuple' ps =
   375   let
   376     fun mk p T ts =
   377       if p mem ps then (case T of
   378           Type ("*", [T1, T2]) =>
   379             let
   380               val (t, ts') = mk (1::p) T1 ts;
   381               val (u, ts'') = mk (2::p) T2 ts'
   382             in (pair_const T1 T2 $ t $ u, ts'') end
   383         | _ => prod_err "mk_tuple'")
   384       else (hd ts, tl ts)
   385   in fst oo mk [] end;
   386 
   387 fun mk_tupleT ps =
   388   let
   389     fun mk p Ts =
   390       if p mem ps then
   391         let
   392           val (T, Ts') = mk (1::p) Ts;
   393           val (U, Ts'') = mk (2::p) Ts'
   394         in (mk_prodT (T, U), Ts'') end
   395       else (hd Ts, tl Ts)
   396   in fst o mk [] end;
   397 
   398 fun strip_split t =
   399   let
   400     fun strip [] qs Ts t = (t, Ts, qs)
   401       | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   402           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
   403       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
   404       | strip (p :: ps) qs Ts t = strip ps qs
   405           (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
   406           (incr_boundvars 1 t $ Bound 0)
   407   in strip [[]] [] [] t end;
   408 
   409 
   410 (* nat *)
   411 
   412 val natT = Type ("nat", []);
   413 
   414 val zero = Const ("HOL.zero_class.zero", natT);
   415 
   416 fun is_zero (Const ("HOL.zero_class.zero", _)) = true
   417   | is_zero _ = false;
   418 
   419 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   420 
   421 fun dest_Suc (Const ("Suc", _) $ t) = t
   422   | dest_Suc t = raise TERM ("dest_Suc", [t]);
   423 
   424 val Suc_zero = mk_Suc zero;
   425 
   426 fun mk_nat n =
   427   let
   428     fun mk 0 = zero
   429       | mk n = mk_Suc (mk (n - 1));
   430   in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
   431 
   432 fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
   433   | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   434   | dest_nat t = raise TERM ("dest_nat", [t]);
   435 
   436 val class_size = "Nat.size";
   437 
   438 fun size_const T = Const ("Nat.size_class.size", T --> natT);
   439 
   440 
   441 (* bit *)
   442 
   443 val bitT = Type ("Numeral.bit", []);
   444 
   445 val B0_const = Const ("Numeral.bit.B0", bitT);
   446 val B1_const =  Const ("Numeral.bit.B1", bitT);
   447 
   448 fun mk_bit 0 = B0_const
   449   | mk_bit 1 = B1_const
   450   | mk_bit _ = raise TERM ("mk_bit", []);
   451 
   452 fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
   453   | dest_bit (Const ("Numeral.bit.B1", _)) = 1
   454   | dest_bit t = raise TERM ("dest_bit", [t]);
   455 
   456 
   457 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *)
   458 
   459 val intT = Type ("IntDef.int", []);
   460 
   461 val pls_const = Const ("Numeral.Pls", intT)
   462 and min_const = Const ("Numeral.Min", intT)
   463 and bit_const = Const ("Numeral.Bit", intT --> bitT --> intT);
   464 
   465 fun mk_numeral 0 = pls_const
   466   | mk_numeral ~1 = min_const
   467   | mk_numeral i =
   468       let val (q, r) = Integer.div_mod i 2;
   469       in bit_const $ mk_numeral q $ mk_bit r end;
   470 
   471 fun dest_numeral (Const ("Numeral.Pls", _)) = 0
   472   | dest_numeral (Const ("Numeral.Min", _)) = ~1
   473   | dest_numeral (Const ("Numeral.Bit", _) $ bs $ b) = 2 * dest_numeral bs + dest_bit b
   474   | dest_numeral t = raise TERM ("dest_numeral", [t]);
   475 
   476 fun number_of_const T = Const ("Numeral.number_class.number_of", intT --> T);
   477 
   478 fun add_numerals (Const ("Numeral.number_class.number_of", Type (_, [_, T])) $ t) = cons (t, T)
   479   | add_numerals (t $ u) = add_numerals t #> add_numerals u
   480   | add_numerals (Abs (_, _, t)) = add_numerals t
   481   | add_numerals _ = I;
   482 
   483 fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
   484   | mk_number T 1 = Const ("HOL.one_class.one", T)
   485   | mk_number T i = number_of_const T $ mk_numeral i;
   486 
   487 fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
   488   | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
   489   | dest_number (Const ("Numeral.number_class.number_of", Type ("fun", [_, T])) $ t) =
   490       (T, dest_numeral t)
   491   | dest_number t = raise TERM ("dest_number", [t]);
   492 
   493 
   494 (* real *)
   495 
   496 val realT = Type ("RealDef.real", []);
   497 
   498 
   499 (* nibble *)
   500 
   501 val nibbleT = Type ("List.nibble", []);
   502 
   503 fun mk_nibble n =
   504   let val s =
   505     if 0 <= n andalso n <= 9 then chr (n + ord "0")
   506     else if 10 <= n andalso n <= 15 then chr (n + ord "A" - 10)
   507     else raise TERM ("mk_nibble", [])
   508   in Const ("List.nibble.Nibble" ^ s, nibbleT) end;
   509 
   510 fun dest_nibble t =
   511   let fun err () = raise TERM ("dest_nibble", [t]) in
   512     (case try (unprefix "List.nibble.Nibble" o fst o Term.dest_Const) t of
   513       NONE => err ()
   514     | SOME c =>
   515         if size c <> 1 then err ()
   516         else if "0" <= c andalso c <= "9" then ord c - ord "0"
   517         else if "A" <= c andalso c <= "F" then ord c - ord "A" + 10
   518         else err ())
   519   end;
   520 
   521 
   522 (* char *)
   523 
   524 val charT = Type ("List.char", []);
   525 
   526 fun mk_char n =
   527   if 0 <= n andalso n <= 255 then
   528     Const ("List.char.Char", nibbleT --> nibbleT --> charT) $
   529       mk_nibble (n div 16) $ mk_nibble (n mod 16)
   530   else raise TERM ("mk_char", []);
   531 
   532 fun dest_char (Const ("List.char.Char", _) $ t $ u) =
   533       dest_nibble t * 16 + dest_nibble u
   534   | dest_char t = raise TERM ("dest_char", [t]);
   535 
   536 
   537 (* list *)
   538 
   539 fun listT T = Type ("List.list", [T]);
   540 
   541 fun mk_list T ts =
   542   let
   543     val lT = listT T;
   544     val Nil = Const ("List.list.Nil", lT);
   545     fun Cons t u = Const ("List.list.Cons", T --> lT --> lT) $ t $ u;
   546   in fold_rev Cons ts Nil end;
   547 
   548 fun dest_list (Const ("List.list.Nil", _)) = []
   549   | dest_list (Const ("List.list.Cons", _) $ t $ u) = t :: dest_list u
   550   | dest_list t = raise TERM ("dest_list", [t]);
   551 
   552 
   553 (* string *)
   554 
   555 val stringT = Type ("List.string", []);
   556 
   557 val mk_string = mk_list charT o map (mk_char o ord) o explode;
   558 val dest_string = implode o map (chr o dest_char) o dest_list;
   559 
   560 end;