# 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