# HG changeset patch
# User wenzelm
# Date 1164054192 -3600
# Node ID c11ab38b78a7968d51fd9733effaa6dbae767563
# Parent  5295ffa18285b8c85895fba15ea1d579aa2ac085
HOL-Prolog: converted legacy ML scripts;

diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 20 21:23:12 2006 +0100
@@ -499,9 +499,8 @@
 
 HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
 
-$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/HOHH.ML Prolog/HOHH.thy \
-  Prolog/Test.ML Prolog/Test.thy  \
-  Prolog/Func.ML Prolog/Func.thy Prolog/Type.ML Prolog/Type.thy
+$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML Prolog/HOHH.thy \
+  Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Prolog
 
 
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/Func.ML
--- a/src/HOL/Prolog/Func.ML	Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title:    HOL/Prolog/Func.ML
-    ID:       $Id$
-    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-val prog_Func = prog_HOHH @ [eval];
-fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Func));
-val p = ptac prog_Func 1;
-
-pgoal "eval ((S (S Z)) + (S Z)) ?X";
-
-pgoal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
-                        \(n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X";
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Func.thy	Mon Nov 20 21:23:12 2006 +0100
@@ -20,8 +20,8 @@
 
   true    :: tm
   false   :: tm
-  "and"   :: "tm => tm => tm"       (infixr 999)
-  "eq"    :: "tm => tm => tm"       (infixr 999)
+  "and"   :: "tm => tm => tm"       (infixr "and" 999)
+  eq      :: "tm => tm => tm"       (infixr "eq" 999)
 
   Z       :: tm                     ("Z")
   S       :: "tm => tm"
@@ -60,6 +60,16 @@
 eval ( Z    * M) Z..
 eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemmas prog_Func = eval
+
+lemma "eval ((S (S Z)) + (S Z)) ?X"
+  apply (prolog prog_Func)
+  done
+
+lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+                        (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
+  apply (prolog prog_Func)
+  done
 
 end
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/HOHH.ML
--- a/src/HOL/Prolog/HOHH.ML	Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(*  Title:    HOL/Prolog/HOHH.ML
-    ID:       $Id$
-    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-exception not_HOHH;
-
-fun isD t = case t of
-    Const("Trueprop",_)$t     => isD t
-  | Const("op &"  ,_)$l$r     => isD l andalso isD r
-  | Const("op -->",_)$l$r     => isG l andalso isD r
-  | Const(   "==>",_)$l$r     => isG l andalso isD r
-  | Const("All",_)$Abs(s,_,t) => isD t
-  | Const("all",_)$Abs(s,_,t) => isD t
-  | Const("op |",_)$_$_       => false
-  | Const("Ex" ,_)$_          => false
-  | Const("not",_)$_          => false
-  | Const("True",_)           => false
-  | Const("False",_)          => false
-  | l $ r                     => isD l
-  | Const _ (* rigid atom *)  => true
-  | Bound _ (* rigid atom *)  => true
-  | Free  _ (* rigid atom *)  => true
-  | _    (* flexible atom,
-            anything else *)  => false
-and
-    isG t = case t of
-    Const("Trueprop",_)$t     => isG t
-  | Const("op &"  ,_)$l$r     => isG l andalso isG r
-  | Const("op |"  ,_)$l$r     => isG l andalso isG r
-  | Const("op -->",_)$l$r     => isD l andalso isG r
-  | Const(   "==>",_)$l$r     => isD l andalso isG r
-  | Const("All",_)$Abs(_,_,t) => isG t
-  | Const("all",_)$Abs(_,_,t) => isG t
-  | Const("Ex" ,_)$Abs(_,_,t) => isG t
-  | Const("True",_)           => true
-  | Const("not",_)$_          => false
-  | Const("False",_)          => false
-  | _ (* atom *)              => true;
-
-val check_HOHH_tac1 = PRIMITIVE (fn thm =>
-        if isG (concl_of thm) then thm else raise not_HOHH);
-val check_HOHH_tac2 = PRIMITIVE (fn thm =>
-        if forall isG (prems_of thm) then thm else raise not_HOHH);
-fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
-                        then thm else raise not_HOHH);
-
-fun atomizeD thm = let
-    fun at  thm = case concl_of thm of
-      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
-                                        "?"^(if s="P" then "PP" else s))] spec))
-    | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
-    | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
-    | _                             => [thm]
-in map zero_var_indexes (at thm) end;
-
-val atomize_ss =
-  Simplifier.theory_context (the_context ()) empty_ss
-  setmksimps (mksimps mksimps_pairs)
-  addsimps [
-        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
-        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
-        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
-        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
-
-(*val hyp_resolve_tac = METAHYPS (fn prems =>
-                                  resolve_tac (List.concat (map atomizeD prems)) 1);
-  -- is nice, but cannot instantiate unknowns in the assumptions *)
-fun hyp_resolve_tac i st = let
-        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
-        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
-        |   ap t                          =                         (0,false,t);
-(*
-        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
-        |   rep_goal (Const ("==>",_)$s$t)         =
-                        (case rep_goal t of (l,t) => (s::l,t))
-        |   rep_goal t                             = ([]  ,t);
-        val (prems, Const("Trueprop", _)$concl) = rep_goal
-                                                (#3(dest_state (st,i)));
-*)
-        val subgoal = #3(dest_state (st,i));
-        val prems = Logic.strip_assums_hyp subgoal;
-        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
-        fun drot_tac k i = DETERM (rotate_tac k i);
-        fun spec_tac 0 i = all_tac
-        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
-        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
-                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
-        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
-        |   same_head k (s$_)         (t$_)         = same_head k s t
-        |   same_head k (Bound i)     (Bound j)     = i = j + k
-        |   same_head _ _             _             = true;
-        fun mapn f n []      = []
-        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
-        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
-                if same_head k t concl
-                then dup_spec_tac k i THEN
-                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
-                else no_tac);
-        val ptacs = mapn (fn n => fn t =>
-                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
-        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
-
-fun ptac prog = let
-  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
-  in    (REPEAT_DETERM1 o FIRST' [
-                rtac TrueI,                     (* "True" *)
-                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
-                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
-                rtac exI,                       (* "P x ==> ? x. P x" *)
-                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
-                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
-                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
-                ])
-        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
-        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
-                 THEN' (fn _ => check_HOHH_tac2))
-end;
-
-fun prolog_tac prog = check_HOHH_tac1 THEN
-                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
-
-val prog_HOHH = [];
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/HOHH.thy	Mon Nov 20 21:23:12 2006 +0100
@@ -7,18 +7,27 @@
 
 theory HOHH
 imports HOL
+uses "prolog.ML"
 begin
 
+method_setup ptac =
+  {* Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o Prolog.ptac) *}
+  "Basic Lambda Prolog interpreter"
+
+method_setup prolog =
+  {* Method.thms_args (Method.SIMPLE_METHOD o Prolog.prolog_tac) *}
+  "Lambda Prolog interpreter"
+
 consts
 
 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
