src/HOL/BNF/Tools/bnf_lfp_util.ML
author blanchet
Mon May 06 21:20:54 2013 +0200 (2013-05-06)
changeset 51884 2928fda12661
parent 49510 ba50d204095e
child 53032 953534445ab6
permissions -rw-r--r--
factor out construction of iterator
     1 (*  Title:      HOL/BNF/Tools/bnf_lfp_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012
     5 
     6 Library for the datatype construction.
     7 *)
     8 
     9 signature BNF_LFP_UTIL =
    10 sig
    11   val HOL_arg_cong: cterm -> thm
    12 
    13   val mk_bij_betw: term -> term -> term -> term
    14   val mk_cardSuc: term -> term
    15   val mk_convol: term * term -> term
    16   val mk_cpow: term -> term
    17   val mk_inver: term -> term -> term -> term
    18   val mk_not_empty: term -> term
    19   val mk_not_eq: term -> term -> term
    20   val mk_rapp: term -> typ -> term
    21   val mk_relChain: term -> term -> term
    22   val mk_underS: term -> term
    23   val mk_worec: term -> term -> term
    24 end;
    25 
    26 structure BNF_LFP_Util : BNF_LFP_UTIL =
    27 struct
    28 
    29 open BNF_Util
    30 
    31 fun HOL_arg_cong ct = Drule.instantiate'
    32   (map SOME (Thm.dest_ctyp (Thm.ctyp_of_term ct))) [NONE, NONE, SOME ct] arg_cong;
    33 
    34 (*reverse application*)
    35 fun mk_rapp arg T = Term.absdummy (fastype_of arg --> T) (Bound 0 $ arg);
    36 
    37 fun mk_underS r =
    38   let val T = fst (dest_relT (fastype_of r));
    39   in Const (@{const_name rel.underS}, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
    40 
    41 fun mk_worec r f =
    42   let val (A, AB) = apfst domain_type (dest_funT (fastype_of f));
    43   in Const (@{const_name wo_rel.worec}, mk_relT (A, A) --> (AB --> AB) --> AB) $ r $ f end;
    44 
    45 fun mk_relChain r f =
    46   let val (A, AB) = `domain_type (fastype_of f);
    47   in Const (@{const_name relChain}, mk_relT (A, A) --> AB --> HOLogic.boolT) $ r $ f end;
    48 
    49 fun mk_cardSuc r =
    50   let val T = fst (dest_relT (fastype_of r));
    51   in Const (@{const_name cardSuc}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
    52 
    53 fun mk_cpow r =
    54   let val T = fst (dest_relT (fastype_of r));
    55   in Const (@{const_name cpow}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
    56 
    57 fun mk_bij_betw f A B =
    58  Const (@{const_name bij_betw},
    59    fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
    60 
    61 fun mk_inver f g A =
    62  Const (@{const_name inver}, fastype_of f --> fastype_of g --> fastype_of A --> HOLogic.boolT) $
    63    f $ g $ A;
    64 
    65 fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y));
    66 
    67 fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);
    68 
    69 fun mk_convol (f, g) =
    70   let
    71     val (fU, fTU) = `range_type (fastype_of f);
    72     val ((gT, gU), gTU) = `dest_funT (fastype_of g);
    73     val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
    74   in Const (@{const_name convol}, convolT) $ f $ g end;
    75 
    76 end;