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