src/HOL/Prolog/prolog.ML
changeset 21425 c11ab38b78a7
child 27153 56b6cdce22f1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Prolog/prolog.ML	Mon Nov 20 21:23:12 2006 +0100
     1.3 @@ -0,0 +1,130 @@
     1.4 +(*  Title:    HOL/Prolog/prolog.ML
     1.5 +    ID:       $Id$
     1.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 +*)
     1.8 +
     1.9 +set Proof.show_main_goal;
    1.10 +
    1.11 +structure Prolog =
    1.12 +struct
    1.13 +
    1.14 +exception not_HOHH;
    1.15 +
    1.16 +fun isD t = case t of
    1.17 +    Const("Trueprop",_)$t     => isD t
    1.18 +  | Const("op &"  ,_)$l$r     => isD l andalso isD r
    1.19 +  | Const("op -->",_)$l$r     => isG l andalso isD r
    1.20 +  | Const(   "==>",_)$l$r     => isG l andalso isD r
    1.21 +  | Const("All",_)$Abs(s,_,t) => isD t
    1.22 +  | Const("all",_)$Abs(s,_,t) => isD t
    1.23 +  | Const("op |",_)$_$_       => false
    1.24 +  | Const("Ex" ,_)$_          => false
    1.25 +  | Const("not",_)$_          => false
    1.26 +  | Const("True",_)           => false
    1.27 +  | Const("False",_)          => false
    1.28 +  | l $ r                     => isD l
    1.29 +  | Const _ (* rigid atom *)  => true
    1.30 +  | Bound _ (* rigid atom *)  => true
    1.31 +  | Free  _ (* rigid atom *)  => true
    1.32 +  | _    (* flexible atom,
    1.33 +            anything else *)  => false
    1.34 +and
    1.35 +    isG t = case t of
    1.36 +    Const("Trueprop",_)$t     => isG t
    1.37 +  | Const("op &"  ,_)$l$r     => isG l andalso isG r
    1.38 +  | Const("op |"  ,_)$l$r     => isG l andalso isG r
    1.39 +  | Const("op -->",_)$l$r     => isD l andalso isG r
    1.40 +  | Const(   "==>",_)$l$r     => isD l andalso isG r
    1.41 +  | Const("All",_)$Abs(_,_,t) => isG t
    1.42 +  | Const("all",_)$Abs(_,_,t) => isG t
    1.43 +  | Const("Ex" ,_)$Abs(_,_,t) => isG t
    1.44 +  | Const("True",_)           => true
    1.45 +  | Const("not",_)$_          => false
    1.46 +  | Const("False",_)          => false
    1.47 +  | _ (* atom *)              => true;
    1.48 +
    1.49 +val check_HOHH_tac1 = PRIMITIVE (fn thm =>
    1.50 +        if isG (concl_of thm) then thm else raise not_HOHH);
    1.51 +val check_HOHH_tac2 = PRIMITIVE (fn thm =>
    1.52 +        if forall isG (prems_of thm) then thm else raise not_HOHH);
    1.53 +fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
    1.54 +                        then thm else raise not_HOHH);
    1.55 +
    1.56 +fun atomizeD thm = let
    1.57 +    fun at  thm = case concl_of thm of
    1.58 +      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
    1.59 +                                        "?"^(if s="P" then "PP" else s))] spec))
    1.60 +    | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    1.61 +    | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
    1.62 +    | _                             => [thm]
    1.63 +in map zero_var_indexes (at thm) end;
    1.64 +
    1.65 +val atomize_ss =
    1.66 +  Simplifier.theory_context (the_context ()) empty_ss
    1.67 +  setmksimps (mksimps mksimps_pairs)
    1.68 +  addsimps [
    1.69 +        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    1.70 +        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    1.71 +        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    1.72 +        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    1.73 +
    1.74 +(*val hyp_resolve_tac = METAHYPS (fn prems =>
    1.75 +                                  resolve_tac (List.concat (map atomizeD prems)) 1);
    1.76 +  -- is nice, but cannot instantiate unknowns in the assumptions *)
    1.77 +fun hyp_resolve_tac i st = let
    1.78 +        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    1.79 +        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    1.80 +        |   ap t                          =                         (0,false,t);
    1.81 +(*
    1.82 +        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    1.83 +        |   rep_goal (Const ("==>",_)$s$t)         =
    1.84 +                        (case rep_goal t of (l,t) => (s::l,t))
    1.85 +        |   rep_goal t                             = ([]  ,t);
    1.86 +        val (prems, Const("Trueprop", _)$concl) = rep_goal
    1.87 +                                                (#3(dest_state (st,i)));
    1.88 +*)
    1.89 +        val subgoal = #3(dest_state (st,i));
    1.90 +        val prems = Logic.strip_assums_hyp subgoal;
    1.91 +        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    1.92 +        fun drot_tac k i = DETERM (rotate_tac k i);
    1.93 +        fun spec_tac 0 i = all_tac
    1.94 +        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
    1.95 +        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
    1.96 +                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
    1.97 +        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
    1.98 +        |   same_head k (s$_)         (t$_)         = same_head k s t
    1.99 +        |   same_head k (Bound i)     (Bound j)     = i = j + k
   1.100 +        |   same_head _ _             _             = true;
   1.101 +        fun mapn f n []      = []
   1.102 +        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
   1.103 +        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
   1.104 +                if same_head k t concl
   1.105 +                then dup_spec_tac k i THEN
   1.106 +                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
   1.107 +                else no_tac);
   1.108 +        val ptacs = mapn (fn n => fn t =>
   1.109 +                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   1.110 +        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
   1.111 +
   1.112 +fun ptac prog = let
   1.113 +  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
   1.114 +  in    (REPEAT_DETERM1 o FIRST' [
   1.115 +                rtac TrueI,                     (* "True" *)
   1.116 +                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
   1.117 +                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
   1.118 +                rtac exI,                       (* "P x ==> ? x. P x" *)
   1.119 +                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   1.120 +                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
   1.121 +                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
   1.122 +                ])
   1.123 +        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
   1.124 +        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
   1.125 +                 THEN' (fn _ => check_HOHH_tac2))
   1.126 +end;
   1.127 +
   1.128 +fun prolog_tac prog = check_HOHH_tac1 THEN
   1.129 +                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
   1.130 +
   1.131 +val prog_HOHH = [];
   1.132 +
   1.133 +end;