1(* ===================================================================== *) 2(* FILE : boolSyntax.sml *) 3(* DESCRIPTION : Derived HOL syntax operations. Mostly translated from *) 4(* the hol88 source. *) 5(* *) 6(* AUTHORS : (c) Mike Gordon, University of Cambridge *) 7(* Konrad Slind, University of Calgary *) 8(* Modified : September 1997, Ken Larsen (functor removal) *) 9(* Modified : July 2000, Konrad Slind *) 10(* ===================================================================== *) 11 12structure boolSyntax :> boolSyntax = 13struct 14 15open Feedback Lib HolKernel boolTheory; 16 17val ERR = mk_HOL_ERR "boolSyntax" 18 19(*--------------------------------------------------------------------------- 20 Basic constants 21 ---------------------------------------------------------------------------*) 22 23val equality = prim_mk_const {Name = "=", Thy = "min"} 24val implication = prim_mk_const {Name = "==>", Thy = "min"} 25val select = prim_mk_const {Name = "@", Thy = "min"} 26val T = prim_mk_const {Name = "T", Thy = "bool"} 27val F = prim_mk_const {Name = "F", Thy = "bool"} 28val universal = prim_mk_const {Name = "!", Thy = "bool"} 29val existential = prim_mk_const {Name = "?", Thy = "bool"} 30val exists1 = prim_mk_const {Name = "?!", Thy = "bool"} 31val conjunction = prim_mk_const {Name = "/\\", Thy = "bool"} 32val disjunction = prim_mk_const {Name = "\\/", Thy = "bool"} 33val negation = prim_mk_const {Name = "~", Thy = "bool"} 34val conditional = prim_mk_const {Name = "COND", Thy = "bool"} 35val let_tm = prim_mk_const {Name = "LET", Thy = "bool"} 36val arb = prim_mk_const {Name = "ARB", Thy = "bool"} 37val the_value = prim_mk_const {Name = "the_value", Thy = "bool"} 38val bool_case = prim_mk_const {Name = "COND", Thy = "bool"} 39val literal_case = prim_mk_const {Name = "literal_case", Thy = "bool"} 40val bounded_tm = prim_mk_const {Name = "BOUNDED", Thy = "bool"} 41val IN_tm = prim_mk_const {Name = "IN", Thy = "bool"} 42 43(*--------------------------------------------------------------------------- 44 Derived syntax operations 45 ---------------------------------------------------------------------------*) 46 47fun mk_eq (lhs, rhs) = 48 list_mk_comb (inst [alpha |-> type_of lhs] equality, [lhs, rhs]) 49 handle HOL_ERR _ => raise ERR "mk_eq" "lhs and rhs have different types" 50 51fun mk_imp (ant, conseq) = 52 list_mk_comb (implication, [ant, conseq]) 53 handle HOL_ERR _ => raise ERR "mk_imp" "Non-boolean argument" 54 55val mk_select = mk_binder select "mk_select" 56val mk_forall = mk_binder universal "mk_forall" 57val mk_exists = mk_binder existential "mk_exists" 58val mk_exists1 = mk_binder exists1 "mk_exists1" 59 60fun mk_conj (conj1, conj2) = 61 list_mk_comb (conjunction, [conj1, conj2]) 62 handle HOL_ERR _ => raise ERR "mk_conj" "Non-boolean argument" 63 64fun mk_disj (disj1, disj2) = 65 list_mk_comb (disjunction, [disj1, disj2]) 66 handle HOL_ERR _ => raise ERR "mk_disj" "Non-boolean argument" 67 68fun mk_neg M = 69 with_exn mk_comb (negation, M) (ERR "mk_neg" "Non-boolean argument") 70 71fun mk_cond (cond, larm, rarm) = 72 list_mk_comb (inst [alpha |-> type_of larm] conditional, [cond, larm, rarm]) 73 handle HOL_ERR _ => raise ERR "mk_cond" "" 74 75fun mk_let (func, arg) = 76 let 77 val (dom, rng) = dom_rng (type_of func) 78 in 79 list_mk_comb (inst [alpha |-> dom, beta |-> rng] let_tm, [func, arg]) 80 end 81 handle HOL_ERR _ => raise ERR "mk_let" "" 82 83fun mk_bool_case (a0, a1, b) = 84 list_mk_comb (inst [alpha |-> type_of a0] bool_case, [b, a0, a1]) 85 handle HOL_ERR _ => raise ERR "mk_bool_case" "" 86 87fun mk_literal_case (func, arg) = 88 let 89 val (dom, rng) = dom_rng (type_of func) 90 in 91 list_mk_comb 92 (inst [alpha |-> dom, beta |-> rng] literal_case, [func, arg]) 93 end 94 handle HOL_ERR _ => raise ERR "mk_literal_case" "" 95 96fun mk_arb ty = inst [alpha |-> ty] arb 97 98fun mk_itself ty = inst [alpha |-> ty] the_value 99 100val mk_icomb = Lib.uncurry HolKernel.mk_monop 101 102fun mk_IN (t1, t2) = mk_comb(mk_icomb(IN_tm, t1), t2) 103 104 105 106(*--------------------------------------------------------------------------* 107 * Destructors * 108 *--------------------------------------------------------------------------*) 109 110local 111 val dest_eq_ty_err = ERR "dest_eq(_ty)" "not an \"=\"" 112 val lhs_err = ERR "lhs" "not an \"=\"" 113 val rhs_err = ERR "rhs" "not an \"=\"" 114 val lhand_err = ERR "lhand" "not a binary comb" 115 val dest_imp_err = ERR "dest_imp" "not an \"==>\"" 116 val dest_cond_err = ERR "dest_cond" "not a conditional" 117 val bool_case_err = ERR "dest_bool_case" "not a \"bool_case\"" 118 val literal_case_err = ERR "dest_literal_case" "not a \"literal_case\"" 119in 120 val dest_eq = dest_binop equality dest_eq_ty_err 121 fun dest_eq_ty M = let val (l, r) = dest_eq M in (l, r, type_of l) end 122 fun lhs M = with_exn (fst o dest_eq) M lhs_err 123 fun rhs M = with_exn (snd o dest_eq) M rhs_err 124 fun lhand M = with_exn (rand o rator) M lhand_err 125 126 val dest_neg = dest_monop negation (ERR "dest_neg" "not a negation") 127 val dest_imp_only = dest_binop implication dest_imp_err 128 fun dest_imp M = dest_imp_only M 129 handle HOL_ERR _ => (dest_neg M, F) 130 handle HOL_ERR _ => raise dest_imp_err 131 val dest_select = dest_binder select (ERR "dest_select" "not a \"@\"") 132 val dest_forall = dest_binder universal (ERR "dest_forall" "not a \"!\"") 133 val dest_exists = dest_binder existential (ERR "dest_exists" "not a \"?\"") 134 val dest_exists1 = dest_binder exists1 (ERR "dest_exists1" "not a \"?!\"") 135 val dest_conj = dest_binop conjunction (ERR "dest_conj" "not a \"/\\\"") 136 val dest_disj = dest_binop disjunction (ERR "dest_disj" "not a \"\\/\"") 137 val dest_let = dest_binop let_tm (ERR "dest_let" "not a let term") 138 val dest_IN = dest_binop IN_tm (ERR "dest_IN" "not an IN term") 139 140 fun dest_cond M = 141 let 142 val (Rator, t2) = with_exn dest_comb M dest_cond_err 143 val (b, t1) = dest_binop conditional dest_cond_err Rator 144 in 145 (b, t1, t2) 146 end 147 148 fun dest_bool_case M = 149 let 150 val (Rator, a1) = with_exn dest_comb M bool_case_err 151 val (b, a0) = dest_binop bool_case bool_case_err Rator 152 in 153 (a0, a1, b) 154 end 155 156 val dest_literal_case = dest_binop literal_case literal_case_err 157 158 fun dest_arb M = 159 if same_const M arb then type_of M else raise ERR "dest_arb" "" 160 161 fun dest_itself M = 162 if same_const M the_value 163 then hd (snd (dest_type (type_of M))) 164 else raise ERR "dest_itself" "" 165end (* local *) 166 167(*--------------------------------------------------------------------------- 168 Selectors 169 ---------------------------------------------------------------------------*) 170 171val is_eq = can dest_eq 172val is_imp = can dest_imp 173val is_imp_only = can dest_imp_only 174val is_select = can dest_select 175val is_forall = can dest_forall 176val is_exists = can dest_exists 177val is_exists1 = can dest_exists1 178val is_conj = can dest_conj 179val is_disj = can dest_disj 180val is_neg = can dest_neg 181val is_cond = can dest_cond 182val is_let = can dest_let 183val is_bool_case = can dest_bool_case 184val is_literal_case = can dest_literal_case 185val is_arb = same_const arb 186val is_the_value = same_const the_value 187val is_IN = can dest_IN 188 189(*---------------------------------------------------------------------------* 190 * Construction and destruction functions that deal with SML lists * 191 *---------------------------------------------------------------------------*) 192 193val list_mk_comb = HolKernel.list_mk_comb 194val list_mk_abs = HolKernel.list_mk_abs 195 196val list_mk_forall = list_mk_binder (SOME universal) 197val list_mk_exists = list_mk_binder (SOME existential) 198val list_mk_conj = list_mk_rbinop (curry mk_conj) 199val list_mk_disj = list_mk_rbinop (curry mk_disj) 200 201fun list_mk_imp (A, c) = list_mk_rbinop (curry mk_imp) (A @ [c]) 202 203fun list_mk_icomb (f, args) = List.foldl (fn (a, t) => mk_icomb (t, a)) f args 204 205val strip_comb = HolKernel.strip_comb 206val strip_abs = HolKernel.strip_abs 207val strip_forall = HolKernel.strip_binder (SOME universal) 208val strip_exists = HolKernel.strip_binder (SOME existential) 209val strip_conj = strip_binop (total dest_conj) 210val strip_disj = strip_binop (total dest_disj) 211 212fun dest_strip_comb t = 213 let 214 val (l, r) = strip_comb t 215 val {Thy = thy, Name = name, ...} = Term.dest_thy_const l 216 in 217 (thy ^ "$" ^ name, r) 218 end 219 220val strip_imp = 221 let 222 val desti = total dest_imp 223 fun strip A M = 224 case desti M of 225 NONE => (List.rev A, M) 226 | SOME (ant, conseq) => strip (ant :: A) conseq 227 in 228 strip [] 229 end 230 231val strip_imp_only = 232 let 233 val desti = total dest_imp_only 234 fun strip A M = 235 case desti M of 236 NONE => (List.rev A, M) 237 | SOME (ant, conseq) => strip (ant :: A) conseq 238 in 239 strip [] 240 end 241 242val strip_neg = 243 let 244 val destn = total dest_neg 245 fun strip A M = 246 case destn M of 247 NONE => (M, A) 248 | SOME N => strip (A + 1) N 249 in 250 strip 0 251 end 252 253fun gen_all tm = list_mk_forall (free_vars tm, tm) 254 255(*---------------------------------------------------------------------------* 256 * Construction and destruction of function types from/to lists of types * 257 * Michael Norrish - December 1999 * 258 *---------------------------------------------------------------------------*) 259 260val list_mk_fun = HolKernel.list_mk_fun 261val strip_fun = HolKernel.strip_fun 262 263(*--------------------------------------------------------------------------- 264 Linking definitional principles and signature operations 265 with grammars. 266 ---------------------------------------------------------------------------*) 267 268fun dest t = 269 let 270 val (lhs, rhs) = dest_eq (snd (strip_forall t)) 271 val (f, args) = strip_comb lhs 272 val f = mk_var(dest_const f) handle HOL_ERR _ => f 273 in 274 if all is_var args 275 then (args, mk_eq (f, list_mk_abs (args, rhs))) 276 else raise ERR "new_definition" "non-variable argument" 277 end 278 279fun RIGHT_BETA th = TRANS th (BETA_CONV (rhs (concl th))) 280 281fun post (V, th) = 282 let 283 fun add_var v th = RIGHT_BETA (AP_THM th v) 284 in 285 itlist GEN V (rev_itlist add_var V th) 286 end 287 288val _ = Definition.new_definition_hook := (dest, post) 289 290open Parse 291 292fun defname t = 293 let 294 val head = #1 (strip_comb (lhs (#2 (strip_forall t)))) 295 in 296 fst (dest_var head handle HOL_ERR _ => dest_const head) 297 end 298 299fun new_infixr_definition (s, t, p) = 300 Definition.new_definition (s, t) before set_fixity (defname t) (Infixr p) 301 302fun new_infixl_definition (s, t, p) = 303 Definition.new_definition (s, t) before set_fixity (defname t) (Infixl p) 304 305fun new_binder_definition (s, t) = 306 Definition.new_definition (s, t) before Parse.set_fixity (defname t) Binder 307 308fun new_type_definition (name, inhab_thm) = 309 Definition.new_type_definition (name, inhab_thm) 310 311fun new_infix (Name, Ty, Prec) = 312 Theory.new_constant (Name, Ty) 313 before Parse.add_infix (Name, Prec, Parse.RIGHT) 314 315fun new_binder (p as (Name, _)) = 316 Theory.new_constant p before set_fixity Name Binder 317 318fun new_infix_type (x as {Name, Arity, ParseName, Prec, Assoc}) = 319 let 320 val _ = Arity = 2 orelse 321 raise ERR "new_infix_type" "Infix types must have arity 2" 322 in 323 Theory.new_type (Name, Arity) 324 before Parse.add_infix_type 325 {Name = Name, ParseName = ParseName, Prec = Prec, Assoc = Assoc} 326 end 327 328(*---------------------------------------------------------------------------*) 329(* Lifter for booleans *) 330(*---------------------------------------------------------------------------*) 331 332fun lift_bool _ true = T 333 | lift_bool _ false = F 334 335(*--------------------------------------------------------------------------*) 336(* Some simple algebraic properties expressed at the term level. *) 337(*--------------------------------------------------------------------------*) 338 339val (comm_tm, assoc_tm, idem_tm, ldistrib_tm, rdistrib_tm) = 340 let 341 val f = mk_var ("f", alpha --> alpha --> alpha) 342 val g = mk_var ("g", alpha --> alpha --> alpha) 343 val g1 = mk_var ("g", alpha --> alpha) 344 val x = mk_var ("x", alpha) 345 val y = mk_var ("y", alpha) 346 val z = mk_var ("z", alpha) 347 in 348 (mk_eq (list_mk_comb (f, [x, y]), list_mk_comb (f, [y, x])), 349 mk_eq (list_mk_comb (f, [x, list_mk_comb (f, [y, z])]), 350 list_mk_comb (f, [list_mk_comb (f, [x, y]), z])), 351 mk_eq (mk_comb (g1, mk_comb (g1, x)), mk_comb (g1, x)), 352 mk_eq (list_mk_comb (f, [x, list_mk_comb (g, [y, z])]), 353 list_mk_comb (g, [list_mk_comb (f, [x, y]), 354 list_mk_comb (f, [x, z])])), 355 mk_eq (list_mk_comb (f, [list_mk_comb (g, [y, z]), x]), 356 list_mk_comb (g, [list_mk_comb (f, [y, x]), 357 list_mk_comb (f, [z, x])]))) 358 end 359 360(* ===================================================================== *) 361(* Syntactic operations on restricted quantifications. *) 362(* These ought to be generalised to all kinds of restrictions, *) 363(* but one thing at a time. *) 364(* --------------------------------------------------------------------- *) 365 366val (mk_res_forall, mk_res_exists, mk_res_exists_unique, 367 mk_res_select, mk_res_abstract) = 368 let 369 fun mk_res_quan cons s (x, t1, t2) = 370 let 371 val xty = type_of x 372 val t2_ty = type_of t2 373 val ty = (xty --> bool) --> (xty --> t2_ty) 374 --> (if cons = "RES_ABSTRACT" 375 then xty --> t2_ty 376 else if cons = "RES_SELECT" 377 then xty 378 else Type.bool) 379 in 380 mk_comb (mk_comb (mk_thy_const {Name=cons, Thy="bool", Ty=ty}, t1), 381 mk_abs (x, t2)) 382 end 383 handle _ => raise ERR "mk_res_quan" s 384 in 385 (mk_res_quan "RES_FORALL" "mk_res_forall", 386 mk_res_quan "RES_EXISTS" "mk_res_exists", 387 mk_res_quan "RES_EXISTS_UNIQUE" "mk_res_exists_unique", 388 mk_res_quan "RES_SELECT" "mk_res_select", 389 mk_res_quan "RES_ABSTRACT" "mk_res_abstract") 390 end 391 392fun list_mk_res_forall (ress, body) = 393 (itlist (fn (v, p) => fn b => mk_res_forall (v, p, b)) ress body) 394 handle _ => raise ERR "list_mk_res_forall" "" 395 396fun list_mk_res_exists (ress, body) = 397 (itlist (fn (v, p) => fn b => mk_res_exists (v, p, b)) ress body) 398 handle _ => raise ERR "list_mk_res_exists" "" 399 400val (dest_res_forall, dest_res_exists, dest_res_exists_unique, 401 dest_res_select, dest_res_abstract) = 402 let 403 fun dest_res_quan cons s = 404 let 405 val check = 406 assert (fn c => 407 let 408 val {Name, Thy, ...} = dest_thy_const c 409 in 410 Name = cons andalso Thy = "bool" 411 end) 412 in 413 fn tm => 414 let 415 val (op1, rand1) = dest_comb tm 416 val (op2, c1) = dest_comb op1 417 val _ = check op2 418 val (c2, c3) = dest_abs rand1 419 in 420 (c2, c1, c3) 421 end 422 end 423 handle _ => raise ERR "dest_res_quan" s 424 in 425 (dest_res_quan "RES_FORALL" "dest_res_forall", 426 dest_res_quan "RES_EXISTS" "dest_res_exists", 427 dest_res_quan "RES_EXISTS_UNIQUE" "dest_res_exists_unique", 428 dest_res_quan "RES_SELECT" "dest_res_select", 429 dest_res_quan "RES_ABSTRACT" "dest_res_abstract") 430 end 431 432fun strip_res_forall fm = 433 let 434 val (bv, pred, body) = dest_res_forall fm 435 val (prs, core) = strip_res_forall body 436 in 437 ((bv, pred) :: prs, core) 438 end 439 handle _ => ([], fm) 440 441fun strip_res_exists fm = 442 let 443 val (bv, pred, body) = dest_res_exists fm 444 val (prs, core) = strip_res_exists body 445 in 446 ((bv, pred) :: prs, core) 447 end 448 handle _ => ([], fm) 449 450val is_res_forall = can dest_res_forall 451val is_res_exists = can dest_res_exists 452val is_res_exists_unique = can dest_res_exists_unique 453val is_res_select = can dest_res_select 454val is_res_abstract = can dest_res_abstract 455 456fun mk n = prim_mk_const {Name = n, Thy = "bool"} 457 458val res_forall_tm = mk "RES_FORALL" 459val res_exists_tm = mk "RES_EXISTS" 460val res_exists1_tm = mk "RES_EXISTS_UNIQUE" 461val res_select_tm = mk "RES_SELECT" 462val res_abstract_tm = mk "RES_ABSTRACT" 463 464fun op~~(t1,t2) = aconv t1 t2 465fun op!~(t1,t2) = not (t1 ~~ t2) 466val ES = HOLset.empty Term.compare 467fun singt t = HOLset.add(ES, t) 468fun listset ts = HOLset.addList(ES, ts) 469fun FVLset ts = FVL ts ES 470fun FVs t = FVLset [t] 471 472end 473