26 |
26 |
27 (*terms*) |
27 (*terms*) |
28 val dest_conj: term -> term * term |
28 val dest_conj: term -> term * term |
29 val dest_disj: term -> term * term |
29 val dest_disj: term -> term * term |
30 val under_quant: (term -> 'a) -> term -> 'a |
30 val under_quant: (term -> 'a) -> term -> 'a |
|
31 val is_number: term -> bool |
31 |
32 |
32 (*patterns and instantiations*) |
33 (*patterns and instantiations*) |
33 val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm |
34 val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm |
34 val destT1: ctyp -> ctyp |
35 val destT1: ctyp -> ctyp |
35 val destT2: ctyp -> ctyp |
36 val destT2: ctyp -> ctyp |
130 (case t of |
131 (case t of |
131 Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u |
132 Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u |
132 | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u |
133 | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u |
133 | _ => f t) |
134 | _ => f t) |
134 |
135 |
|
136 val is_number = |
|
137 let |
|
138 fun is_num env (Const (@{const_name If}, _) $ _ $ t $ u) = |
|
139 is_num env t andalso is_num env u |
|
140 | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = |
|
141 is_num (t :: env) u |
|
142 | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t |
|
143 | is_num env (Const (@{const_name divide}, _) $ t $ u) = |
|
144 is_num env t andalso is_num env u |
|
145 | is_num env (Bound i) = i < length env andalso is_num env (nth env i) |
|
146 | is_num _ t = can HOLogic.dest_number t |
|
147 in is_num [] end |
|
148 |
135 |
149 |
136 (* patterns and instantiations *) |
150 (* patterns and instantiations *) |
137 |
151 |
138 fun mk_const_pat thy name destT = |
152 fun mk_const_pat thy name destT = |
139 let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name)) |
153 let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name)) |