equal
deleted
inserted
replaced
81 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
81 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
82 |
82 |
83 in |
83 in |
84 |
84 |
85 fun mk_meta_eq r = r RS eq_reflection; |
85 fun mk_meta_eq r = r RS eq_reflection; |
|
86 fun mk_meta_eq_True r = Some(r RS meta_eq_to_obj_eq RS P_imp_P_eq_True); |
86 |
87 |
87 fun mk_meta_eq_simp r = case concl_of r of |
88 fun mk_meta_eq_simp r = case concl_of r of |
88 Const("==",_)$_$_ => r |
89 Const("==",_)$_$_ => r |
89 | _$(Const("op =",_)$lhs$rhs) => |
90 | _$(Const("op =",_)$lhs$rhs) => mk_meta_eq r |
90 (case fst(Logic.rewrite_rule_ok (#sign(rep_thm r)) (prems_of r) lhs rhs) of |
|
91 None => mk_meta_eq r |
|
92 | Some _ => r RS P_imp_P_eq_True) |
|
93 | _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False |
91 | _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False |
94 | _ => r RS P_imp_P_eq_True; |
92 | _ => r RS P_imp_P_eq_True; |
95 (* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
93 (* last 2 lines requires all formulae to be of the from Trueprop(.) *) |
96 |
94 |
97 val simp_thms = map prover |
95 val simp_thms = map prover |
384 eq_assume_tac, ematch_tac [FalseE]]; |
382 eq_assume_tac, ematch_tac [FalseE]]; |
385 |
383 |
386 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
384 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac |
387 setSSolver safe_solver |
385 setSSolver safe_solver |
388 setSolver unsafe_solver |
386 setSolver unsafe_solver |
389 setmksimps (mksimps mksimps_pairs); |
387 setmksimps (mksimps mksimps_pairs) |
|
388 setmkeqTrue mk_meta_eq_True; |
390 |
389 |
391 val HOL_ss = |
390 val HOL_ss = |
392 HOL_basic_ss addsimps |
391 HOL_basic_ss addsimps |
393 ([triv_forall_equality, (* prunes params *) |
392 ([triv_forall_equality, (* prunes params *) |
394 True_implies_equals, (* prune asms `True' *) |
393 True_implies_equals, (* prune asms `True' *) |