318 ) |
318 ) |
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 ML {* |
|
324 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
|
325 *} |
|
326 |
323 definition |
327 definition |
324 "(x : p) ==> (Babs p m x = m x)" |
328 "(x : p) \<Longrightarrow> (Babs p m x = m x)" |
325 |
329 |
326 print_theorems |
330 print_theorems |
327 thm Babs_def |
331 |
328 ML {* type_of @{term Babs } *} |
332 thm Ball_def |
329 ML {* type_of @{term Ball } *} |
333 |
330 ML {* |
334 definition |
331 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
335 "BAll A P \<equiv> (\<And>x. x \<in> A \<Longrightarrow> P x)" |
332 *} |
336 thm BAll_def |
333 ML {* type_of @{term Respects } *} |
|
334 |
337 |
335 ML {* |
338 ML {* |
336 (* trm \<Rightarrow> new_trm *) |
339 (* trm \<Rightarrow> new_trm *) |
337 fun regularise trm rty rel lthy = |
340 fun regularise trm rty rel lthy = |
338 case trm of |
341 case trm of |
346 val sub_res_term = tyRel T rty rel lthy; |
349 val sub_res_term = tyRel T rty rel lthy; |
347 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
350 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
348 val res_term = respects $ sub_res_term; |
351 val res_term = respects $ sub_res_term; |
349 val ty = fastype_of trm; |
352 val ty = fastype_of trm; |
350 val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); |
353 val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); |
351 val rabs_term = (rabs $ respects) $ lam_term; |
354 val rabs_term = (rabs $ res_term) $ lam_term; |
352 in |
355 in |
353 rabs_term |
356 rabs_term |
354 end else let |
357 end else let |
355 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
358 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
356 val v = Free (x', rty); |
359 val v = Free (x', rty); |
357 val t' = subst_bound (v, t); |
360 val t' = subst_bound (v, t); |
358 val rec_term = regularise t' rty rel lthy2; |
361 val rec_term = regularise t' rty rel lthy2; |
359 in |
362 in |
360 Term.lambda_name (x, v) rec_term |
363 Term.lambda_name (x, v) rec_term |
361 end |
364 end |
|
365 | ((Const (@{const_name "All"}, _)) $ (Abs (x, T, t))) => |
|
366 if T = rty then let |
|
367 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
368 val v = Free (x', rty); |
|
369 val t' = subst_bound (v, t); |
|
370 val rec_term = regularise t' rty rel lthy2; |
|
371 val lam_term = Term.lambda_name (x, v) rec_term; |
|
372 val sub_res_term = tyRel T rty rel lthy; |
|
373 val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); |
|
374 val res_term = respects $ sub_res_term; |
|
375 val ty = fastype_of lam_term; |
|
376 val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool}); |
|
377 val rall_term = (rall $ res_term) $ lam_term; |
|
378 in |
|
379 rall_term |
|
380 end else let |
|
381 val ([x'], lthy2) = Variable.variant_fixes [x] lthy; |
|
382 val v = Free (x', rty); |
|
383 val t' = subst_bound (v, t); |
|
384 val rec_term = regularise t' rty rel lthy2; |
|
385 in |
|
386 Term.lambda_name (x, v) rec_term |
|
387 end |
362 | _ => trm |
388 | _ => trm |
363 |
389 |
364 *} |
390 *} |
365 |
391 term "Ball" |
366 term "Babs (Respects (RR)) (\<lambda>x :: trm. x)" |
392 term "Ball (Respects (RR)) (\<lambda>x :: trm. true)" |
367 |
393 |
368 (* |
394 ML {* |
369 ML {* |
395 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}); |
370 Toplevel.program (fn () => |
396 cterm_of @{theory} (regularise @{term "\<forall>x :: trm. true"} @{typ "trm"} @{term "RR"} @{context}) |
371 cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context}) |
397 *} |
372 ) |
398 |
373 *} |
399 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
374 |
|
375 fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
|
376 trm == new_trm |
400 trm == new_trm |
377 *) |
401 *) |
378 |
402 |
|
403 thm list.induct |
|
404 |
379 text {* produces the definition for a lifted constant *} |
405 text {* produces the definition for a lifted constant *} |
|
406 |
380 ML {* |
407 ML {* |
381 fun get_const_def nconst oconst rty qty lthy = |
408 fun get_const_def nconst oconst rty qty lthy = |
382 let |
409 let |
383 val ty = fastype_of nconst |
410 val ty = fastype_of nconst |
384 val (arg_tys, res_ty) = strip_type ty |
411 val (arg_tys, res_ty) = strip_type ty |