159 |
159 |
160 lemmas [id_simps] = |
160 lemmas [id_simps] = |
161 fun_map_id[THEN eq_reflection] |
161 fun_map_id[THEN eq_reflection] |
162 id_apply[THEN eq_reflection] |
162 id_apply[THEN eq_reflection] |
163 id_def[THEN eq_reflection,symmetric] |
163 id_def[THEN eq_reflection,symmetric] |
164 |
|
165 section {* Matching of Terms and Types *} |
|
166 |
|
167 ML {* |
|
168 fun struct_match_typ (ty, ty') = |
|
169 case (ty, ty') of |
|
170 (_, TVar _) => true |
|
171 | (TFree x, TFree x') => x = x' |
|
172 | (Type (s, tys), Type (s', tys')) => |
|
173 s = s' andalso |
|
174 if (length tys = length tys') |
|
175 then (List.all struct_match_typ (tys ~~ tys')) |
|
176 else false |
|
177 | _ => false |
|
178 |
|
179 fun struct_match_term (trm, trm') = |
|
180 case (trm, trm') of |
|
181 (_, Var _) => true |
|
182 | (Const (s, ty), Const (s', ty')) => s = s' andalso struct_match_typ (ty, ty') |
|
183 | (Free (x, ty), Free (x', ty')) => x = x' andalso struct_match_typ (ty, ty') |
|
184 | (Bound i, Bound j) => i = j |
|
185 | (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t') |
|
186 | (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s') |
|
187 | _ => false |
|
188 *} |
|
189 |
164 |
190 section {* Computation of the Regularize Goal *} |
165 section {* Computation of the Regularize Goal *} |
191 |
166 |
192 (* |
167 (* |
193 Regularizing an rtrm means: |
168 Regularizing an rtrm means: |
324 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
299 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
325 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
300 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
326 val thy = ProofContext.theory_of lthy |
301 val thy = ProofContext.theory_of lthy |
327 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
302 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
328 in |
303 in |
329 if struct_match_term (rtrm, rtrm') then rtrm else |
304 if Pattern.matches thy (rtrm', rtrm) then rtrm else |
330 let |
305 let |
331 val _ = tracing (Syntax.string_of_term @{context} rtrm); |
306 val _ = tracing ("rtrm := " ^ Syntax.string_of_term @{context} rtrm); |
332 val _ = tracing (Syntax.string_of_term @{context} rtrm'); |
307 val _ = tracing ("rtrm':= " ^ Syntax.string_of_term @{context} rtrm'); |
333 in raise exc2 end |
308 in raise exc2 end |
334 end |
309 end |
335 end |
310 end |
336 |
311 |
337 | (t1 $ t2, t1' $ t2') => |
312 | (t1 $ t2, t1' $ t2') => |