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