src/HOL/Prolog/Func.thy
changeset 17311 5b1d47d920ce
parent 14981 e73f8140af78
child 20713 823967ef47f1
     1.1 --- a/src/HOL/Prolog/Func.thy	Wed Sep 07 21:00:30 2005 +0200
     1.2 +++ b/src/HOL/Prolog/Func.thy	Wed Sep 07 21:07:09 2005 +0200
     1.3 @@ -1,40 +1,41 @@
     1.4  (*  Title:    HOL/Prolog/Func.thy
     1.5      ID:       $Id$
     1.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     1.7 -
     1.8 -untyped functional language, with call by value semantics 
     1.9  *)
    1.10  
    1.11 -Func = HOHH +
    1.12 +header {* Untyped functional language, with call by value semantics *}
    1.13  
    1.14 -types tm
    1.15 -
    1.16 -arities tm :: type
    1.17 +theory Func
    1.18 +imports HOHH
    1.19 +begin
    1.20  
    1.21 -consts	abs	:: (tm => tm) => tm
    1.22 -	app	:: tm => tm => tm
    1.23 +typedecl tm
    1.24  
    1.25 -	cond	:: tm => tm => tm => tm
    1.26 -	fix	:: (tm => tm) => tm
    1.27 +consts
    1.28 +  abs     :: "(tm => tm) => tm"
    1.29 +  app     :: "tm => tm => tm"
    1.30 +
    1.31 +  cond    :: "tm => tm => tm => tm"
    1.32 +  "fix"   :: "(tm => tm) => tm"
    1.33  
    1.34 -	true,
    1.35 -	false	:: tm
    1.36 -	"and"	:: tm => tm => tm	(infixr 999)
    1.37 -	"eq"	:: tm => tm => tm	(infixr 999)
    1.38 +  true    :: tm
    1.39 +  false   :: tm
    1.40 +  "and"   :: "tm => tm => tm"       (infixr 999)
    1.41 +  "eq"    :: "tm => tm => tm"       (infixr 999)
    1.42  
    1.43 -	"0"	:: tm			("Z")
    1.44 -	S	:: tm => tm
    1.45 +  "0"     :: tm                   ("Z")
    1.46 +  S       :: "tm => tm"
    1.47  (*
    1.48 -	"++", "--",
    1.49 -	"**"	:: tm => tm => tm	(infixr 999)
    1.50 +        "++", "--",
    1.51 +        "**"    :: tm => tm => tm       (infixr 999)
    1.52  *)
    1.53 -	eval	:: [tm, tm] => bool
    1.54 +        eval    :: "[tm, tm] => bool"
    1.55  
    1.56 -arities tm :: plus
    1.57 -arities tm :: minus
    1.58 -arities tm :: times
    1.59 +instance tm :: plus ..
    1.60 +instance tm :: minus ..
    1.61 +instance tm :: times ..
    1.62  
    1.63 -rules	eval "
    1.64 +axioms   eval: "
    1.65  
    1.66  eval (abs RR) (abs RR)..
    1.67  eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
    1.68 @@ -47,7 +48,7 @@
    1.69  eval false false..
    1.70  eval (P and Q) true  :- eval P true  & eval Q true ..
    1.71  eval (P and Q) false :- eval P false | eval Q false..
    1.72 -eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1.. 
    1.73 +eval (A1 eq B1) true  :- eval A1 C1 & eval B1 C1..
    1.74  eval (A2 eq B2) false :- True..
    1.75  
    1.76  eval Z Z..
    1.77 @@ -59,4 +60,6 @@
    1.78  eval ( Z    * M) Z..
    1.79  eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
    1.80  
    1.81 +ML {* use_legacy_bindings (the_context ()) *}
    1.82 +
    1.83  end