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