1(* Title: HOL/Tools/BNF/bnf_gfp_util.ML 2 Author: Dmitriy Traytel, TU Muenchen 3 Copyright 2012 4 5Library for the codatatype construction. 6*) 7 8signature BNF_GFP_UTIL = 9sig 10 val mk_rec_simps: int -> thm -> thm list -> thm list list 11 12 val dest_listT: typ -> typ 13 14 val mk_Cons: term -> term -> term 15 val mk_InN: typ list -> term -> int -> term 16 val mk_Shift: term -> term -> term 17 val mk_Succ: term -> term -> term 18 val mk_Times: term * term -> term 19 val mk_append: term * term -> term 20 val mk_congruent: term -> term -> term 21 val mk_Id_on: term -> term 22 val mk_in_rel: term -> term 23 val mk_equiv: term -> term -> term 24 val mk_fromCard: term -> term -> term 25 val mk_proj: term -> term 26 val mk_quotient: term -> term -> term 27 val mk_rec_list: term -> term -> term 28 val mk_rec_nat: term -> term -> term 29 val mk_shift: term -> term -> term 30 val mk_size: term -> term 31 val mk_toCard: term -> term -> term 32 val mk_undefined: typ -> term 33 val mk_univ: term -> term 34 35 val mk_specN: int -> thm -> thm 36 37 val mk_InN_Field: int -> int -> thm 38 val mk_InN_inject: int -> int -> thm 39 val mk_InN_not_InM: int -> int -> thm 40 val mk_sumEN: int -> thm 41end; 42 43structure BNF_GFP_Util : BNF_GFP_UTIL = 44struct 45 46open BNF_Util 47open BNF_FP_Util 48 49val mk_append = HOLogic.mk_binop \<^const_name>\<open>append\<close>; 50 51fun mk_equiv B R = 52 Const (\<^const_name>\<open>equiv\<close>, fastype_of B --> fastype_of R --> HOLogic.boolT) $ B $ R; 53 54fun mk_InN [_] t 1 = t 55 | mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t 56 | mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) 57 | mk_InN Ts t _ = raise TYPE ("mk_InN", Ts, [t]); 58 59fun mk_Sigma (A, B) = 60 let 61 val AT = fastype_of A; 62 val BT = fastype_of B; 63 val ABT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT (range_type BT)); 64 in Const (\<^const_name>\<open>Sigma\<close>, AT --> BT --> ABT) $ A $ B end; 65 66fun mk_Id_on A = 67 let 68 val AT = fastype_of A; 69 val AAT = mk_relT (HOLogic.dest_setT AT, HOLogic.dest_setT AT); 70 in Const (\<^const_name>\<open>Id_on\<close>, AT --> AAT) $ A end; 71 72fun mk_in_rel R = 73 let 74 val ((A, B), RT) = `dest_relT (fastype_of R); 75 in Const (\<^const_name>\<open>in_rel\<close>, RT --> mk_pred2T A B) $ R end; 76 77fun mk_Times (A, B) = 78 let val AT = HOLogic.dest_setT (fastype_of A); 79 in mk_Sigma (A, Term.absdummy AT B) end; 80 81fun dest_listT (Type (\<^type_name>\<open>list\<close>, [T])) = T 82 | dest_listT T = raise TYPE ("dest_setT: set type expected", [T], []); 83 84fun mk_Succ Kl kl = 85 let val T = fastype_of kl; 86 in 87 Const (\<^const_name>\<open>Succ\<close>, 88 HOLogic.mk_setT T --> T --> HOLogic.mk_setT (dest_listT T)) $ Kl $ kl 89 end; 90 91fun mk_Shift Kl k = 92 let val T = fastype_of Kl; 93 in 94 Const (\<^const_name>\<open>Shift\<close>, T --> dest_listT (HOLogic.dest_setT T) --> T) $ Kl $ k 95 end; 96 97fun mk_shift lab k = 98 let val T = fastype_of lab; 99 in 100 Const (\<^const_name>\<open>shift\<close>, T --> dest_listT (Term.domain_type T) --> T) $ lab $ k 101 end; 102 103fun mk_toCard A r = 104 let 105 val AT = fastype_of A; 106 val rT = fastype_of r; 107 in 108 Const (\<^const_name>\<open>toCard\<close>, 109 AT --> rT --> HOLogic.dest_setT AT --> fst (dest_relT rT)) $ A $ r 110 end; 111 112fun mk_fromCard A r = 113 let 114 val AT = fastype_of A; 115 val rT = fastype_of r; 116 in 117 Const (\<^const_name>\<open>fromCard\<close>, 118 AT --> rT --> fst (dest_relT rT) --> HOLogic.dest_setT AT) $ A $ r 119 end; 120 121fun mk_Cons x xs = 122 let val T = fastype_of xs; 123 in Const (\<^const_name>\<open>Cons\<close>, dest_listT T --> T --> T) $ x $ xs end; 124 125fun mk_size t = HOLogic.size_const (fastype_of t) $ t; 126 127fun mk_quotient A R = 128 let val T = fastype_of A; 129 in Const (\<^const_name>\<open>quotient\<close>, T --> fastype_of R --> HOLogic.mk_setT T) $ A $ R end; 130 131fun mk_proj R = 132 let val ((AT, BT), T) = `dest_relT (fastype_of R); 133 in Const (\<^const_name>\<open>proj\<close>, T --> AT --> HOLogic.mk_setT BT) $ R end; 134 135fun mk_univ f = 136 let val ((AT, BT), T) = `dest_funT (fastype_of f); 137 in Const (\<^const_name>\<open>univ\<close>, T --> HOLogic.mk_setT AT --> BT) $ f end; 138 139fun mk_congruent R f = 140 Const (\<^const_name>\<open>congruent\<close>, fastype_of R --> fastype_of f --> HOLogic.boolT) $ R $ f; 141 142fun mk_undefined T = Const (\<^const_name>\<open>undefined\<close>, T); 143 144fun mk_rec_nat Zero Suc = 145 let val T = fastype_of Zero; 146 in Const (\<^const_name>\<open>old.rec_nat\<close>, T --> fastype_of Suc --> HOLogic.natT --> T) $ Zero $ Suc end; 147 148fun mk_rec_list Nil Cons = 149 let 150 val T = fastype_of Nil; 151 val (U, consT) = `(Term.domain_type) (fastype_of Cons); 152 in 153 Const (\<^const_name>\<open>rec_list\<close>, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons 154 end; 155 156fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr} 157 | mk_InN_not_InM n m = 158 if n > m then mk_InN_not_InM m n RS @{thm not_sym} 159 else mk_InN_not_InM (n - 1) (m - 1) RS @{thm not_arg_cong_Inr}; 160 161fun mk_InN_Field 1 1 = @{thm TrueE[OF TrueI]} 162 | mk_InN_Field _ 1 = @{thm Inl_Field_csum} 163 | mk_InN_Field 2 2 = @{thm Inr_Field_csum} 164 | mk_InN_Field n m = mk_InN_Field (n - 1) (m - 1) RS @{thm Inr_Field_csum}; 165 166fun mk_InN_inject 1 _ = @{thm TrueE[OF TrueI]} 167 | mk_InN_inject _ 1 = @{thm Inl_inject} 168 | mk_InN_inject 2 2 = @{thm Inr_inject} 169 | mk_InN_inject n m = @{thm Inr_inject} RS mk_InN_inject (n - 1) (m - 1); 170 171fun mk_sumEN 1 = @{thm one_pointE} 172 | mk_sumEN 2 = @{thm sumE} 173 | mk_sumEN n = 174 (fold (fn i => fn thm => @{thm obj_sumE_f} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF 175 replicate n (impI RS allI); 176 177fun mk_specN 0 thm = thm 178 | mk_specN n thm = mk_specN (n - 1) (thm RS spec); 179 180fun mk_rec_simps n rec_thm defs = map (fn i => 181 map (fn def => def RS rec_thm RS mk_nthI n i RS fun_cong) defs) (1 upto n); 182 183end; 184