HOL-Prolog: converted legacy ML scripts;
authorwenzelm
Mon Nov 20 21:23:12 2006 +0100 (2006-11-20)
changeset 21425c11ab38b78a7
parent 21424 5295ffa18285
child 21426 87ac12bed1ab
HOL-Prolog: converted legacy ML scripts;
src/HOL/IsaMakefile
src/HOL/Prolog/Func.ML
src/HOL/Prolog/Func.thy
src/HOL/Prolog/HOHH.ML
src/HOL/Prolog/HOHH.thy
src/HOL/Prolog/Test.ML
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.ML
src/HOL/Prolog/Type.thy
src/HOL/Prolog/prolog.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Nov 20 21:23:12 2006 +0100
     1.3 @@ -499,9 +499,8 @@
     1.4  
     1.5  HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
     1.6  
     1.7 -$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/HOHH.ML Prolog/HOHH.thy \
     1.8 -  Prolog/Test.ML Prolog/Test.thy  \
     1.9 -  Prolog/Func.ML Prolog/Func.thy Prolog/Type.ML Prolog/Type.thy
    1.10 +$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML Prolog/HOHH.thy \
    1.11 +  Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
    1.12  	@$(ISATOOL) usedir $(OUT)/HOL Prolog
    1.13  
    1.14  
     2.1 --- a/src/HOL/Prolog/Func.ML	Mon Nov 20 11:51:10 2006 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,13 +0,0 @@
     2.4 -(* Title:    HOL/Prolog/Func.ML
     2.5 -    ID:       $Id$
     2.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     2.7 -*)
     2.8 -
     2.9 -val prog_Func = prog_HOHH @ [eval];
    2.10 -fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
    2.11 -val p = ptac prog_Func 1;
    2.12 -
    2.13 -pgoal "eval ((S (S Z)) + (S Z)) ?X";
    2.14 -
    2.15 -pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
    2.16 -                        \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
     3.1 --- a/src/HOL/Prolog/Func.thy	Mon Nov 20 11:51:10 2006 +0100
     3.2 +++ b/src/HOL/Prolog/Func.thy	Mon Nov 20 21:23:12 2006 +0100
     3.3 @@ -20,8 +20,8 @@
     3.4  
     3.5    true    :: tm
     3.6    false   :: tm
     3.7 -  "and"   :: "tm => tm => tm"       (infixr 999)
     3.8 -  "eq"    :: "tm => tm => tm"       (infixr 999)
     3.9 +  "and"   :: "tm => tm => tm"       (infixr "and" 999)
    3.10 +  eq      :: "tm => tm => tm"       (infixr "eq" 999)
    3.11  
    3.12    Z       :: tm                     ("Z")
    3.13    S       :: "tm => tm"
    3.14 @@ -60,6 +60,16 @@
    3.15  eval ( Z    * M) Z..
    3.16  eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
    3.17  
    3.18 -ML {* use_legacy_bindings (the_context ()) *}
    3.19 +
    3.20 +lemmas prog_Func = eval
    3.21 +
    3.22 +lemma "eval ((S (S Z)) + (S Z)) ?X"
    3.23 +  apply (prolog prog_Func)
    3.24 +  done
    3.25 +
    3.26 +lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    3.27 +                        (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
    3.28 +  apply (prolog prog_Func)
    3.29 +  done
    3.30  
    3.31  end
     4.1 --- a/src/HOL/Prolog/HOHH.ML	Mon Nov 20 11:51:10 2006 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,123 +0,0 @@
     4.4 -(*  Title:    HOL/Prolog/HOHH.ML
     4.5 -    ID:       $Id$
     4.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4.7 -*)
     4.8 -
     4.9 -exception not_HOHH;
    4.10 -
    4.11 -fun isD t = case t of
    4.12 -    Const("Trueprop",_)$t     => isD t
    4.13 -  | Const("op &"  ,_)$l$r     => isD l andalso isD r
    4.14 -  | Const("op -->",_)$l$r     => isG l andalso isD r
    4.15 -  | Const(   "==>",_)$l$r     => isG l andalso isD r
    4.16 -  | Const("All",_)$Abs(s,_,t) => isD t
    4.17 -  | Const("all",_)$Abs(s,_,t) => isD t
    4.18 -  | Const("op |",_)$_$_       => false
    4.19 -  | Const("Ex" ,_)$_          => false
    4.20 -  | Const("not",_)$_          => false
    4.21 -  | Const("True",_)           => false
    4.22 -  | Const("False",_)          => false
    4.23 -  | l $ r                     => isD l
    4.24 -  | Const _ (* rigid atom *)  => true
    4.25 -  | Bound _ (* rigid atom *)  => true
    4.26 -  | Free  _ (* rigid atom *)  => true
    4.27 -  | _    (* flexible atom,
    4.28 -            anything else *)  => false
    4.29 -and
    4.30 -    isG t = case t of
    4.31 -    Const("Trueprop",_)$t     => isG t
    4.32 -  | Const("op &"  ,_)$l$r     => isG l andalso isG r
    4.33 -  | Const("op |"  ,_)$l$r     => isG l andalso isG r
    4.34 -  | Const("op -->",_)$l$r     => isD l andalso isG r
    4.35 -  | Const(   "==>",_)$l$r     => isD l andalso isG r
    4.36 -  | Const("All",_)$Abs(_,_,t) => isG t
    4.37 -  | Const("all",_)$Abs(_,_,t) => isG t
    4.38 -  | Const("Ex" ,_)$Abs(_,_,t) => isG t
    4.39 -  | Const("True",_)           => true
    4.40 -  | Const("not",_)$_          => false
    4.41 -  | Const("False",_)          => false
    4.42 -  | _ (* atom *)              => true;
    4.43 -
    4.44 -val check_HOHH_tac1 = PRIMITIVE (fn thm =>
    4.45 -        if isG (concl_of thm) then thm else raise not_HOHH);
    4.46 -val check_HOHH_tac2 = PRIMITIVE (fn thm =>
    4.47 -        if forall isG (prems_of thm) then thm else raise not_HOHH);
    4.48 -fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
    4.49 -                        then thm else raise not_HOHH);
    4.50 -
    4.51 -fun atomizeD thm = let
    4.52 -    fun at  thm = case concl_of thm of
    4.53 -      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
    4.54 -                                        "?"^(if s="P" then "PP" else s))] spec))
    4.55 -    | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    4.56 -    | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
    4.57 -    | _                             => [thm]
    4.58 -in map zero_var_indexes (at thm) end;
    4.59 -
    4.60 -val atomize_ss =
    4.61 -  Simplifier.theory_context (the_context ()) empty_ss
    4.62 -  setmksimps (mksimps mksimps_pairs)
    4.63 -  addsimps [
    4.64 -        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    4.65 -        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    4.66 -        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
    4.67 -        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
    4.68 -
    4.69 -(*val hyp_resolve_tac = METAHYPS (fn prems =>
    4.70 -                                  resolve_tac (List.concat (map atomizeD prems)) 1);
    4.71 -  -- is nice, but cannot instantiate unknowns in the assumptions *)
    4.72 -fun hyp_resolve_tac i st = let
    4.73 -        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    4.74 -        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    4.75 -        |   ap t                          =                         (0,false,t);
    4.76 -(*
    4.77 -        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
    4.78 -        |   rep_goal (Const ("==>",_)$s$t)         =
    4.79 -                        (case rep_goal t of (l,t) => (s::l,t))
    4.80 -        |   rep_goal t                             = ([]  ,t);
    4.81 -        val (prems, Const("Trueprop", _)$concl) = rep_goal
    4.82 -                                                (#3(dest_state (st,i)));
    4.83 -*)
    4.84 -        val subgoal = #3(dest_state (st,i));
    4.85 -        val prems = Logic.strip_assums_hyp subgoal;
    4.86 -        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
    4.87 -        fun drot_tac k i = DETERM (rotate_tac k i);
    4.88 -        fun spec_tac 0 i = all_tac
    4.89 -        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
    4.90 -        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
    4.91 -                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
    4.92 -        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
    4.93 -        |   same_head k (s$_)         (t$_)         = same_head k s t
    4.94 -        |   same_head k (Bound i)     (Bound j)     = i = j + k
    4.95 -        |   same_head _ _             _             = true;
    4.96 -        fun mapn f n []      = []
    4.97 -        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
    4.98 -        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
    4.99 -                if same_head k t concl
   4.100 -                then dup_spec_tac k i THEN
   4.101 -                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
   4.102 -                else no_tac);
   4.103 -        val ptacs = mapn (fn n => fn t =>
   4.104 -                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
   4.105 -        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
   4.106 -
   4.107 -fun ptac prog = let
   4.108 -  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
   4.109 -  in    (REPEAT_DETERM1 o FIRST' [
   4.110 -                rtac TrueI,                     (* "True" *)
   4.111 -                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
   4.112 -                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
   4.113 -                rtac exI,                       (* "P x ==> ? x. P x" *)
   4.114 -                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
   4.115 -                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
   4.116 -                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
   4.117 -                ])
   4.118 -        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
   4.119 -        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
   4.120 -                 THEN' (fn _ => check_HOHH_tac2))
   4.121 -end;
   4.122 -
   4.123 -fun prolog_tac prog = check_HOHH_tac1 THEN
   4.124 -                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
   4.125 -
   4.126 -val prog_HOHH = [];
     5.1 --- a/src/HOL/Prolog/HOHH.thy	Mon Nov 20 11:51:10 2006 +0100
     5.2 +++ b/src/HOL/Prolog/HOHH.thy	Mon Nov 20 21:23:12 2006 +0100
     5.3 @@ -7,18 +7,27 @@
     5.4  
     5.5  theory HOHH
     5.6  imports HOL
     5.7 +uses "prolog.ML"
     5.8  begin
     5.9  
    5.10 +method_setup ptac =
    5.11 +  {* Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o Prolog.ptac) *}
    5.12 +  "Basic Lambda Prolog interpreter"
    5.13 +
    5.14 +method_setup prolog =
    5.15 +  {* Method.thms_args (Method.SIMPLE_METHOD o Prolog.prolog_tac) *}
    5.16 +  "Lambda Prolog interpreter"
    5.17 +
    5.18  consts
    5.19  
    5.20  (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
    5.21 -  "Dand"        :: "[bool, bool] => bool"         (infixr ".." 28)
    5.22 -  ":-"          :: "[bool, bool] => bool"         (infixl 29)
    5.23 +  Dand        :: "[bool, bool] => bool"         (infixr ".." 28)
    5.24 +  Dif        :: "[bool, bool] => bool"         (infixl ":-" 29)
    5.25  
    5.26  (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
    5.27                                 | True | !x. G | D => G                  *)
    5.28 -(*","           :: "[bool, bool] => bool"         (infixr 35)*)
    5.29 -  "=>"          :: "[bool, bool] => bool"         (infixr 27)
    5.30 +(*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
    5.31 +  Dimp          :: "[bool, bool] => bool"         (infixr "=>" 27)
    5.32  
    5.33  translations
    5.34  
     6.1 --- a/src/HOL/Prolog/Test.ML	Mon Nov 20 11:51:10 2006 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,145 +0,0 @@
     6.4 -(*  Title:    HOL/Prolog/Test.ML
     6.5 -    ID:       $Id$
     6.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     6.7 -*)
     6.8 -
     6.9 -val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
    6.10 -fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
    6.11 -val p = ptac prog_Test 1;
    6.12 -
    6.13 -pgoal "append ?x ?y [a,b,c,d]";
    6.14 -back();
    6.15 -back();
    6.16 -back();
    6.17 -back();
    6.18 -
    6.19 -pgoal "append [a,b] y ?L";
    6.20 -pgoal "!y. append [a,b] y (?L y)";
    6.21 -
    6.22 -pgoal "reverse [] ?L";
    6.23 -
    6.24 -pgoal "reverse [23] ?L";
    6.25 -pgoal "reverse [23,24,?x] ?L";
    6.26 -pgoal "reverse ?L [23,24,?x]";
    6.27 -
    6.28 -pgoal "mappred age ?x [23,24]";
    6.29 -back();
    6.30 -
    6.31 -pgoal "mappred (%x y. ? z. age z y) ?x [23,24]";
    6.32 -
    6.33 -pgoal "mappred ?P [bob,sue] [24,23]";
    6.34 -
    6.35 -pgoal "mapfun f [bob,bob,sue] [?x,?y,?z]";
    6.36 -
    6.37 -pgoal "mapfun (%x. h x 25) [bob,sue] ?L";
    6.38 -
    6.39 -pgoal "mapfun ?F [24,25] [h bob 24,h bob 25]";
    6.40 -
    6.41 -pgoal "mapfun ?F [24] [h 24 24]";
    6.42 -back();
    6.43 -back();
    6.44 -back();
    6.45 -
    6.46 -
    6.47 -(*
    6.48 -goal (the_context ()) "f a = ?g a a & ?g = x";
    6.49 -by (rtac conjI 1);
    6.50 -by (rtac refl 1);
    6.51 -back();
    6.52 -back();
    6.53 -*)
    6.54 -
    6.55 -pgoal "True";
    6.56 -
    6.57 -pgoal "age ?x 24 & age ?y 23";
    6.58 -back();
    6.59 -
    6.60 -pgoal "age ?x 24 | age ?x 23";
    6.61 -back();
    6.62 -back();
    6.63 -
    6.64 -pgoal "? x y. age x y";
    6.65 -
    6.66 -pgoal "!x y. append [] x x";
    6.67 -
    6.68 -pgoal "age sue 24 .. age bob 23 => age ?x ?y";
    6.69 -back();
    6.70 -back();
    6.71 -back();
    6.72 -back();
    6.73 -
    6.74 -(*set trace_DEPTH_FIRST;*)
    6.75 -pgoal "age bob 25 :- age bob 24 => age bob 25";
    6.76 -(*reset trace_DEPTH_FIRST;*)
    6.77 -
    6.78 -pgoal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25";
    6.79 -back();
    6.80 -back();
    6.81 -back();
    6.82 -
    6.83 -pgoal "!x. ? y. eq x y";
    6.84 -
    6.85 -pgoal "? P. P & eq P ?x";
    6.86 -(*
    6.87 -back();
    6.88 -back();
    6.89 -back();
    6.90 -back();
    6.91 -back();
    6.92 -back();
    6.93 -back();
    6.94 -back();
    6.95 -*)
    6.96 -
    6.97 -pgoal "? P. eq P (True & True) & P";
    6.98 -
    6.99 -pgoal "? P. eq P op | & P k True";
   6.100 -
   6.101 -pgoal "? P. eq P (Q => True) & P";
   6.102 -
   6.103 -(* P flexible: *)
   6.104 -pgoal "(!P k l. P k l :- eq P Q) => Q a b";
   6.105 -(*
   6.106 -loops:
   6.107 -pgoal "(!P k l. P k l :- eq P (%x y. x | y)) => a | b";
   6.108 -*)
   6.109 -
   6.110 -(* implication and disjunction in atom: *)
   6.111 -goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
   6.112 -by (fast_tac HOL_cs 1);
   6.113 -
   6.114 -(* disjunction in atom: *)
   6.115 -goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
   6.116 -by (step_tac HOL_cs 1);
   6.117 -by (step_tac HOL_cs 1);
   6.118 -by (step_tac HOL_cs 1);
   6.119 -by (fast_tac HOL_cs 2);
   6.120 -by (fast_tac HOL_cs 1);
   6.121 -(*
   6.122 -hangs:
   6.123 -goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
   6.124 -by (fast_tac HOL_cs 1);
   6.125 -*)
   6.126 -
   6.127 -pgoal "!Emp Stk.(\
   6.128 -\                       empty    (Emp::'b) .. \
   6.129 -\         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. \
   6.130 -\         (!(X::nat) S. remove X ((Stk X S)::'b) S))\
   6.131 -\ => bag_appl 23 24 ?X ?Y";
   6.132 -
   6.133 -pgoal "!Qu. ( \
   6.134 -\          (!L.            empty    (Qu L L)) .. \
   6.135 -\          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..\
   6.136 -\          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))\
   6.137 -\ => bag_appl 23 24 ?X ?Y";
   6.138 -
   6.139 -pgoal "D & (!y. E) :- (!x. True & True) :- True => D";
   6.140 -
   6.141 -pgoal "P x .. P y => P ?X";
   6.142 -back();
   6.143 -(*
   6.144 -back();
   6.145 --> problem with DEPTH_SOLVE:
   6.146 -Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
   6.147 -Exception raised at run-time
   6.148 -*)
     7.1 --- a/src/HOL/Prolog/Test.thy	Mon Nov 20 11:51:10 2006 +0100
     7.2 +++ b/src/HOL/Prolog/Test.thy	Mon Nov 20 21:23:12 2006 +0100
     7.3 @@ -80,6 +80,202 @@
     7.4                                  remove Y S4 S5 &
     7.5                                  empty    S5)"
     7.6  
     7.7 -ML {* use_legacy_bindings (the_context ()) *}
     7.8 +lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
     7.9 +
    7.10 +lemma "append ?x ?y [a,b,c,d]"
    7.11 +  apply (prolog prog_Test)
    7.12 +  back
    7.13 +  back
    7.14 +  back
    7.15 +  back
    7.16 +  done
    7.17 +
    7.18 +lemma "append [a,b] y ?L"
    7.19 +  apply (prolog prog_Test)
    7.20 +  done
    7.21 +
    7.22 +lemma "!y. append [a,b] y (?L y)"
    7.23 +  apply (prolog prog_Test)
    7.24 +  done
    7.25 +
    7.26 +lemma "reverse [] ?L"
    7.27 +  apply (prolog prog_Test)
    7.28 +  done
    7.29 +
    7.30 +lemma "reverse [23] ?L"
    7.31 +  apply (prolog prog_Test)
    7.32 +  done
    7.33 +
    7.34 +lemma "reverse [23,24,?x] ?L"
    7.35 +  apply (prolog prog_Test)
    7.36 +  done
    7.37 +
    7.38 +lemma "reverse ?L [23,24,?x]"
    7.39 +  apply (prolog prog_Test)
    7.40 +  done
    7.41 +
    7.42 +lemma "mappred age ?x [23,24]"
    7.43 +  apply (prolog prog_Test)
    7.44 +  back
    7.45 +  done
    7.46 +
    7.47 +lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
    7.48 +  apply (prolog prog_Test)
    7.49 +  done
    7.50 +
    7.51 +lemma "mappred ?P [bob,sue] [24,23]"
    7.52 +  apply (prolog prog_Test)
    7.53 +  done
    7.54 +
    7.55 +lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
    7.56 +  apply (prolog prog_Test)
    7.57 +  done
    7.58 +
    7.59 +lemma "mapfun (%x. h x 25) [bob,sue] ?L"
    7.60 +  apply (prolog prog_Test)
    7.61 +  done
    7.62 +
    7.63 +lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
    7.64 +  apply (prolog prog_Test)
    7.65 +  done
    7.66 +
    7.67 +lemma "mapfun ?F [24] [h 24 24]"
    7.68 +  apply (prolog prog_Test)
    7.69 +  back
    7.70 +  back
    7.71 +  back
    7.72 +  done
    7.73 +
    7.74 +lemma "True"
    7.75 +  apply (prolog prog_Test)
    7.76 +  done
    7.77 +
    7.78 +lemma "age ?x 24 & age ?y 23"
    7.79 +  apply (prolog prog_Test)
    7.80 +  back
    7.81 +  done
    7.82 +
    7.83 +lemma "age ?x 24 | age ?x 23"
    7.84 +  apply (prolog prog_Test)
    7.85 +  back
    7.86 +  back
    7.87 +  done
    7.88 +
    7.89 +lemma "? x y. age x y"
    7.90 +  apply (prolog prog_Test)
    7.91 +  done
    7.92 +
    7.93 +lemma "!x y. append [] x x"
    7.94 +  apply (prolog prog_Test)
    7.95 +  done
    7.96 +
    7.97 +lemma "age sue 24 .. age bob 23 => age ?x ?y"
    7.98 +  apply (prolog prog_Test)
    7.99 +  back
   7.100 +  back
   7.101 +  back
   7.102 +  back
   7.103 +  done
   7.104 +
   7.105 +(*set trace_DEPTH_FIRST;*)
   7.106 +lemma "age bob 25 :- age bob 24 => age bob 25"
   7.107 +  apply (prolog prog_Test)
   7.108 +  done
   7.109 +(*reset trace_DEPTH_FIRST;*)
   7.110 +
   7.111 +lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
   7.112 +  apply (prolog prog_Test)
   7.113 +  back
   7.114 +  back
   7.115 +  back
   7.116 +  done
   7.117 +
   7.118 +lemma "!x. ? y. eq x y"
   7.119 +  apply (prolog prog_Test)
   7.120 +  done
   7.121 +
   7.122 +lemma "? P. P & eq P ?x"
   7.123 +  apply (prolog prog_Test)
   7.124 +(*
   7.125 +  back
   7.126 +  back
   7.127 +  back
   7.128 +  back
   7.129 +  back
   7.130 +  back
   7.131 +  back
   7.132 +  back
   7.133 +*)
   7.134 +  done
   7.135 +
   7.136 +lemma "? P. eq P (True & True) & P"
   7.137 +  apply (prolog prog_Test)
   7.138 +  done
   7.139 +
   7.140 +lemma "? P. eq P op | & P k True"
   7.141 +  apply (prolog prog_Test)
   7.142 +  done
   7.143 +
   7.144 +lemma "? P. eq P (Q => True) & P"
   7.145 +  apply (prolog prog_Test)
   7.146 +  done
   7.147 +
   7.148 +(* P flexible: *)
   7.149 +lemma "(!P k l. P k l :- eq P Q) => Q a b"
   7.150 +  apply (prolog prog_Test)
   7.151 +  done
   7.152 +(*
   7.153 +loops:
   7.154 +lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
   7.155 +*)
   7.156 +
   7.157 +(* implication and disjunction in atom: *)
   7.158 +lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"
   7.159 +  by fast
   7.160 +
   7.161 +(* disjunction in atom: *)
   7.162 +lemma "(!P. g P :- (P => b | a)) => g(a | b)"
   7.163 +  apply (tactic "step_tac HOL_cs 1")
   7.164 +  apply (tactic "step_tac HOL_cs 1")
   7.165 +  apply (tactic "step_tac HOL_cs 1")
   7.166 +   prefer 2
   7.167 +   apply fast
   7.168 +  apply fast
   7.169 +  done
   7.170 +
   7.171 +(*
   7.172 +hangs:
   7.173 +lemma "(!P. g P :- (P => b | a)) => g(a | b)"
   7.174 +  by fast
   7.175 +*)
   7.176 +
   7.177 +lemma "!Emp Stk.(
   7.178 +                       empty    (Emp::'b) .. 
   7.179 +         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
   7.180 +         (!(X::nat) S. remove X ((Stk X S)::'b) S))
   7.181 + => bag_appl 23 24 ?X ?Y"
   7.182 +  oops
   7.183 +
   7.184 +lemma "!Qu. ( 
   7.185 +          (!L.            empty    (Qu L L)) .. 
   7.186 +          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
   7.187 +          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
   7.188 + => bag_appl 23 24 ?X ?Y"
   7.189 +  oops
   7.190 +
   7.191 +lemma "D & (!y. E) :- (!x. True & True) :- True => D"
   7.192 +  apply (prolog prog_Test)
   7.193 +  done
   7.194 +
   7.195 +lemma "P x .. P y => P ?X"
   7.196 +  apply (prolog prog_Test)
   7.197 +  back
   7.198 +  done
   7.199 +(*
   7.200 +back
   7.201 +-> problem with DEPTH_SOLVE:
   7.202 +Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
   7.203 +Exception raised at run-time
   7.204 +*)
   7.205  
   7.206  end
     8.1 --- a/src/HOL/Prolog/Type.ML	Mon Nov 20 11:51:10 2006 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,27 +0,0 @@
     8.4 -(*  Title:    HOL/Prolog/Type.ML
     8.5 -    ID:       $Id$
     8.6 -    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     8.7 -*)
     8.8 -
     8.9 -val prog_Type = prog_Func @ [good_typeof,common_typeof];
    8.10 -fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
    8.11 -val p = ptac prog_Type 1;
    8.12 -
    8.13 -pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
    8.14 -
    8.15 -pgoal "typeof (fix (%x. x)) ?T";
    8.16 -
    8.17 -pgoal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T";
    8.18 -
    8.19 -pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
    8.20 -  \(n * (app fact (n - (S Z))))))) ?T";
    8.21 -
    8.22 -pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
    8.23 -Goal "typeof (abs(%v. Z)) ?T";
    8.24 -by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
    8.25 -back(); (* 2nd result (?A1 -> ?A1) wrong *)
    8.26 -
    8.27 -(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
    8.28 -Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
    8.29 -by (prolog_tac [bad2_typeof,common_typeof]); 
    8.30 -	(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
     9.1 --- a/src/HOL/Prolog/Type.thy	Mon Nov 20 11:51:10 2006 +0100
     9.2 +++ b/src/HOL/Prolog/Type.thy	Mon Nov 20 21:23:12 2006 +0100
     9.3 @@ -14,7 +14,7 @@
     9.4  consts
     9.5    bool    :: ty
     9.6    nat     :: ty
     9.7 -  "->"    :: "ty => ty => ty"       (infixr 20)
     9.8 +  arrow   :: "ty => ty => ty"       (infixr "->" 20)
     9.9    typeof  :: "[tm, ty] => bool"
    9.10    anyterm :: tm
    9.11  
    9.12 @@ -45,6 +45,45 @@
    9.13  axioms bad2_typeof:     "
    9.14  typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
    9.15  
    9.16 -ML {* use_legacy_bindings (the_context ()) *}
    9.17 +
    9.18 +lemmas prog_Type = prog_Func good_typeof common_typeof
    9.19 +
    9.20 +lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
    9.21 +  apply (prolog prog_Type)
    9.22 +  done
    9.23 +
    9.24 +lemma "typeof (fix (%x. x)) ?T"
    9.25 +  apply (prolog prog_Type)
    9.26 +  done
    9.27 +
    9.28 +lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
    9.29 +  apply (prolog prog_Type)
    9.30 +  done
    9.31 +
    9.32 +lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    9.33 +  (n * (app fact (n - (S Z))))))) ?T"
    9.34 +  apply (prolog prog_Type)
    9.35 +  done
    9.36 +
    9.37 +lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
    9.38 +  apply (prolog prog_Type)
    9.39 +  done
    9.40 +
    9.41 +lemma "typeof (abs(%v. Z)) ?T"
    9.42 +  apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
    9.43 +  done
    9.44 +
    9.45 +lemma "typeof (abs(%v. Z)) ?T"
    9.46 +  apply (prolog bad1_typeof common_typeof)
    9.47 +  back (* 2nd result (?A1 -> ?A1) wrong *)
    9.48 +  done
    9.49 +
    9.50 +lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
    9.51 +  apply (prolog prog_Type)?  (*correctly fails*)
    9.52 +  oops
    9.53 +
    9.54 +lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
    9.55 +  apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
    9.56 +  done
    9.57  
    9.58  end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Prolog/prolog.ML	Mon Nov 20 21:23:12 2006 +0100
    10.3 @@ -0,0 +1,130 @@
    10.4 +(*  Title:    HOL/Prolog/prolog.ML
    10.5 +    ID:       $Id$
    10.6 +    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    10.7 +*)
    10.8 +
    10.9 +set Proof.show_main_goal;
   10.10 +
   10.11 +structure Prolog =
   10.12 +struct
   10.13 +
   10.14 +exception not_HOHH;
   10.15 +
   10.16 +fun isD t = case t of
   10.17 +    Const("Trueprop",_)$t     => isD t
   10.18 +  | Const("op &"  ,_)$l$r     => isD l andalso isD r
   10.19 +  | Const("op -->",_)$l$r     => isG l andalso isD r
   10.20 +  | Const(   "==>",_)$l$r     => isG l andalso isD r
   10.21 +  | Const("All",_)$Abs(s,_,t) => isD t
   10.22 +  | Const("all",_)$Abs(s,_,t) => isD t
   10.23 +  | Const("op |",_)$_$_       => false
   10.24 +  | Const("Ex" ,_)$_          => false
   10.25 +  | Const("not",_)$_          => false
   10.26 +  | Const("True",_)           => false
   10.27 +  | Const("False",_)          => false
   10.28 +  | l $ r                     => isD l
   10.29 +  | Const _ (* rigid atom *)  => true
   10.30 +  | Bound _ (* rigid atom *)  => true
   10.31 +  | Free  _ (* rigid atom *)  => true
   10.32 +  | _    (* flexible atom,
   10.33 +            anything else *)  => false
   10.34 +and
   10.35 +    isG t = case t of
   10.36 +    Const("Trueprop",_)$t     => isG t
   10.37 +  | Const("op &"  ,_)$l$r     => isG l andalso isG r
   10.38 +  | Const("op |"  ,_)$l$r     => isG l andalso isG r
   10.39 +  | Const("op -->",_)$l$r     => isD l andalso isG r
   10.40 +  | Const(   "==>",_)$l$r     => isD l andalso isG r
   10.41 +  | Const("All",_)$Abs(_,_,t) => isG t
   10.42 +  | Const("all",_)$Abs(_,_,t) => isG t
   10.43 +  | Const("Ex" ,_)$Abs(_,_,t) => isG t
   10.44 +  | Const("True",_)           => true
   10.45 +  | Const("not",_)$_          => false
   10.46 +  | Const("False",_)          => false
   10.47 +  | _ (* atom *)              => true;
   10.48 +
   10.49 +val check_HOHH_tac1 = PRIMITIVE (fn thm =>
   10.50 +        if isG (concl_of thm) then thm else raise not_HOHH);
   10.51 +val check_HOHH_tac2 = PRIMITIVE (fn thm =>
   10.52 +        if forall isG (prems_of thm) then thm else raise not_HOHH);
   10.53 +fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
   10.54 +                        then thm else raise not_HOHH);
   10.55 +
   10.56 +fun atomizeD thm = let
   10.57 +    fun at  thm = case concl_of thm of
   10.58 +      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
   10.59 +                                        "?"^(if s="P" then "PP" else s))] spec))
   10.60 +    | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
   10.61 +    | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
   10.62 +    | _                             => [thm]
   10.63 +in map zero_var_indexes (at thm) end;
   10.64 +
   10.65 +val atomize_ss =
   10.66 +  Simplifier.theory_context (the_context ()) empty_ss
   10.67 +  setmksimps (mksimps mksimps_pairs)
   10.68 +  addsimps [
   10.69 +        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
   10.70 +        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
   10.71 +        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
   10.72 +        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
   10.73 +
   10.74 +(*val hyp_resolve_tac = METAHYPS (fn prems =>
   10.75 +                                  resolve_tac (List.concat (map atomizeD prems)) 1);
   10.76 +  -- is nice, but cannot instantiate unknowns in the assumptions *)
   10.77 +fun hyp_resolve_tac i st = let
   10.78 +        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
   10.79 +        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
   10.80 +        |   ap t                          =                         (0,false,t);
   10.81 +(*
   10.82 +        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
   10.83 +        |   rep_goal (Const ("==>",_)$s$t)         =
   10.84 +                        (case rep_goal t of (l,t) => (s::l,t))
   10.85 +        |   rep_goal t                             = ([]  ,t);
   10.86 +        val (prems, Const("Trueprop", _)$concl) = rep_goal
   10.87 +                                                (#3(dest_state (st,i)));
   10.88 +*)
   10.89 +        val subgoal = #3(dest_state (st,i));
   10.90 +        val prems = Logic.strip_assums_hyp subgoal;
   10.91 +        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
   10.92 +        fun drot_tac k i = DETERM (rotate_tac k i);
   10.93 +        fun spec_tac 0 i = all_tac
   10.94 +        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
   10.95 +        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
   10.96 +                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
   10.97 +        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
   10.98 +        |   same_head k (s$_)         (t$_)         = same_head k s t
   10.99 +        |   same_head k (Bound i)     (Bound j)     = i = j + k
  10.100 +        |   same_head _ _             _             = true;
  10.101 +        fun mapn f n []      = []
  10.102 +        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
  10.103 +        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
  10.104 +                if same_head k t concl
  10.105 +                then dup_spec_tac k i THEN
  10.106 +                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
  10.107 +                else no_tac);
  10.108 +        val ptacs = mapn (fn n => fn t =>
  10.109 +                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
  10.110 +        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
  10.111 +
  10.112 +fun ptac prog = let
  10.113 +  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
  10.114 +  in    (REPEAT_DETERM1 o FIRST' [
  10.115 +                rtac TrueI,                     (* "True" *)
  10.116 +                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
  10.117 +                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
  10.118 +                rtac exI,                       (* "P x ==> ? x. P x" *)
  10.119 +                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
  10.120 +                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
  10.121 +                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
  10.122 +                ])
  10.123 +        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
  10.124 +        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
  10.125 +                 THEN' (fn _ => check_HOHH_tac2))
  10.126 +end;
  10.127 +
  10.128 +fun prolog_tac prog = check_HOHH_tac1 THEN
  10.129 +                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
  10.130 +
  10.131 +val prog_HOHH = [];
  10.132 +
  10.133 +end;