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