src/HOL/Prolog/prolog.ML
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27239 f2f42f9fa09d
child 32010 cb1a1c94b4cd
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (*  Title:    HOL/Prolog/prolog.ML
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4 *)
     5 
     6 set Proof.show_main_goal;
     7 
     8 structure Prolog =
     9 struct
    10 
    11 exception not_HOHH;
    12 
    13 fun isD t = case t of
    14     Const("Trueprop",_)$t     => isD t
    15   | Const("op &"  ,_)$l$r     => isD l andalso isD r
    16   | Const("op -->",_)$l$r     => isG l andalso isD r
    17   | Const(   "==>",_)$l$r     => isG l andalso isD r
    18   | Const("All",_)$Abs(s,_,t) => isD t
    19   | Const("all",_)$Abs(s,_,t) => isD t
    20   | Const("op |",_)$_$_       => false
    21   | Const("Ex" ,_)$_          => false
    22   | Const("not",_)$_          => false
    23   | Const("True",_)           => false
    24   | Const("False",_)          => false
    25   | l $ r                     => isD l
    26   | Const _ (* rigid atom *)  => true
    27   | Bound _ (* rigid atom *)  => true
    28   | Free  _ (* rigid atom *)  => true
    29   | _    (* flexible atom,
    30             anything else *)  => false
    31 and
    32     isG t = case t of
    33     Const("Trueprop",_)$t     => isG t
    34   | Const("op &"  ,_)$l$r     => isG l andalso isG r
    35   | Const("op |"  ,_)$l$r     => isG l andalso isG r
    36   | Const("op -->",_)$l$r     => isD l andalso isG r
    37   | Const(   "==>",_)$l$r     => isD l andalso isG r
    38   | Const("All",_)$Abs(_,_,t) => isG t
    39   | Const("all",_)$Abs(_,_,t) => isG t
    40   | Const("Ex" ,_)$Abs(_,_,t) => isG t
    41   | Const("True",_)           => true
    42   | Const("not",_)$_          => false
    43   | Const("False",_)          => false
    44   | _ (* atom *)              => true;
    45 
    46 val check_HOHH_tac1 = PRIMITIVE (fn thm =>
    47         if isG (concl_of thm) then thm else raise not_HOHH);
    48 val check_HOHH_tac2 = PRIMITIVE (fn thm =>
    49         if forall isG (prems_of thm) then thm else raise not_HOHH);
    50 fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
    51                         then thm else raise not_HOHH);
    52 
    53 fun atomizeD ctxt thm = let
    54     fun at  thm = case concl_of thm of
    55       _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS
    56         (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
    57     | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    58     | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
    59     | _                             => [thm]
    60 in map zero_var_indexes (at thm) end;
    61 
    62 val atomize_ss =
    63   Simplifier.theory_context (the_context ()) empty_ss
    64   setmksimps (mksimps mksimps_pairs)
    65   addsimps [
    66         all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    67         imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    68         imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    69         imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    70 
    71 (*val hyp_resolve_tac = METAHYPS (fn prems =>
    72                                   resolve_tac (List.concat (map atomizeD prems)) 1);
    73   -- is nice, but cannot instantiate unknowns in the assumptions *)
    74 fun hyp_resolve_tac i st = let
    75         fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    76         |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    77         |   ap t                          =                         (0,false,t);
    78 (*
    79         fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    80         |   rep_goal (Const ("==>",_)$s$t)         =
    81                         (case rep_goal t of (l,t) => (s::l,t))
    82         |   rep_goal t                             = ([]  ,t);
    83         val (prems, Const("Trueprop", _)$concl) = rep_goal
    84                                                 (#3(dest_state (st,i)));
    85 *)
    86         val subgoal = #3(dest_state (st,i));
    87         val prems = Logic.strip_assums_hyp subgoal;
    88         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    89         fun drot_tac k i = DETERM (rotate_tac k i);
    90         fun spec_tac 0 i = all_tac
    91         |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
    92         fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
    93                       [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
    94         fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
    95         |   same_head k (s$_)         (t$_)         = same_head k s t
    96         |   same_head k (Bound i)     (Bound j)     = i = j + k
    97         |   same_head _ _             _             = true;
    98         fun mapn f n []      = []
    99         |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
   100         fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
   101                 if same_head k t concl
   102                 then dup_spec_tac k i THEN
   103                      (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
   104                 else no_tac);
   105         val ptacs = mapn (fn n => fn t =>
   106                           pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   107         in Library.foldl (op APPEND) (no_tac, ptacs) st end;
   108 
   109 fun ptac ctxt prog = let
   110   val proga = List.concat (map (atomizeD ctxt) prog)                   (* atomize the prog *)
   111   in    (REPEAT_DETERM1 o FIRST' [
   112                 rtac TrueI,                     (* "True" *)
   113                 rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
   114                 rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
   115                 rtac exI,                       (* "P x ==> ? x. P x" *)
   116                 rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   117                   asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
   118                   (REPEAT_DETERM o (etac conjE))        (* split the asms *)
   119                 ])
   120         ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
   121         ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
   122                  THEN' (fn _ => check_HOHH_tac2))
   123 end;
   124 
   125 fun prolog_tac ctxt prog =
   126   check_HOHH_tac1 THEN
   127   DEPTH_SOLVE (ptac ctxt (map check_HOHH prog) 1);
   128 
   129 val prog_HOHH = [];
   130 
   131 end;