dropped reference to type classes
authorhaftmann
Fri Feb 19 14:47:00 2010 +0100 (2010-02-19)
changeset 352653fd8c3edf639
parent 35264 f44ef0e2d178
child 35266 07a56610c00b
dropped reference to type classes
src/HOL/Prolog/Func.thy
     1.1 --- a/src/HOL/Prolog/Func.thy	Fri Feb 19 14:46:59 2010 +0100
     1.2 +++ b/src/HOL/Prolog/Func.thy	Fri Feb 19 14:47:00 2010 +0100
     1.3 @@ -10,31 +10,28 @@
     1.4  
     1.5  typedecl tm
     1.6  
     1.7 -consts
     1.8 -  abs     :: "(tm => tm) => tm"
     1.9 -  app     :: "tm => tm => tm"
    1.10 +axiomatization
    1.11 +  abs     :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and
    1.12 +  app     :: "tm \<Rightarrow> tm \<Rightarrow> tm" and
    1.13  
    1.14 -  cond    :: "tm => tm => tm => tm"
    1.15 -  "fix"   :: "(tm => tm) => tm"
    1.16 -
    1.17 -  true    :: tm
    1.18 -  false   :: tm
    1.19 -  "and"   :: "tm => tm => tm"       (infixr "and" 999)
    1.20 -  eq      :: "tm => tm => tm"       (infixr "eq" 999)
    1.21 +  cond    :: "tm \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" and
    1.22 +  "fix"   :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and
    1.23  
    1.24 -  Z       :: tm                     ("Z")
    1.25 -  S       :: "tm => tm"
    1.26 -(*
    1.27 -        "++", "--",
    1.28 -        "**"    :: tm => tm => tm       (infixr 999)
    1.29 -*)
    1.30 -        eval    :: "[tm, tm] => bool"
    1.31 +  true    :: tm and
    1.32 +  false   :: tm and
    1.33 +  "and"   :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixr "and" 999) and
    1.34 +  eq      :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixr "eq" 999) and
    1.35 +
    1.36 +  Z       :: tm                     ("Z") and
    1.37 +  S       :: "tm \<Rightarrow> tm" and
    1.38  
    1.39 -instance tm :: plus ..
    1.40 -instance tm :: minus ..
    1.41 -instance tm :: times ..
    1.42 +  plus    :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixl "+" 65) and
    1.43 +  minus   :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixl "-" 65) and
    1.44 +  times   :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixl "*" 70) and
    1.45  
    1.46 -axioms   eval: "
    1.47 +  eval    :: "tm \<Rightarrow> tm \<Rightarrow> bool" where
    1.48 +
    1.49 +eval: "
    1.50  
    1.51  eval (abs RR) (abs RR)..
    1.52  eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
    1.53 @@ -59,7 +56,6 @@
    1.54  eval ( Z    * M) Z..
    1.55  eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
    1.56  
    1.57 -
    1.58  lemmas prog_Func = eval
    1.59  
    1.60  lemma "eval ((S (S Z)) + (S Z)) ?X"