equal
deleted
inserted
replaced
319 end |
319 end |
320 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
320 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
321 *} |
321 *} |
322 |
322 |
323 definition |
323 definition |
324 "x IN p ==> (Babs p m x = m x)" |
324 "(x : p) ==> (Babs p m x = m x)" |
325 |
325 |
326 print_theorems |
326 print_theorems |
327 thm Babs_def |
327 thm Babs_def |
328 ML {* type_of @{term Babs } *} |
328 ML {* type_of @{term Babs } *} |
|
329 ML {* type_of @{term Ball } *} |
329 ML {* |
330 ML {* |
330 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
331 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
331 *} |
332 *} |
332 ML {* type_of @{term Respects } *} |
333 ML {* type_of @{term Respects } *} |
333 |
334 |
345 val sub_res_term = tyRel T rty rel lthy; |
346 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 respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
347 val res_term = respects $ sub_res_term; |
348 val res_term = respects $ sub_res_term; |
348 val ty = fastype_of trm; |
349 val ty = fastype_of trm; |
349 val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); |
350 val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); |
350 val rabs_term = rabs $ respects $ lam_term; |
351 val rabs_term = (rabs $ respects) $ lam_term; |
351 in |
352 in |
352 rabs_term |
353 rabs_term |
353 end else let |
354 end else let |
354 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
355 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
355 val v = Free (x', rty); |
356 val v = Free (x', rty); |
358 in |
359 in |
359 Term.lambda_name (x, v) rec_term |
360 Term.lambda_name (x, v) rec_term |
360 end |
361 end |
361 | _ => trm |
362 | _ => trm |
362 |
363 |
|
364 *} |
|
365 |
|
366 term "Babs (Respects (RR)) (\<lambda>x :: trm. x)" |
|
367 |
|
368 (* |
|
369 ML {* |
|
370 Toplevel.program (fn () => |
|
371 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}) |
|
372 ) |
363 *} |
373 *} |
364 |
374 |
365 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
375 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
366 trm == new_trm |
376 trm == new_trm |
367 *) |
377 *) |