1(* Title: HOL/Prolog/Func.thy 2 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) 3*) 4 5section \<open>Untyped functional language, with call by value semantics\<close> 6 7theory Func 8imports HOHH 9begin 10 11typedecl tm 12 13axiomatization 14 abs :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and 15 app :: "tm \<Rightarrow> tm \<Rightarrow> tm" and 16 17 cond :: "tm \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" and 18 "fix" :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and 19 20 true :: tm and 21 false :: tm and 22 "and" :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixr "and" 999) and 23 eq :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixr "eq" 999) and 24 25 Z :: tm ("Z") and 26 S :: "tm \<Rightarrow> tm" and 27 28 plus :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixl "+" 65) and 29 minus :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixl "-" 65) and 30 times :: "tm \<Rightarrow> tm \<Rightarrow> tm" (infixl "*" 70) and 31 32 eval :: "tm \<Rightarrow> tm \<Rightarrow> bool" where 33 34eval: " 35 36eval (abs RR) (abs RR).. 37eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V.. 38 39eval (cond P L1 R1) D1 :- eval P true & eval L1 D1.. 40eval (cond P L2 R2) D2 :- eval P false & eval R2 D2.. 41eval (fix G) W :- eval (G (fix G)) W.. 42 43eval true true .. 44eval false false.. 45eval (P and Q) true :- eval P true & eval Q true .. 46eval (P and Q) false :- eval P false | eval Q false.. 47eval (A1 eq B1) true :- eval A1 C1 & eval B1 C1.. 48eval (A2 eq B2) false :- True.. 49 50eval Z Z.. 51eval (S N) (S M) :- eval N M.. 52eval ( Z + M) K :- eval M K.. 53eval ((S N) + M) (S K) :- eval (N + M) K.. 54eval (N - Z) K :- eval N K.. 55eval ((S N) - (S M)) K :- eval (N- M) K.. 56eval ( Z * M) Z.. 57eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K" 58 59lemmas prog_Func = eval 60 61schematic_goal "eval ((S (S Z)) + (S Z)) ?X" 62 apply (prolog prog_Func) 63 done 64 65schematic_goal "eval (app (fix (%fact. abs(%n. cond (n eq Z) (S Z) 66 (n * (app fact (n - (S Z))))))) (S (S (S Z)))) ?X" 67 apply (prolog prog_Func) 68 done 69 70end 71