src/HOL/HOLCF/Tools/holcf_library.ML
author wenzelm
Sun, 21 Aug 2022 15:00:14 +0200
changeset 75952 864b10457a7d
parent 74375 ba880f3a4e52
permissions -rw-r--r--
more robust concurrency: use shared Browser_Info.Context with synchronized file-system operations; tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41429
diff changeset
     1
(*  Title:      HOL/HOLCF/Tools/holcf_library.ML
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     3
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     4
Functions for constructing HOLCF types and terms.
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     5
*)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     6
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     7
structure HOLCF_Library =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     8
struct
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
     9
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    10
infixr 6 ->>
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    11
infixr -->>
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    12
infix 9 `
35476
8e5eb497b042 fix infix declarations
huffman
parents: 35475
diff changeset
    13
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    14
(*** Operations from Isabelle/HOL ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    15
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    16
val mk_equals = Logic.mk_equals
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    17
val mk_eq = HOLogic.mk_eq
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    18
val mk_trp = HOLogic.mk_Trueprop
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    19
val mk_fst = HOLogic.mk_fst
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    20
val mk_snd = HOLogic.mk_snd
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    21
val mk_not = HOLogic.mk_not
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    22
val mk_conj = HOLogic.mk_conj
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    23
val mk_disj = HOLogic.mk_disj
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    24
val mk_imp = HOLogic.mk_imp
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    25
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    26
fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    27
fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    28
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    29
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    30
(*** Basic HOLCF concepts ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    31
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    32
fun mk_bottom T = \<^Const>\<open>bottom T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    33
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    34
fun below_const T = \<^Const>\<open>below T\<close>
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    35
fun mk_below (t, u) = below_const (fastype_of t) $ t $ u
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    36
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    37
fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t))
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    38
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    39
fun mk_defined t = mk_not (mk_undef t)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    40
40021
d888417f7deb add function mk_adm
huffman
parents: 37108
diff changeset
    41
fun mk_adm t =
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    42
  let val T = Term.domain_type (fastype_of t)
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    43
  in \<^Const>\<open>adm T for t\<close> end
40021
d888417f7deb add function mk_adm
huffman
parents: 37108
diff changeset
    44
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    45
fun mk_compact t =
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    46
  let val T = fastype_of t
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    47
  in \<^Const>\<open>compact T for t\<close> end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    48
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    49
fun mk_cont t =
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    50
  let val \<^Type>\<open>fun A B\<close> = fastype_of t
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    51
  in \<^Const>\<open>cont A B for t\<close> end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    52
35489
dd02201d95b6 add function define_take_functions
huffman
parents: 35476
diff changeset
    53
fun mk_chain t =
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    54
  let val T = Term.range_type (Term.fastype_of t)
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    55
  in \<^Const>\<open>chain T for t\<close> end
35489
dd02201d95b6 add function define_take_functions
huffman
parents: 35476
diff changeset
    56
35555
ec01c27bf580 move function mk_lub into holcf_library.ML
huffman
parents: 35525
diff changeset
    57
fun mk_lub t =
ec01c27bf580 move function mk_lub into holcf_library.ML
huffman
parents: 35525
diff changeset
    58
  let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    59
    val T = Term.range_type (Term.fastype_of t)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 61424
diff changeset
    60
    val UNIV_const = \<^term>\<open>UNIV :: nat set\<close>
74375
ba880f3a4e52 tuned antiquotations;
wenzelm
parents: 74305
diff changeset
    61
  in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end
35555
ec01c27bf580 move function mk_lub into holcf_library.ML
huffman
parents: 35525
diff changeset
    62
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    63
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    64
(*** Continuous function space ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    65
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    66
fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    67
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    68
val (op ->>) = mk_cfunT
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    69
val (op -->>) = Library.foldr mk_cfunT
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    70
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    71
fun dest_cfunT \<^Type>\<open>cfun T U\<close> = (T, U)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    72
  | dest_cfunT T = raise TYPE ("dest_cfunT", [T], [])
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    73
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    74
fun capply_const (S, T) = \<^Const>\<open>Rep_cfun S T\<close>
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    75
fun cabs_const (S, T) = \<^Const>\<open>Abs_cfun S T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    76
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    77
fun mk_cabs t =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    78
  let val T = fastype_of t
40840
2f97215e79bf just one Term.dest_funT;
wenzelm
parents: 40832
diff changeset
    79
  in cabs_const (Term.dest_funT T) $ t end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    80
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    81
(* builds the expression (% v1 v2 .. vn. rhs) *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    82
fun lambdas [] rhs = rhs
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    83
  | lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    84
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    85
(* builds the expression (LAM v. rhs) *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    86
fun big_lambda v rhs =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    87
  cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    88
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    89
(* builds the expression (LAM v1 v2 .. vn. rhs) *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    90
fun big_lambdas [] rhs = rhs
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    91
  | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    92
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    93
fun mk_capply (t, u) =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    94
  let val (S, T) =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    95
    case fastype_of t of
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
    96
        \<^Type>\<open>cfun S T\<close> => (S, T)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    97
      | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u])
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
    98
  in capply_const (S, T) $ t $ u end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
    99
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   100
val (op `) = mk_capply
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   101
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   102
val list_ccomb : term * term list -> term = Library.foldl mk_capply
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   103
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   104
fun mk_ID T = \<^Const>\<open>ID T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   105
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   106
fun mk_cfcomp (f, g) =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   107
  let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   108
    val (U, V) = dest_cfunT (fastype_of f)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   109
    val (T, U') = dest_cfunT (fastype_of g)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   110
  in
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   111
    if U = U'
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   112
    then mk_capply (mk_capply (\<^Const>\<open>cfcomp U V T\<close>, f), g)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   113
    else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   114
  end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   115
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   116
fun mk_strictify t =
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   117
  let val (T, U) = dest_cfunT (fastype_of t)
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   118
  in \<^Const>\<open>strictify T U\<close> ` t end;
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   119
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   120
fun mk_strict t =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   121
  let val (T, U) = dest_cfunT (fastype_of t)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   122
  in mk_eq (t ` mk_bottom T, mk_bottom U) end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   123
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   124
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   125
(*** Product type ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   126
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   127
val mk_prodT = HOLogic.mk_prodT
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   128
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   129
fun mk_tupleT [] = HOLogic.unitT
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   130
  | mk_tupleT [T] = T
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   131
  | mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   132
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   133
(* builds the expression (v1,v2,..,vn) *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   134
fun mk_tuple [] = HOLogic.unit
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   135
  | mk_tuple (t::[]) = t
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   136
  | mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   137
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   138
(* builds the expression (%(v1,v2,..,vn). rhs) *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   139
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   140
  | lambda_tuple (v::[]) rhs = Term.lambda v rhs
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   141
  | lambda_tuple (v::vs) rhs =
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 44169
diff changeset
   142
      HOLogic.mk_case_prod (Term.lambda v (lambda_tuple vs rhs))
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   143
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   144
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   145
(*** Lifted cpo type ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   146
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   147
fun mk_upT T = \<^Type>\<open>u T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   148
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   149
fun dest_upT \<^Type>\<open>u T\<close> = T
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   150
  | dest_upT T = raise TYPE ("dest_upT", [T], [])
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   151
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   152
fun up_const T = \<^Const>\<open>up T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   153
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   154
fun mk_up t = up_const (fastype_of t) ` t
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   155
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   156
fun fup_const (T, U) = \<^Const>\<open>fup T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   157
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   158
fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   159
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   160
fun from_up T = fup_const (T, T) ` mk_ID T
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   161
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   162
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   163
(*** Lifted unit type ***)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   164
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 61424
diff changeset
   165
val oneT = \<^typ>\<open>one\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   166
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   167
fun one_case_const T = \<^Const>\<open>one_case T\<close>
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   168
fun mk_one_case t = one_case_const (fastype_of t) ` t
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   169
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   170
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   171
(*** Strict product type ***)
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   172
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   173
fun mk_sprodT (T, U) = \<^Type>\<open>sprod T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   174
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   175
fun dest_sprodT \<^Type>\<open>sprod T U\<close> = (T, U)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   176
  | dest_sprodT T = raise TYPE ("dest_sprodT", [T], [])
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   177
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   178
fun spair_const (T, U) = \<^Const>\<open>spair T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   179
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   180
(* builds the expression (:t, u:) *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   181
fun mk_spair (t, u) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   182
  spair_const (fastype_of t, fastype_of u) ` t ` u
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   183
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   184
(* builds the expression (:t1,t2,..,tn:) *)
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 61424
diff changeset
   185
fun mk_stuple [] = \<^term>\<open>ONE\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   186
  | mk_stuple (t::[]) = t
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   187
  | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   188
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   189
fun sfst_const (T, U) = \<^Const>\<open>sfst T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   190
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   191
fun ssnd_const (T, U) = \<^Const>\<open>ssnd T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   192
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   193
fun ssplit_const (T, U, V) = \<^Const>\<open>ssplit T U V\<close>
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   194
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   195
fun mk_ssplit t =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   196
  let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t))
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   197
  in ssplit_const (T, U, V) ` t end
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   198
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   199
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   200
(*** Strict sum type ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   201
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   202
fun mk_ssumT (T, U) = \<^Type>\<open>ssum T U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   203
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   204
fun dest_ssumT \<^Type>\<open>ssum T U\<close> = (T, U)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   205
  | dest_ssumT T = raise TYPE ("dest_ssumT", [T], [])
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   206
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   207
fun sinl_const (T, U) = \<^Const>\<open>sinl T U\<close>
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   208
fun sinr_const (T, U) = \<^Const>\<open>sinr U T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   209
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   210
(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   211
fun mk_sinjects ts =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   212
  let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   213
    val Ts = map fastype_of ts
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   214
    fun combine (t, T) (us, U) =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   215
      let
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   216
        val v = sinl_const (T, U) ` t
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   217
        val vs = map (fn u => sinr_const (T, U) ` u) us
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   218
      in
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   219
        (v::vs, mk_ssumT (T, U))
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   220
      end
35912
b0e300bd3a2c error -> raise Fail
huffman
parents: 35906
diff changeset
   221
    fun inj [] = raise Fail "mk_sinjects: empty list"
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   222
      | inj ((t, T)::[]) = ([t], T)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   223
      | inj ((t, T)::ts) = combine (t, T) (inj ts)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   224
  in
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   225
    fst (inj (ts ~~ Ts))
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   226
  end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   227
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   228
fun sscase_const (T, U, V) = \<^Const>\<open>sscase T V U\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   229
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   230
fun mk_sscase (t, u) =
44080
53d95b52954c HOLCF: fix warnings about unreferenced identifiers
huffman
parents: 42151
diff changeset
   231
  let val (T, _) = dest_cfunT (fastype_of t)
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   232
      val (U, V) = dest_cfunT (fastype_of u)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   233
  in sscase_const (T, U, V) ` t ` u end
35785
cdaf99fddd17 move functions into holcf_library.ML
huffman
parents: 35555
diff changeset
   234
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   235
fun from_sinl (T, U) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   236
  sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T)
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   237
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   238
fun from_sinr (T, U) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   239
  sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   240
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   241
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   242
(*** pattern match monad type ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   243
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   244
fun mk_matchT T = \<^Type>\<open>match T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   245
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   246
fun dest_matchT \<^Type>\<open>match T\<close> = T
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   247
  | dest_matchT T = raise TYPE ("dest_matchT", [T], [])
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   248
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   249
fun mk_fail T = \<^Const>\<open>Fixrec.fail T\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   250
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   251
fun succeed_const T = \<^Const>\<open>Fixrec.succeed T\<close>
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   252
fun mk_succeed t = succeed_const (fastype_of t) ` t
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   253
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   254
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   255
(*** lifted boolean type ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   256
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 61424
diff changeset
   257
val trT = \<^typ>\<open>tr\<close>
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   258
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   259
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   260
(*** theory of fixed points ***)
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   261
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   262
fun mk_fix t =
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   263
  let val (T, _) = dest_cfunT (fastype_of t)
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   264
  in mk_capply (\<^Const>\<open>fix T\<close>, t) end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   265
74305
28a582aa25dd more antiquotations;
wenzelm
parents: 69597
diff changeset
   266
fun iterate_const T = \<^Const>\<open>iterate T\<close>
35489
dd02201d95b6 add function define_take_functions
huffman
parents: 35476
diff changeset
   267
dd02201d95b6 add function define_take_functions
huffman
parents: 35476
diff changeset
   268
fun mk_iterate (n, f) =
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   269
  let val (T, _) = dest_cfunT (Term.fastype_of f)
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   270
  in (iterate_const T $ n) ` f ` mk_bottom T end
35475
979019ab92eb move common functions into new file holcf_library.ML
huffman
parents:
diff changeset
   271
40832
4352ca878c41 remove gratuitous semicolons from ML code
huffman
parents: 40774
diff changeset
   272
end