src/HOL/BNF/Tools/bnf_gfp_util.ML
author blanchet
Mon May 06 21:20:54 2013 +0200 (2013-05-06)
changeset 51884 2928fda12661
parent 51447 a19e973fa2cf
child 51893 596baae88a88
permissions -rw-r--r--
factor out construction of iterator
     1 (*  Title:      HOL/BNF/Tools/bnf_gfp_util.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Copyright   2012
     4 
     5 Library for the codatatype construction.
     6 *)
     7 
     8 signature BNF_GFP_UTIL =
     9 sig
    10   val mk_rec_simps: int -> thm -> thm list -> thm list list
    11 
    12   val dest_listT: typ -> typ
    13 
    14   val mk_Cons: term -> term -> term
    15   val mk_Shift: term -> term -> term
    16   val mk_Succ: term -> term -> term
    17   val mk_Times: term * term -> term
    18   val mk_append: term * term -> term
    19   val mk_congruent: term -> term -> term
    20   val mk_clists: term -> term
    21   val mk_Id_on: term -> term
    22   val mk_equiv: term -> term -> term
    23   val mk_fromCard: term -> term -> term
    24   val mk_list_rec: term -> term -> term
    25   val mk_nat_rec: term -> term -> term
    26   val mk_pickWP: term -> term -> term -> term -> term -> term
    27   val mk_prefCl: term -> term
    28   val mk_prefixeq: term -> term -> term
    29   val mk_proj: term -> term
    30   val mk_quotient: term -> term -> term
    31   val mk_shift: term -> term -> term
    32   val mk_size: term -> term
    33   val mk_thePull: term -> term -> term -> term -> term
    34   val mk_toCard: term -> term -> term
    35   val mk_undefined: typ -> term
    36   val mk_univ: term -> term
    37 
    38   val mk_specN: int -> thm -> thm
    39 
    40   val mk_InN_Field: int -> int -> thm
    41   val mk_InN_inject: int -> int -> thm
    42   val mk_InN_not_InM: int -> int -> thm
    43 end;
    44 
    45 structure BNF_GFP_Util : BNF_GFP_UTIL =
    46 struct
    47 
    48 open BNF_Util
    49 
    50 val mk_append = HOLogic.mk_binop @{const_name append};
    51 
    52 fun mk_equiv B R =
    53   Const (@{const_name equiv}, fastype_of B --> fastype_of R --> HOLogic.boolT) $ B $ R;
    54 
    55 fun mk_Sigma (A, B) =
    56   let
    57     val AT = fastype_of A;
    58     val BT = fastype_of B;
    59     val ABT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT (range_type BT));
    60   in Const (@{const_name Sigma}, AT --> BT --> ABT) $ A $ B end;
    61 
    62 fun mk_Id_on A =
    63   let
    64     val AT = fastype_of A;
    65     val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT);
    66   in Const (@{const_name Id_on}, AT --> AAT) $ A end;
    67 
    68 fun mk_Times (A, B) =
    69   let val AT = HOLogic.dest_setT (fastype_of A);
    70   in mk_Sigma (A, Term.absdummy AT B) end;
    71 
    72 fun dest_listT (Type (@{type_name list}, [T])) = T
    73   | dest_listT T = raise TYPE ("dest_setT: set type expected", [T], []);
    74 
    75 fun mk_Succ Kl kl =
    76   let val T = fastype_of kl;
    77   in
    78     Const (@{const_name Succ},
    79       HOLogic.mk_setT T --> T --> HOLogic.mk_setT (dest_listT T)) $ Kl $ kl
    80   end;
    81 
    82 fun mk_Shift Kl k =
    83   let val T = fastype_of Kl;
    84   in
    85     Const (@{const_name Shift}, T --> dest_listT (HOLogic.dest_setT T) --> T) $ Kl $ k
    86   end;
    87 
    88 fun mk_shift lab k =
    89   let val T = fastype_of lab;
    90   in
    91     Const (@{const_name shift}, T --> dest_listT (Term.domain_type T) --> T) $ lab $ k
    92   end;
    93 
    94 fun mk_prefCl A =
    95   Const (@{const_name prefCl}, fastype_of A --> HOLogic.boolT) $ A;
    96 
    97 fun mk_prefixeq xs ys =
    98   Const (@{const_name prefixeq}, fastype_of xs --> fastype_of ys --> HOLogic.boolT) $ xs $ ys;
    99 
   100 fun mk_clists r =
   101   let val T = fastype_of r;
   102   in Const (@{const_name clists}, T --> mk_relT (`I (HOLogic.listT (fst (dest_relT T))))) $ r end;
   103 
   104 fun mk_toCard A r =
   105   let
   106     val AT = fastype_of A;
   107     val rT = fastype_of r;
   108   in
   109     Const (@{const_name toCard},
   110       AT --> rT --> HOLogic.dest_setT AT --> fst (dest_relT rT)) $ A $ r
   111   end;
   112 
   113 fun mk_fromCard A r =
   114   let
   115     val AT = fastype_of A;
   116     val rT = fastype_of r;
   117   in
   118     Const (@{const_name fromCard},
   119       AT --> rT --> fst (dest_relT rT) --> HOLogic.dest_setT AT) $ A $ r
   120   end;
   121 
   122 fun mk_Cons x xs =
   123   let val T = fastype_of xs;
   124   in Const (@{const_name Cons}, dest_listT T --> T --> T) $ x $ xs end;
   125 
   126 fun mk_size t = HOLogic.size_const (fastype_of t) $ t;
   127 
   128 fun mk_quotient A R =
   129   let val T = fastype_of A;
   130   in Const (@{const_name quotient}, T --> fastype_of R --> HOLogic.mk_setT T) $ A $ R end;
   131 
   132 fun mk_proj R =
   133   let val ((AT, BT), T) = `dest_relT (fastype_of R);
   134   in Const (@{const_name proj}, T --> AT --> HOLogic.mk_setT BT) $ R end;
   135 
   136 fun mk_univ f =
   137   let val ((AT, BT), T) = `dest_funT (fastype_of f);
   138   in Const (@{const_name univ}, T --> HOLogic.mk_setT AT --> BT) $ f end;
   139 
   140 fun mk_congruent R f =
   141   Const (@{const_name congruent}, fastype_of R --> fastype_of f --> HOLogic.boolT) $ R $ f;
   142 
   143 fun mk_undefined T = Const (@{const_name undefined}, T);
   144 
   145 fun mk_nat_rec Zero Suc =
   146   let val T = fastype_of Zero;
   147   in Const (@{const_name nat_rec}, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end;
   148 
   149 fun mk_list_rec Nil Cons =
   150   let
   151     val T = fastype_of Nil;
   152     val (U, consT) = `(Term.domain_type) (fastype_of Cons);
   153   in
   154     Const (@{const_name list_rec}, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons
   155   end;
   156 
   157 fun mk_thePull B1 B2 f1 f2 =
   158   let
   159     val fT1 = fastype_of f1;
   160     val fT2 = fastype_of f2;
   161     val BT1 = domain_type fT1;
   162     val BT2 = domain_type fT2;
   163   in
   164     Const (@{const_name thePull}, HOLogic.mk_setT BT1 --> HOLogic.mk_setT BT2 --> fT1 --> fT2 -->
   165       mk_relT (BT1, BT2)) $ B1 $ B2 $ f1 $ f2
   166   end;
   167 
   168 fun mk_pickWP A f1 f2 b1 b2 =
   169   let
   170     val fT1 = fastype_of f1;
   171     val fT2 = fastype_of f2;
   172     val AT = domain_type fT1;
   173     val BT1 = range_type fT1;
   174     val BT2 = range_type fT2;
   175   in
   176     Const (@{const_name pickWP}, HOLogic.mk_setT AT --> fT1 --> fT2 --> BT1 --> BT2 --> AT) $
   177       A $ f1 $ f2 $ b1 $ b2
   178   end;
   179 
   180 fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr}
   181   | mk_InN_not_InM n m =
   182     if n > m then mk_InN_not_InM m n RS @{thm not_sym}
   183     else mk_InN_not_InM (n - 1) (m - 1) RS @{thm not_arg_cong_Inr};
   184 
   185 fun mk_InN_Field 1 1 = @{thm TrueE[OF TrueI]}
   186   | mk_InN_Field _ 1 = @{thm Inl_Field_csum}
   187   | mk_InN_Field 2 2 = @{thm Inr_Field_csum}
   188   | mk_InN_Field n m = mk_InN_Field (n - 1) (m - 1) RS @{thm Inr_Field_csum};
   189 
   190 fun mk_InN_inject 1 _ = @{thm TrueE[OF TrueI]}
   191   | mk_InN_inject _ 1 = @{thm Inl_inject}
   192   | mk_InN_inject 2 2 = @{thm Inr_inject}
   193   | mk_InN_inject n m = @{thm Inr_inject} RS mk_InN_inject (n - 1) (m - 1);
   194 
   195 fun mk_specN 0 thm = thm
   196   | mk_specN n thm = mk_specN (n - 1) (thm RS spec);
   197 
   198 fun mk_rec_simps n rec_thm defs = map (fn i =>
   199   map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n);
   200 
   201 end;