File ‹prolog.ML›
structure Prolog =
struct
exception not_HOHH;
fun isD t = case t of
Const(\<^const_name>‹Trueprop›,_)$t => isD t
| Const(\<^const_name>‹HOL.conj› ,_)$l$r => isD l andalso isD r
| Const(\<^const_name>‹HOL.implies›,_)$l$r => isG l andalso isD r
| Const(\<^const_name>‹Pure.imp›,_)$l$r => isG l andalso isD r
| Const(\<^const_name>‹All›,_)$Abs(s,_,t) => isD t
| Const(\<^const_name>‹Pure.all›,_)$Abs(s,_,t) => isD t
| Const(\<^const_name>‹HOL.disj›,_)$_$_ => false
| Const(\<^const_name>‹Ex› ,_)$_ => false
| Const(\<^const_name>‹Not›,_)$_ => false
| Const(\<^const_name>‹True›,_) => false
| Const(\<^const_name>‹False›,_) => false
| l $ r => isD l
| Const _ => true
| Bound _ => true
| Free _ => true
| _ => false
and
isG t = case t of
Const(\<^const_name>‹Trueprop›,_)$t => isG t
| Const(\<^const_name>‹HOL.conj› ,_)$l$r => isG l andalso isG r
| Const(\<^const_name>‹HOL.disj› ,_)$l$r => isG l andalso isG r
| Const(\<^const_name>‹HOL.implies›,_)$l$r => isD l andalso isG r
| Const(\<^const_name>‹Pure.imp›,_)$l$r => isD l andalso isG r
| Const(\<^const_name>‹All›,_)$Abs(_,_,t) => isG t
| Const(\<^const_name>‹Pure.all›,_)$Abs(_,_,t) => isG t
| Const(\<^const_name>‹Ex› ,_)$Abs(_,_,t) => isG t
| Const(\<^const_name>‹True›,_) => true
| Const(\<^const_name>‹Not›,_)$_ => false
| Const(\<^const_name>‹False›,_) => false
| _ => true;
val check_HOHH_tac1 = PRIMITIVE (fn thm =>
if isG (Thm.concl_of thm) then thm else raise not_HOHH);
val check_HOHH_tac2 = PRIMITIVE (fn thm =>
if forall isG (Thm.prems_of thm) then thm else raise not_HOHH);
fun check_HOHH thm = (if isD (Thm.concl_of thm) andalso forall isG (Thm.prems_of thm)
then thm else raise not_HOHH);
fun atomizeD ctxt thm =
let
fun at thm = case Thm.concl_of thm of
_$(Const(\<^const_name>‹All› ,_)$Abs(s,_,_))=>
let val s' = if s="P" then "PP" else s in
at(thm RS (Rule_Insts.read_instantiate ctxt [((("x", 0), Position.none), s')] [s'] spec))
end
| _$(Const(\<^const_name>‹HOL.conj›,_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2)
| _$(Const(\<^const_name>‹HOL.implies›,_)$_$_) => at(thm RS mp)
| _ => [thm]
in map zero_var_indexes (at thm) end;
val atomize_ss =
(empty_simpset \<^context> |> Simplifier.set_mksimps (mksimps mksimps_pairs))
addsimps [
@{thm all_conj_distrib},
@{thm imp_conjL} RS sym,
@{thm imp_conjR},
@{thm imp_all}]
|> simpset_of;
fun hyp_resolve_tac ctxt = SUBGOAL (fn (subgoal, i) =>
let
fun ap (Const(\<^const_name>‹All›,_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t))
| ap (Const(\<^const_name>‹HOL.implies›,_)$_$t) =(case ap t of (k,_,t) => (k,true ,t))
| ap t = (0,false,t);
val prems = Logic.strip_assums_hyp subgoal;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
fun drot_tac k i = DETERM (rotate_tac k i);
fun spec_tac 0 i = all_tac
| spec_tac k i = EVERY' [dresolve_tac ctxt [spec], drot_tac ~1, spec_tac (k-1)] i;
fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
[DETERM o (eresolve_tac ctxt [all_dupE]), drot_tac ~2, spec_tac (k-1)] i;
fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
| same_head k (s$_) (t$_) = same_head k s t
| same_head k (Bound i) (Bound j) = i = j + k
| same_head _ _ _ = true;
fun mapn f n [] = []
| mapn f n (x::xs) = f n x::mapn f (n+1) xs;
fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
if same_head k t concl
then dup_spec_tac k i THEN
(if arrow then eresolve_tac ctxt [mp] i THEN drot_tac (~n) i else assume_tac ctxt i)
else no_tac);
val ptacs = mapn (fn n => fn t =>
pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
in Library.foldl (op APPEND) (no_tac, ptacs) end);
fun ptac ctxt prog = let
val proga = maps (atomizeD ctxt) prog
in (REPEAT_DETERM1 o FIRST' [
resolve_tac ctxt [TrueI],
resolve_tac ctxt [conjI],
resolve_tac ctxt [allI],
resolve_tac ctxt [exI],
resolve_tac ctxt [impI] THEN'
asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN'
(REPEAT_DETERM o (eresolve_tac ctxt [conjE]))
])
ORELSE' resolve_tac ctxt [disjI1,disjI2]
ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac ctxt)
THEN' (fn _ => check_HOHH_tac2))
end;
fun prolog_tac ctxt prog =
check_HOHH_tac1 THEN
DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1);
val prog_HOHH = [];
end;