47 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
47 val check_HOHH_tac2 = PRIMITIVE (fn thm => |
48 if forall isG (prems_of thm) then thm else raise not_HOHH); |
48 if forall isG (prems_of thm) then thm else raise not_HOHH); |
49 fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) |
49 fun check_HOHH thm = (if isD (concl_of thm) andalso forall isG (prems_of thm) |
50 then thm else raise not_HOHH); |
50 then thm else raise not_HOHH); |
51 |
51 |
52 fun atomizeD ctxt thm = let |
52 fun atomizeD ctxt thm = |
|
53 let |
53 fun at thm = case concl_of thm of |
54 fun at thm = case concl_of thm of |
54 _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS |
55 _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> |
55 (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec)) |
56 let val s' = if s="P" then "PP" else s |
|
57 in at(thm RS (read_instantiate ctxt [(("x", 0), s')] [s'] spec)) end |
56 | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
58 | _$(Const(@{const_name HOL.conj},_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) |
57 | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp) |
59 | _$(Const(@{const_name HOL.implies},_)$_$_) => at(thm RS mp) |
58 | _ => [thm] |
60 | _ => [thm] |
59 in map zero_var_indexes (at thm) end; |
61 in map zero_var_indexes (at thm) end; |
60 |
62 |
61 val atomize_ss = |
63 val atomize_ss = |
62 (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs)) |
64 (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs)) |
63 addsimps [ |
65 addsimps [ |
64 @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |
66 @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *) |