# HG changeset patch
# User oheimb
# Date 959942644 -7200
# Node ID 8006e900962120630c2ab1340edf8acbfdeb34c7
# Parent 4382883421ecec0b050fcf8fef6396732e5bddee
added HOL/Prolog
diff -r 4382883421ec -r 8006e9009621 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile Thu Jun 01 13:28:00 2000 +0200
+++ b/src/HOL/IsaMakefile Fri Jun 02 12:44:04 2000 +0200
@@ -9,8 +9,8 @@
default: HOL
images: HOL HOL-Real TLA
test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \
- HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
- HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
+ HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML \
+ HOL-BCV HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
@@ -291,6 +291,16 @@
@$(ISATOOL) usedir $(OUT)/HOL Lambda
+## HOL-Prolog
+
+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
+ @$(ISATOOL) usedir $(OUT)/HOL Prolog
+
+
## HOL-W0
HOL-W0: HOL $(LOG)/HOL-W0.gz
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/Func.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/Func.ML Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,12 @@
+open Func;
+
+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 4382883421ec -r 8006e9009621 src/HOL/Prolog/Func.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/Func.thy Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,57 @@
+(* untyped functional language, with call by value semantics *)
+
+Func = HOHH +
+
+types tm
+
+arities tm :: term
+
+consts abs :: (tm => tm) => tm
+ app :: tm => tm => tm
+
+ cond :: tm => tm => tm => tm
+ fix :: (tm => tm) => tm
+
+ true,
+ false :: tm
+ "and" :: tm => tm => tm (infixr 999)
+ "eq" :: tm => tm => tm (infixr 999)
+
+ "0" :: tm ("Z")
+ S :: tm => tm
+(*
+ "++", "--",
+ "**" :: tm => tm => tm (infixr 999)
+*)
+ eval :: [tm, tm] => bool
+
+arities tm :: plus
+arities tm :: minus
+arities tm :: times
+
+rules eval "
+
+eval (abs RR) (abs RR)..
+eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
+
+eval (cond P L1 R1) D1 :- eval P true & eval L1 D1..
+eval (cond P L2 R2) D2 :- eval P false & eval R2 D2..
+eval (fix G) W :- eval (G (fix G)) W..
+
+eval true true ..
+eval false false..
+eval (P and Q) true :- eval P true & eval Q true ..
+eval (P and Q) false :- eval P false | eval Q false..
+eval (A1 eq B1) true :- eval A1 C1 & eval B1 C1..
+eval (A2 eq B2) false :- True..
+
+eval Z Z..
+eval (S N) (S M) :- eval N M..
+eval ( Z + M) K :- eval M K..
+eval ((S N) + M) (S K) :- eval (N + M) K..
+eval (N - Z) K :- eval N K..
+eval ((S N) - (S M)) K :- eval (N- M) K..
+eval ( Z * M) Z..
+eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
+
+end
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/HOHH.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/HOHH.ML Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,117 @@
+open HOHH;
+
+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 = 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 (flat (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 foldl (op APPEND) (no_tac, ptacs) st end;
+
+fun ptac prog = let
+ val proga = flat (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 4382883421ec -r 8006e9009621 src/HOL/Prolog/HOHH.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/HOHH.thy Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,24 @@
+(* higher-order hereditary Harrop formulas *)
+
+HOHH = HOL +
+
+consts
+
+(* D-formulas (programs): D ::= !x. D | D .. D | D :- G | A *)
+ "Dand" :: [bool, bool] => bool (infixr ".." 28)
+ ":-" :: [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)
+
+translations
+
+ "D :- G" => "G --> D"
+ "D1 .. D2" => "D1 & D2"
+(*"G1 , G2" => "G1 & G2"*)
+ "D => G" => "D --> G"
+
+end
+
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/README.html Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,13 @@
+
+
+HOL/Prolog/README
+
+
+Prolog -- A bare-bones implementation of Lambda-Prolog
+
+This is a simple exploratory implementatin of
+Lambda-Prolog in HOL,
+including some minimal examples (in Test.thy) and a more typical example
+of a little functional language and its type system.
+
+
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/ROOT.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/ROOT.ML Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,2 @@
+use_thy"Test";
+use_thy"Type";
\ No newline at end of file
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/Test.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/Test.ML Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,142 @@
+open Test;
+
+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 thy "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 thy "? 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 thy "(!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 thy "(!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
+*)
\ No newline at end of file
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/Test.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/Test.thy Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,76 @@
+(* basic examples *)
+
+Test = HOHH +
+
+types nat
+arities nat :: term
+
+types 'a list
+arities list :: (term) term
+
+consts Nil :: 'a list ("[]")
+ Cons :: 'a => 'a list => 'a list (infixr "#" 65)
+
+syntax
+ (* list Enumeration *)
+ "@list" :: args => 'a list ("[(_)]")
+
+translations
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
+
+types person
+arities person :: term
+
+consts
+ append :: ['a list, 'a list, 'a list] => bool
+ reverse :: ['a list, 'a list] => bool
+
+ mappred :: [('a => 'b => bool), 'a list, 'b list] => bool
+ mapfun :: [('a => 'b), 'a list, 'b list] => bool
+
+ bob :: person
+ sue :: person
+ ned :: person
+
+ "23" :: nat ("23")
+ "24" :: nat ("24")
+ "25" :: nat ("25")
+
+ age :: [person, nat] => bool
+
+ eq :: ['a, 'a] => bool
+
+ empty :: ['b] => bool
+ add :: ['a, 'b, 'b] => bool
+ remove :: ['a, 'b, 'b] => bool
+ bag_appl:: ['a, 'a, 'a, 'a] => bool
+
+rules append "append [] xs xs ..
+ append (x#xs) ys (x#zs) :- append xs ys zs"
+ reverse "reverse L1 L2 :- (!rev_aux.
+ (!L. rev_aux [] L L )..
+ (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
+ => rev_aux L1 L2 [])"
+
+ mappred "mappred P [] [] ..
+ mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys"
+ mapfun "mapfun f [] [] ..
+ mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
+
+ age "age bob 24 ..
+ age sue 23 ..
+ age ned 23"
+
+ eq "eq x x"
+
+(* actual definitions of empty and add is hidden -> yields abstract data type *)
+
+ bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
+ empty S1 &
+ add A S1 S2 &
+ add B S2 S3 &
+ remove X S3 S4 &
+ remove Y S4 S5 &
+ empty S5)"
+end
diff -r 4382883421ec -r 8006e9009621 src/HOL/Prolog/Type.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/Type.ML Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,22 @@
+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-0))))) ?T";
+
+pgoal "typeof (fix (%fact. abs(%n. cond (n eq 0) (S 0) \
+ \(n * (app fact (n - (S 0))))))) ?T";
+
+pgoal "typeof (abs(%v. 0)) ?T"; (*correct only solution (?A1 -> nat) *)
+Goal "typeof (abs(%v. 0)) ?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 4382883421ec -r 8006e9009621 src/HOL/Prolog/Type.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/Type.thy Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,42 @@
+(* type inference *)
+
+Type = Func +
+
+types ty
+
+arities ty :: term
+
+consts bool :: ty
+ nat :: ty
+ "->" :: ty => ty => ty (infixr 20)
+ typeof :: [tm, ty] => bool
+ anyterm :: tm
+
+rules common_typeof "
+typeof (app M N) B :- typeof M (A -> B) & typeof N A..
+
+typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
+typeof (fix F) A :- (!x. typeof x A => typeof (F x) A)..
+
+typeof true bool..
+typeof false bool..
+typeof (M and N) bool :- typeof M bool & typeof N bool..
+
+typeof (M eq N) bool :- typeof M T & typeof N T ..
+
+typeof Z nat..
+typeof (S N) nat :- typeof N nat..
+typeof (M + N) nat :- typeof M nat & typeof N nat..
+typeof (M - N) nat :- typeof M nat & typeof N nat..
+typeof (M * N) nat :- typeof M nat & typeof N nat"
+
+rules good_typeof "
+typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
+
+rules bad1_typeof "
+typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
+
+rules bad2_typeof "
+typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"
+
+end