src/HOL/Prolog/Func.thy
changeset 9015 8006e9009621
child 12338 de0f4a63baa5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Prolog/Func.thy	Fri Jun 02 12:44:04 2000 +0200
     1.3 @@ -0,0 +1,57 @@
     1.4 +(* untyped functional language, with call by value semantics *)
     1.5 +
     1.6 +Func = HOHH +
     1.7 +
     1.8 +types tm
     1.9 +
    1.10 +arities tm :: term
    1.11 +
    1.12 +consts	abs	:: (tm => tm) => tm
    1.13 +	app	:: tm => tm => tm
    1.14 +
    1.15 +	cond	:: tm => tm => tm => tm
    1.16 +	fix	:: (tm => tm) => tm
    1.17 +
    1.18 +	true,
    1.19 +	false	:: tm
    1.20 +	"and"	:: tm => tm => tm	(infixr 999)
    1.21 +	"eq"	:: tm => tm => tm	(infixr 999)
    1.22 +
    1.23 +	"0"	:: tm			("Z")
    1.24 +	S	:: tm => tm
    1.25 +(*
    1.26 +	"++", "--",
    1.27 +	"**"	:: tm => tm => tm	(infixr 999)
    1.28 +*)
    1.29 +	eval	:: [tm, tm] => bool
    1.30 +
    1.31 +arities tm :: plus
    1.32 +arities tm :: minus
    1.33 +arities tm :: times
    1.34 +
    1.35 +rules	eval "
    1.36 +
    1.37 +eval (abs RR) (abs RR)..
    1.38 +eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
    1.39 +
    1.40 +eval (cond P L1 R1) D1 :- eval P true  & eval L1 D1..
    1.41 +eval (cond P L2 R2) D2 :- eval P false & eval R2 D2..
    1.42 +eval (fix G) W   :- eval (G (fix G)) W..
    1.43 +
    1.44 +eval true  true ..
    1.45 +eval false false..
    1.46 +eval (P and Q) true  :- eval P true  & eval Q true ..
    1.47 +eval (P and Q) false :- eval P false | eval Q false..
    1.48 +eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1.. 
    1.49 +eval (A2 eq B2) false :- True..
    1.50 +
    1.51 +eval Z Z..
    1.52 +eval (S N) (S M) :- eval N M..
    1.53 +eval ( Z    + M) K     :- eval      M  K..
    1.54 +eval ((S N) + M) (S K) :- eval (N + M) K..
    1.55 +eval (N     - Z) K     :- eval  N      K..
    1.56 +eval ((S N) - (S M)) K :- eval (N- M)  K..
    1.57 +eval ( Z    * M) Z..
    1.58 +eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
    1.59 +
    1.60 +end