src/HOL/Prolog/prolog.ML
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 60754 02924903a6fd
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:    HOL/Prolog/prolog.ML
     2     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     3 *)
     4 
     5 Options.default_put_bool @{system_option show_main_goal} true;
     6 
     7 structure Prolog =
     8 struct
     9 
    10 exception not_HOHH;
    11 
    12 fun isD t = case t of
    13     Const(@{const_name Trueprop},_)$t     => isD t
    14   | Const(@{const_name HOL.conj}  ,_)$l$r     => isD l andalso isD r
    15   | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
    16   | Const(@{const_name Pure.imp},_)$l$r     => isG l andalso isD r
    17   | Const(@{const_name All},_)$Abs(s,_,t) => isD t
    18   | Const(@{const_name Pure.all},_)$Abs(s,_,t) => isD t
    19   | Const(@{const_name HOL.disj},_)$_$_       => false
    20   | Const(@{const_name Ex} ,_)$_          => false
    21   | Const(@{const_name Not},_)$_          => false
    22   | Const(@{const_name True},_)           => false
    23   | Const(@{const_name False},_)          => false
    24   | l $ r                     => isD l
    25   | Const _ (* rigid atom *)  => true
    26   | Bound _ (* rigid atom *)  => true
    27   | Free  _ (* rigid atom *)  => true
    28   | _    (* flexible atom,
    29             anything else *)  => false
    30 and
    31     isG t = case t of
    32     Const(@{const_name Trueprop},_)$t     => isG t
    33   | Const(@{const_name HOL.conj}  ,_)$l$r     => isG l andalso isG r
    34   | Const(@{const_name HOL.disj}  ,_)$l$r     => isG l andalso isG r
    35   | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
    36   | Const(@{const_name Pure.imp},_)$l$r     => isD l andalso isG r
    37   | Const(@{const_name All},_)$Abs(_,_,t) => isG t
    38   | Const(@{const_name Pure.all},_)$Abs(_,_,t) => isG t
    39   | Const(@{const_name Ex} ,_)$Abs(_,_,t) => isG t
    40   | Const(@{const_name True},_)           => true
    41   | Const(@{const_name Not},_)$_          => false
    42   | Const(@{const_name False},_)          => false
    43   | _ (* atom *)              => true;
    44 
    45 val check_HOHH_tac1 = PRIMITIVE (fn thm =>
    46         if isG (Thm.concl_of thm) then thm else raise not_HOHH);
    47 val check_HOHH_tac2 = PRIMITIVE (fn thm =>
    48         if forall isG (Thm.prems_of thm) then thm else raise not_HOHH);
    49 fun check_HOHH thm  = (if isD (Thm.concl_of thm) andalso forall isG (Thm.prems_of thm)
    50                         then thm else raise not_HOHH);
    51 
    52 fun atomizeD ctxt thm =
    53   let
    54     fun at  thm = case Thm.concl_of thm of
    55       _$(Const(@{const_name All} ,_)$Abs(s,_,_))=>
    56         let val s' = if s="P" then "PP" else s in
    57           at(thm RS (Rule_Insts.read_instantiate ctxt [((("x", 0), Position.none), s')] [s'] spec))
    58         end
    59     | _$(Const(@{const_name HOL.conj},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    60     | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
    61     | _                             => [thm]
    62   in map zero_var_indexes (at thm) end;
    63 
    64 val atomize_ss =
    65   (empty_simpset @{context} |> Simplifier.set_mksimps (mksimps mksimps_pairs))
    66   addsimps [
    67         @{thm all_conj_distrib}, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    68         @{thm imp_conjL} RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    69         @{thm imp_conjR},        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    70         @{thm imp_all}]          (* "((!x. D) :- G) = (!x. D :- G)" *)
    71   |> simpset_of;
    72 
    73 
    74 (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} =>
    75                                   resolve_tac (maps atomizeD prems) 1);
    76   -- is nice, but cannot instantiate unknowns in the assumptions *)
    77 fun hyp_resolve_tac ctxt = SUBGOAL (fn (subgoal, i) =>
    78   let
    79         fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    80         |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    81         |   ap t                          =                         (0,false,t);
    82 (*
    83         fun rep_goal (Const (@{const_name Pure.all},_)$Abs (_,_,t)) = rep_goal t
    84         |   rep_goal (Const (@{const_name Pure.imp},_)$s$t)         =
    85                         (case rep_goal t of (l,t) => (s::l,t))
    86         |   rep_goal t                             = ([]  ,t);
    87         val (prems, Const(@{const_name Trueprop}, _)$concl) = rep_goal
    88                                                 (#3(dest_state (st,i)));
    89 *)
    90         val prems = Logic.strip_assums_hyp subgoal;
    91         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    92         fun drot_tac k i = DETERM (rotate_tac k i);
    93         fun spec_tac 0 i = all_tac
    94         |   spec_tac k i = EVERY' [dresolve_tac ctxt [spec], drot_tac ~1, spec_tac (k-1)] i;
    95         fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
    96                       [DETERM o (eresolve_tac ctxt [all_dupE]), drot_tac ~2, spec_tac (k-1)] i;
    97         fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
    98         |   same_head k (s$_)         (t$_)         = same_head k s t
    99         |   same_head k (Bound i)     (Bound j)     = i = j + k
   100         |   same_head _ _             _             = true;
   101         fun mapn f n []      = []
   102         |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
   103         fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
   104           if same_head k t concl
   105           then dup_spec_tac k i THEN
   106                (if arrow then eresolve_tac ctxt [mp] i THEN drot_tac (~n) i else assume_tac ctxt i)
   107           else no_tac);
   108         val ptacs = mapn (fn n => fn t =>
   109                           pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   110   in Library.foldl (op APPEND) (no_tac, ptacs) end);
   111 
   112 fun ptac ctxt prog = let
   113   val proga = maps (atomizeD ctxt) prog         (* atomize the prog *)
   114   in    (REPEAT_DETERM1 o FIRST' [
   115                 resolve_tac ctxt [TrueI],                     (* "True" *)
   116                 resolve_tac ctxt [conjI],                     (* "[| P; Q |] ==> P & Q" *)
   117                 resolve_tac ctxt [allI],                      (* "(!!x. P x) ==> ! x. P x" *)
   118                 resolve_tac ctxt [exI],                       (* "P x ==> ? x. P x" *)
   119                 resolve_tac ctxt [impI] THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   120                   asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN'    (* atomize the asms *)
   121                   (REPEAT_DETERM o (eresolve_tac ctxt [conjE]))        (* split the asms *)
   122                 ])
   123         ORELSE' resolve_tac ctxt [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
   124         ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac ctxt)
   125                  THEN' (fn _ => check_HOHH_tac2))
   126 end;
   127 
   128 fun prolog_tac ctxt prog =
   129   check_HOHH_tac1 THEN
   130   DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1);
   131 
   132 val prog_HOHH = [];
   133 
   134 end;