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