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