src/HOL/Prolog/Func.thy
changeset 21425 c11ab38b78a7
parent 20713 823967ef47f1
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Prolog/Func.thy	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ b/src/HOL/Prolog/Func.thy	Mon Nov 20 21:23:12 2006 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4  
     1.5    true    :: tm
     1.6    false   :: tm
     1.7 -  "and"   :: "tm => tm => tm"       (infixr 999)
     1.8 -  "eq"    :: "tm => tm => tm"       (infixr 999)
     1.9 +  "and"   :: "tm => tm => tm"       (infixr "and" 999)
    1.10 +  eq      :: "tm => tm => tm"       (infixr "eq" 999)
    1.11  
    1.12    Z       :: tm                     ("Z")
    1.13    S       :: "tm => tm"
    1.14 @@ -60,6 +60,16 @@
    1.15  eval ( Z    * M) Z..
    1.16  eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
    1.17  
    1.18 -ML {* use_legacy_bindings (the_context ()) *}
    1.19 +
    1.20 +lemmas prog_Func = eval
    1.21 +
    1.22 +lemma "eval ((S (S Z)) + (S Z)) ?X"
    1.23 +  apply (prolog prog_Func)
    1.24 +  done
    1.25 +
    1.26 +lemma "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z)
    1.27 +                        (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X"
    1.28 +  apply (prolog prog_Func)
    1.29 +  done
    1.30  
    1.31  end