-  "Dand"        :: "[bool, bool] => bool"         (infixr ".." 28)
-  ":-"          :: "[bool, bool] => bool"         (infixl 29)
+  Dand        :: "[bool, bool] => bool"         (infixr ".." 28)
+  Dif        :: "[bool, bool] => bool"         (infixl ":-" 29)
 
 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
                                | True | !x. G | D => G                  *)
-(*","           :: "[bool, bool] => bool"         (infixr 35)*)
-  "=>"          :: "[bool, bool] => bool"         (infixr 27)
+(*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
+  Dimp          :: "[bool, bool] => bool"         (infixr "=>" 27)
 
 translations
 
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/Test.ML
--- a/src/HOL/Prolog/Test.ML	Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,145 +0,0 @@
-(*  Title:    HOL/Prolog/Test.ML
-    ID:       $Id$
-    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
-fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
-val p = ptac prog_Test 1;
-
-pgoal "append ?x ?y [a,b,c,d]";
-back();
-back();
-back();
-back();
-
-pgoal "append [a,b] y ?L";
-pgoal "!y. append [a,b] y (?L y)";
-
-pgoal "reverse [] ?L";
-
-pgoal "reverse [23] ?L";
-pgoal "reverse [23,24,?x] ?L";
-pgoal "reverse ?L [23,24,?x]";
-
-pgoal "mappred age ?x [23,24]";
-back();
-
-pgoal "mappred (%x y. ? z. age z y) ?x [23,24]";
-
-pgoal "mappred ?P [bob,sue] [24,23]";
-
-pgoal "mapfun f [bob,bob,sue] [?x,?y,?z]";
-
-pgoal "mapfun (%x. h x 25) [bob,sue] ?L";
-
-pgoal "mapfun ?F [24,25] [h bob 24,h bob 25]";
-
-pgoal "mapfun ?F [24] [h 24 24]";
-back();
-back();
-back();
-
-
-(*
-goal (the_context ()) "f a = ?g a a & ?g = x";
-by (rtac conjI 1);
-by (rtac refl 1);
-back();
-back();
-*)
-
-pgoal "True";
-
-pgoal "age ?x 24 & age ?y 23";
-back();
-
-pgoal "age ?x 24 | age ?x 23";
-back();
-back();
-
-pgoal "? x y. age x y";
-
-pgoal "!x y. append [] x x";
-
-pgoal "age sue 24 .. age bob 23 => age ?x ?y";
-back();
-back();
-back();
-back();
-
-(*set trace_DEPTH_FIRST;*)
-pgoal "age bob 25 :- age bob 24 => age bob 25";
-(*reset trace_DEPTH_FIRST;*)
-
-pgoal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25";
-back();
-back();
-back();
-
-pgoal "!x. ? y. eq x y";
-
-pgoal "? P. P & eq P ?x";
-(*
-back();
-back();
-back();
-back();
-back();
-back();
-back();
-back();
-*)
-
-pgoal "? P. eq P (True & True) & P";
-
-pgoal "? P. eq P op | & P k True";
-
-pgoal "? P. eq P (Q => True) & P";
-
-(* P flexible: *)
-pgoal "(!P k l. P k l :- eq P Q) => Q a b";
-(*
-loops:
-pgoal "(!P k l. P k l :- eq P (%x y. x | y)) => a | b";
-*)
-
-(* implication and disjunction in atom: *)
-goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
-by (fast_tac HOL_cs 1);
-
-(* disjunction in atom: *)
-goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
-by (step_tac HOL_cs 1);
-by (step_tac HOL_cs 1);
-by (step_tac HOL_cs 1);
-by (fast_tac HOL_cs 2);
-by (fast_tac HOL_cs 1);
-(*
-hangs:
-goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)";
-by (fast_tac HOL_cs 1);
-*)
-
-pgoal "!Emp Stk.(\
-\                       empty    (Emp::'b) .. \
-\         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. \
-\         (!(X::nat) S. remove X ((Stk X S)::'b) S))\
-\ => bag_appl 23 24 ?X ?Y";
-
-pgoal "!Qu. ( \
-\          (!L.            empty    (Qu L L)) .. \
-\          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..\
-\          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))\
-\ => bag_appl 23 24 ?X ?Y";
-
-pgoal "D & (!y. E) :- (!x. True & True) :- True => D";
-
-pgoal "P x .. P y => P ?X";
-back();
-(*
-back();
--> problem with DEPTH_SOLVE:
-Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
-Exception raised at run-time
-*)
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Test.thy	Mon Nov 20 21:23:12 2006 +0100
@@ -80,6 +80,202 @@
                                 remove Y S4 S5 &
                                 empty    S5)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
