equal
deleted
inserted
replaced
428 thm FORALL_PRS |
428 thm FORALL_PRS |
429 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} |
429 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} |
430 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} |
430 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} |
431 ML {* ObjectLogic.rulify t_s *} |
431 ML {* ObjectLogic.rulify t_s *} |
432 |
432 |
433 ML {* Type.freeze *} |
|
434 |
|
435 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *} |
433 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *} |
436 ML {* val vars = map Free (Term.add_frees gl []) *} |
434 ML {* val vars = map Free (Term.add_frees gl []) *} |
437 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *} |
435 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *} |
438 ML {* val gla = fold lambda_all vars gl *} |
436 ML {* val gla = fold lambda_all vars gl *} |
439 ML {* val glf = Type.freeze gla *} |
437 ML {* val glf = Type.legacy_freeze gla *} |
440 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *} |
438 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *} |
441 |
439 |
442 ML {* |
440 ML {* |
443 fun apply_subt2 f trm trm2 = |
441 fun apply_subt2 f trm trm2 = |
444 case (trm, trm2) of |
442 case (trm, trm2) of |
487 ) |
485 ) |
488 end |
486 end |
489 else error "tyRel2 fail: different type structures" |
487 else error "tyRel2 fail: different type structures" |
490 | _ => HOLogic.eq_const ty) |
488 | _ => HOLogic.eq_const ty) |
491 *} |
489 *} |
|
490 |
|
491 ML mk_babs |
|
492 |
|
493 ML {* |
|
494 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) |
|
495 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) |
|
496 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) |
|
497 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) |
|
498 *} |
|
499 |
492 |
500 |
493 ML {* |
501 ML {* |
494 fun my_reg2 lthy trm gtrm = |
502 fun my_reg2 lthy trm gtrm = |
495 case (trm, gtrm) of |
503 case (trm, gtrm) of |
496 (Abs (x, T, t), Abs (x2, T2, t2)) => |
504 (Abs (x, T, t), Abs (x2, T2, t2)) => |