1(*  Title:      HOL/Tools/BNF/bnf_lfp_util.ML
2    Author:     Dmitriy Traytel, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4    Copyright   2012
5
6Library for the datatype construction.
7*)
8
9signature BNF_LFP_UTIL =
10sig
11  val mk_bij_betw: term -> term -> term -> term
12  val mk_cardSuc: term -> term
13  val mk_not_empty: term -> term
14  val mk_not_eq: term -> term -> term
15  val mk_rapp: term -> typ -> term
16  val mk_relChain: term -> term -> term
17  val mk_underS: term -> term
18  val mk_worec: term -> term -> term
19end;
20
21structure BNF_LFP_Util : BNF_LFP_UTIL =
22struct
23
24open BNF_Util
25
26(*reverse application*)
27fun mk_rapp arg T = Term.absdummy (fastype_of arg --> T) (Bound 0 $ arg);
28
29fun mk_underS r =
30  let val T = fst (dest_relT (fastype_of r));
31  in Const (\<^const_name>\<open>underS\<close>, mk_relT (T, T) --> T --> HOLogic.mk_setT T) $ r end;
32
33fun mk_worec r f =
34  let val (A, AB) = apfst domain_type (dest_funT (fastype_of f));
35  in Const (\<^const_name>\<open>wo_rel.worec\<close>, mk_relT (A, A) --> (AB --> AB) --> AB) $ r $ f end;
36
37fun mk_relChain r f =
38  let val (A, AB) = `domain_type (fastype_of f);
39  in Const (\<^const_name>\<open>relChain\<close>, mk_relT (A, A) --> AB --> HOLogic.boolT) $ r $ f end;
40
41fun mk_cardSuc r =
42  let val T = fst (dest_relT (fastype_of r));
43  in Const (\<^const_name>\<open>cardSuc\<close>, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
44
45fun mk_bij_betw f A B =
46 Const (\<^const_name>\<open>bij_betw\<close>,
47   fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
48
49fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y));
50
51fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);
52
53end;
54