src/HOL/Tools/BNF/bnf_lfp_util.ML
author blanchet
Wed Apr 23 10:23:26 2014 +0200 (2014-04-23)
changeset 56638 092a306bcc3d
parent 56262 251f60be62a7
child 58315 6d8458bc6e27
permissions -rw-r--r--
generate size instances for new-style datatypes
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_util.ML
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@56638
     6
Library for the new-style datatype construction.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
signature BNF_LFP_UTIL =
blanchet@48975
    10
sig
blanchet@48975
    11
  val mk_bij_betw: term -> term -> term -> term
blanchet@48975
    12
  val mk_cardSuc: term -> term
blanchet@48975
    13
  val mk_not_empty: term -> term
blanchet@48975
    14
  val mk_not_eq: term -> term -> term
blanchet@48975
    15
  val mk_rapp: term -> typ -> term
blanchet@48975
    16
  val mk_relChain: term -> term -> term
blanchet@48975
    17
  val mk_underS: term -> term
blanchet@48975
    18
  val mk_worec: term -> term -> term
blanchet@48975
    19
end;
blanchet@48975
    20
blanchet@48975
    21
structure BNF_LFP_Util : BNF_LFP_UTIL =
blanchet@48975
    22
struct
blanchet@48975
    23
blanchet@48975
    24
open BNF_Util
blanchet@48975
    25
blanchet@48975
    26
(*reverse application*)
blanchet@48975
    27
fun mk_rapp arg T = Term.absdummy (fastype_of arg --> T) (Bound 0 $ arg);
blanchet@48975
    28
blanchet@48975
    29
fun mk_underS r =
blanchet@48975
    30
  let val T = fst (dest_relT (fastype_of r));
blanchet@55023
    31
  in Const (@{const_name underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
blanchet@48975
    32
blanchet@48975
    33
fun mk_worec r f =
blanchet@48975
    34
  let val (A, AB) = apfst domain_type (dest_funT (fastype_of f));
blanchet@48975
    35
  in Const (@{const_name wo_rel.worec}, mk_relT (A, A) --> (AB --> AB) --> AB) $ r $ f end;
blanchet@48975
    36
blanchet@48975
    37
fun mk_relChain r f =
blanchet@48975
    38
  let val (A, AB) = `domain_type (fastype_of f);
blanchet@48975
    39
  in Const (@{const_name relChain}, mk_relT (A, A) --> AB --> HOLogic.boolT) $ r $ f end;
blanchet@48975
    40
blanchet@48975
    41
fun mk_cardSuc r =
blanchet@48975
    42
  let val T = fst (dest_relT (fastype_of r));
blanchet@48975
    43
  in Const (@{const_name cardSuc}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
blanchet@48975
    44
blanchet@48975
    45
fun mk_bij_betw f A B =
blanchet@48975
    46
 Const (@{const_name bij_betw},
blanchet@48975
    47
   fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
blanchet@48975
    48
blanchet@48975
    49
fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y));
blanchet@48975
    50
blanchet@48975
    51
fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);
blanchet@48975
    52
blanchet@48975
    53
end;