322 ) |
318 ) |
323 end |
319 end |
324 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
320 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
325 *} |
321 *} |
326 |
322 |
|
323 definition |
|
324 "x IN p ==> (Babs p m x = m x)" |
|
325 |
|
326 print_theorems |
|
327 thm Babs_def |
|
328 ML {* type_of @{term Babs } *} |
327 ML {* |
329 ML {* |
328 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
330 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
329 *} |
331 *} |
330 |
332 ML {* type_of @{term Respects } *} |
331 (* ML {* |
333 |
332 |
334 ML {* |
333 fun regularise trm \<Rightarrow> new_trm |
335 (* trm \<Rightarrow> new_trm *) |
334 (case trm of |
336 fun regularise trm rty rel lthy = |
335 ?? |
337 case trm of |
336 ) |
338 Abs (x, T, t) => |
|
339 if T = rty then let |
|
340 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
341 val v = Free (x', rty); |
|
342 val t' = subst_bound (v, t); |
|
343 val rec_term = regularise t' rty rel lthy2; |
|
344 val lam_term = Term.lambda_name (x, v) rec_term; |
|
345 val sub_res_term = tyRel T rty rel lthy; |
|
346 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
|
347 val res_term = respects $ sub_res_term; |
|
348 val ty = fastype_of trm; |
|
349 val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); |
|
350 val rabs_term = rabs $ respects $ lam_term; |
|
351 in |
|
352 rabs_term |
|
353 end else let |
|
354 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
355 val v = Free (x', rty); |
|
356 val t' = subst_bound (v, t); |
|
357 val rec_term = regularise t' rty rel lthy2; |
|
358 in |
|
359 Term.lambda_name (x, v) rec_term |
|
360 end |
|
361 | _ => trm |
|
362 |
337 *} |
363 *} |
338 |
364 |
339 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
365 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
340 trm == new_trm |
366 trm == new_trm |
341 *) |
367 *) |
1136 cterm_of @{theory} goal |
1162 cterm_of @{theory} goal |
1137 ); |
1163 ); |
1138 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1164 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1139 *} |
1165 *} |
1140 |
1166 |
1141 definition |
|
1142 "x IN p ==> (Babs p m x = m x)" |
|
1143 |
|
1144 print_theorems |
|
1145 thm Babs_def |
|
1146 |
|
1147 lemma "(Ball (Respects ((op \<approx>) ===> (op =))) |
1167 lemma "(Ball (Respects ((op \<approx>) ===> (op =))) |
1148 (((REP_fset ---> id) ---> id) |
1168 (((REP_fset ---> id) ---> id) |
1149 (((ABS_fset ---> id) ---> id) |
1169 (((ABS_fset ---> id) ---> id) |
1150 (\<lambda>P. |
1170 (\<lambda>P. |
1151 (ABS_fset ---> id) ((REP_fset ---> id) P) |
1171 (ABS_fset ---> id) ((REP_fset ---> id) P) |