26 val eq_ctyp: ctyp * ctyp -> bool |
26 val eq_ctyp: ctyp * ctyp -> bool |
27 val aconvc: cterm * cterm -> bool |
27 val aconvc: cterm * cterm -> bool |
28 val add_tvars: thm -> ctyp list -> ctyp list |
28 val add_tvars: thm -> ctyp list -> ctyp list |
29 val add_frees: thm -> cterm list -> cterm list |
29 val add_frees: thm -> cterm list -> cterm list |
30 val add_vars: thm -> cterm list -> cterm list |
30 val add_vars: thm -> cterm list -> cterm list |
|
31 val dest_ctyp_fun: ctyp -> ctyp * ctyp |
|
32 val strip_type: ctyp -> ctyp list * ctyp |
31 val all_name: Proof.context -> string * cterm -> cterm -> cterm |
33 val all_name: Proof.context -> string * cterm -> cterm -> cterm |
32 val all: Proof.context -> cterm -> cterm -> cterm |
34 val all: Proof.context -> cterm -> cterm -> cterm |
33 val mk_binop: cterm -> cterm -> cterm -> cterm |
35 val mk_binop: cterm -> cterm -> cterm -> cterm |
34 val dest_binop: cterm -> cterm * cterm |
36 val dest_binop: cterm -> cterm * cterm |
35 val dest_implies: cterm -> cterm * cterm |
37 val dest_implies: cterm -> cterm * cterm |
140 val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); |
142 val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); |
141 val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); |
143 val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); |
142 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); |
144 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); |
143 |
145 |
144 |
146 |
|
147 (* ctyp destructors *) |
|
148 |
|
149 fun dest_ctyp_fun cT = |
|
150 let |
|
151 val T = Thm.typ_of cT; |
|
152 fun dest_ctyp_nth i = Thm.dest_ctyp_nth i cT; |
|
153 in |
|
154 (case T of |
|
155 Type ("fun", _) => (dest_ctyp_nth 0, dest_ctyp_nth 1) |
|
156 | _ => raise TYPE ("dest_ctyp_fun", [T], [])) |
|
157 end; |
|
158 |
|
159 (* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) |
|
160 fun strip_type cT = |
|
161 (case Thm.typ_of cT of |
|
162 Type ("fun", _) => |
|
163 let |
|
164 val (cT1, cT2) = dest_ctyp_fun cT; |
|
165 val (cTs, cT') = strip_type cT2 |
|
166 in (cT1 :: cTs, cT') end |
|
167 | _ => ([], cT)); |
|
168 |
|
169 |
145 (* cterm constructors and destructors *) |
170 (* cterm constructors and destructors *) |
146 |
171 |
147 fun all_name ctxt (x, t) A = |
172 fun all_name ctxt (x, t) A = |
148 let |
173 let |
149 val T = Thm.typ_of_cterm t; |
174 val T = Thm.typ_of_cterm t; |