+
+lemma "append ?x ?y [a,b,c,d]"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  back
+  done
+
+lemma "append [a,b] y ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "!y. append [a,b] y (?L y)"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse [] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse [23] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse [23,24,?x] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "reverse ?L [23,24,?x]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mappred age ?x [23,24]"
+  apply (prolog prog_Test)
+  back
+  done
+
+lemma "mappred (%x y. ? z. age z y) ?x [23,24]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mappred ?P [bob,sue] [24,23]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun f [bob,bob,sue] [?x,?y,?z]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun (%x. h x 25) [bob,sue] ?L"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun ?F [24,25] [h bob 24,h bob 25]"
+  apply (prolog prog_Test)
+  done
+
+lemma "mapfun ?F [24] [h 24 24]"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  done
+
+lemma "True"
+  apply (prolog prog_Test)
+  done
+
+lemma "age ?x 24 & age ?y 23"
+  apply (prolog prog_Test)
+  back
+  done
+
+lemma "age ?x 24 | age ?x 23"
+  apply (prolog prog_Test)
+  back
+  back
+  done
+
+lemma "? x y. age x y"
+  apply (prolog prog_Test)
+  done
+
+lemma "!x y. append [] x x"
+  apply (prolog prog_Test)
+  done
+
+lemma "age sue 24 .. age bob 23 => age ?x ?y"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  back
+  done
+
+(*set trace_DEPTH_FIRST;*)
+lemma "age bob 25 :- age bob 24 => age bob 25"
+  apply (prolog prog_Test)
+  done
+(*reset trace_DEPTH_FIRST;*)
+
+lemma "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
+  apply (prolog prog_Test)
+  back
+  back
+  back
+  done
+
+lemma "!x. ? y. eq x y"
+  apply (prolog prog_Test)
+  done
+
+lemma "? P. P & eq P ?x"
+  apply (prolog prog_Test)
+(*
+  back
+  back
+  back
+  back
+  back
+  back
+  back
+  back
+*)
+  done
+
+lemma "? P. eq P (True & True) & P"
+  apply (prolog prog_Test)
+  done
+
+lemma "? P. eq P op | & P k True"
+  apply (prolog prog_Test)
+  done
+
+lemma "? P. eq P (Q => True) & P"
+  apply (prolog prog_Test)
+  done
+
+(* P flexible: *)
+lemma "(!P k l. P k l :- eq P Q) => Q a b"
+  apply (prolog prog_Test)
+  done
+(*
+loops:
+lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
+*)
+
+(* implication and disjunction in atom: *)
+lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"
+  by fast
+
+(* disjunction in atom: *)
+lemma "(!P. g P :- (P => b | a)) => g(a | b)"
+  apply (tactic "step_tac HOL_cs 1")
+  apply (tactic "step_tac HOL_cs 1")
+  apply (tactic "step_tac HOL_cs 1")
+   prefer 2
+   apply fast
+  apply fast
+  done
+
+(*
+hangs:
+lemma "(!P. g P :- (P => b | a)) => g(a | b)"
+  by fast
+*)
+
+lemma "!Emp Stk.(
+                       empty    (Emp::'b) .. 
+         (!(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
+         (!(X::nat) S. remove X ((Stk X S)::'b) S))
+ => bag_appl 23 24 ?X ?Y"
+  oops
+
+lemma "!Qu. ( 
+          (!L.            empty    (Qu L L)) .. 
+          (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
+          (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
+ => bag_appl 23 24 ?X ?Y"
+  oops
+
+lemma "D & (!y. E) :- (!x. True & True) :- True => D"
+  apply (prolog prog_Test)
+  done
+
+lemma "P x .. P y => P ?X"
+  apply (prolog prog_Test)
+  back
+  done
+(*
+back
+-> problem with DEPTH_SOLVE:
+Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised
+Exception raised at run-time
+*)
 
 end
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/Type.ML
--- a/src/HOL/Prolog/Type.ML	Mon Nov 20 11:51:10 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:    HOL/Prolog/Type.ML
-    ID:       $Id$
-    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
-*)
-
-val prog_Type = prog_Func @ [good_typeof,common_typeof];
-fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Type));
-val p = ptac prog_Type 1;
-
-pgoal "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T";
-
-pgoal "typeof (fix (%x. x)) ?T";
-
-pgoal "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T";
-
-pgoal "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z) \
-  \(n * (app fact (n - (S Z))))))) ?T";
-
-pgoal "typeof (abs(%v. Z)) ?T"; (*correct only solution (?A1 -> nat) *)
-Goal "typeof (abs(%v. Z)) ?T";
-by (prolog_tac [bad1_typeof,common_typeof]); (* 1st result ok*)
-back(); (* 2nd result (?A1 -> ?A1) wrong *)
-
-(*pgoal "typeof (abs(%v. abs(%v. app v v))) ?T"; correctly fails*)
-Goal "typeof (abs(%v. abs(%v. app v v))) ?T";
-by (prolog_tac [bad2_typeof,common_typeof]); 
-	(* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/Type.thy
--- a/src/HOL/Prolog/Type.thy	Mon Nov 20 11:51:10 2006 +0100
+++ b/src/HOL/Prolog/Type.thy	Mon Nov 20 21:23:12 2006 +0100
@@ -14,7 +14,7 @@
 consts
   bool    :: ty
   nat     :: ty
-  "->"    :: "ty => ty => ty"       (infixr 20)
+  arrow   :: "ty => ty => ty"       (infixr "->" 20)
   typeof  :: "[tm, ty] => bool"
   anyterm :: tm
 
@@ -45,6 +45,45 @@
 axioms bad2_typeof:     "
 typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemmas prog_Type = prog_Func good_typeof common_typeof
+
+lemma "typeof (abs(%n. abs(%m. abs(%p. p and (n eq m))))) ?T"
+  apply (prolog prog_Type)
+  done
+
+lemma "typeof (fix (%x. x)) ?T"
+  apply (prolog prog_Type)
+  done
+
+lemma "typeof (fix (%fact. abs(%n. (app fact (n - Z))))) ?T"
+  apply (prolog prog_Type)
+  done
+
+lemma "typeof (fix (%fact. abs(%n. cond (n eq Z) (S Z)
+  (n * (app fact (n - (S Z))))))) ?T"
+  apply (prolog prog_Type)
+  done
+
+lemma "typeof (abs(%v. Z)) ?T" (*correct only solution (?A1 -> nat) *)
+  apply (prolog prog_Type)
+  done
+
+lemma "typeof (abs(%v. Z)) ?T"
+  apply (prolog bad1_typeof common_typeof) (* 1st result ok*)
+  done
+
+lemma "typeof (abs(%v. Z)) ?T"
+  apply (prolog bad1_typeof common_typeof)
+  back (* 2nd result (?A1 -> ?A1) wrong *)
+  done
+
+lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+  apply (prolog prog_Type)?  (*correctly fails*)
+  oops
+
+lemma "typeof (abs(%v. abs(%v. app v v))) ?T"
+  apply (prolog bad2_typeof common_typeof) (* wrong result ((?A3 -> ?B3) -> ?A3 -> ?B3)*)
+  done
 
 end
diff -r 5295ffa18285 -r c11ab38b78a7 src/HOL/Prolog/prolog.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/prolog.ML	Mon Nov 20 21:23:12 2006 +0100
@@ -0,0 +1,130 @@
+(*  Title:    HOL/Prolog/prolog.ML
+    ID:       $Id$
+    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
+*)
+
+set Proof.show_main_goal;
+
+structure Prolog =
+struct
+
+exception not_HOHH;
+
+fun isD t = case t of
+    Const("Trueprop",_)$t     => isD t
+  | Const("op &"  ,_)$l$r     => isD l andalso isD r
+  | Const("op -->",_)$l$r     => isG l andalso isD r
+  | Const(   "==>",_)$l$r     => isG l andalso isD r
+  | Const("All",_)$Abs(s,_,t) => isD t
+  | Const("all",_)$Abs(s,_,t) => isD t
+  | Const("op |",_)$_$_       => false
+  | Const("Ex" ,_)$_          => false
+  | Const("not",_)$_          => false
+  | Const("True",_)           => false
+  | Const("False",_)          => false
+  | l $ r                     => isD l
+  | Const _ (* rigid atom *)  => true
+  | Bound _ (* rigid atom *)  => true
+  | Free  _ (* rigid atom *)  => true
+  | _    (* flexible atom,
+            anything else *)  => false
+and
+    isG t = case t of
+    Const("Trueprop",_)$t     => isG t
+  | Const("op &"  ,_)$l$r     => isG l andalso isG r
+  | Const("op |"  ,_)$l$r     => isG l andalso isG r
+  | Const("op -->",_)$l$r     => isD l andalso isG r
+  | Const(   "==>",_)$l$r     => isD l andalso isG r
+  | Const("All",_)$Abs(_,_,t) => isG t
+  | Const("all",_)$Abs(_,_,t) => isG t
+  | Const("Ex" ,_)$Abs(_,_,t) => isG t
+  | Const("True",_)           => true
+  | Const("not",_)$_          => false
+  | Const("False",_)          => false
+  | _ (* atom *)              => true;
+
+val check_HOHH_tac1 = PRIMITIVE (fn thm =>
+        if isG (concl_of thm) then thm else raise not_HOHH);
+val check_HOHH_tac2 = PRIMITIVE (fn thm =>
+        if forall isG (prems_of thm) then thm else raise not_HOHH);
+fun check_HOHH thm  = (if isD (concl_of thm) andalso forall isG (prems_of thm)
+                        then thm else raise not_HOHH);
+
+fun atomizeD thm = let
+    fun at  thm = case concl_of thm of
+      _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (read_instantiate [("x",
+                                        "?"^(if s="P" then "PP" else s))] spec))
+    | _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
+    | _$(Const("op -->",_)$_$_)     => at(thm RS mp)
+    | _                             => [thm]
+in map zero_var_indexes (at thm) end;
+
+val atomize_ss =
+  Simplifier.theory_context (the_context ()) empty_ss
+  setmksimps (mksimps mksimps_pairs)
+  addsimps [
+        all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
+        imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
+        imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
+        imp_all];         (* "((!x. D) :- G) = (!x. D :- G)" *)
+
+(*val hyp_resolve_tac = METAHYPS (fn prems =>
+                                  resolve_tac (List.concat (map atomizeD prems)) 1);
+  -- is nice, but cannot instantiate unknowns in the assumptions *)
+fun hyp_resolve_tac i st = let
+        fun ap (Const("All",_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
+        |   ap (Const("op -->",_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
+        |   ap t                          =                         (0,false,t);
+(*
+        fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t
+        |   rep_goal (Const ("==>",_)$s$t)         =
+                        (case rep_goal t of (l,t) => (s::l,t))
+        |   rep_goal t                             = ([]  ,t);
+        val (prems, Const("Trueprop", _)$concl) = rep_goal
+                                                (#3(dest_state (st,i)));
+*)
+        val subgoal = #3(dest_state (st,i));
+        val prems = Logic.strip_assums_hyp subgoal;
+        val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal);
+        fun drot_tac k i = DETERM (rotate_tac k i);
+        fun spec_tac 0 i = all_tac
+        |   spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i;
+        fun dup_spec_tac k i = if k = 0 then all_tac else EVERY'
+                      [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i;
+        fun same_head _ (Const (x,_)) (Const (y,_)) = x = y
+        |   same_head k (s$_)         (t$_)         = same_head k s t
+        |   same_head k (Bound i)     (Bound j)     = i = j + k
+        |   same_head _ _             _             = true;
+        fun mapn f n []      = []
+        |   mapn f n (x::xs) = f n x::mapn f (n+1) xs;
+        fun pres_tac (k,arrow,t) n i = drot_tac n i THEN (
+                if same_head k t concl
+                then dup_spec_tac k i THEN
+                     (if arrow then etac mp i THEN drot_tac (~n) i else atac i)
+                else no_tac);
+        val ptacs = mapn (fn n => fn t =>
+                          pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems;
+        in Library.foldl (op APPEND) (no_tac, ptacs) st end;
+
+fun ptac prog = let
+  val proga = List.concat (map atomizeD prog)                   (* atomize the prog *)
+  in    (REPEAT_DETERM1 o FIRST' [
+                rtac TrueI,                     (* "True" *)
+                rtac conjI,                     (* "[| P; Q |] ==> P & Q" *)
+                rtac allI,                      (* "(!!x. P x) ==> ! x. P x" *)
+                rtac exI,                       (* "P x ==> ? x. P x" *)
+                rtac impI THEN'                 (* "(P ==> Q) ==> P --> Q" *)
+                  asm_full_simp_tac atomize_ss THEN'    (* atomize the asms *)
+                  (REPEAT_DETERM o (etac conjE))        (* split the asms *)
+                ])
+        ORELSE' resolve_tac [disjI1,disjI2]     (* "P ==> P | Q","Q ==> P | Q"*)
+        ORELSE' ((resolve_tac proga APPEND' hyp_resolve_tac)
+                 THEN' (fn _ => check_HOHH_tac2))
+end;
+
+fun prolog_tac prog = check_HOHH_tac1 THEN
+                      DEPTH_SOLVE (ptac (map check_HOHH prog) 1);
+
+val prog_HOHH = [];
+
+end;