--- a/src/HOL/Prolog/Test.thy Thu Feb 28 14:24:21 2013 +0100
+++ b/src/HOL/Prolog/Test.thy Thu Feb 28 14:29:54 2013 +0100
@@ -26,52 +26,51 @@
typedecl person
-consts
- append :: "['a list, 'a list, 'a list] => bool"
- reverse :: "['a list, 'a list] => bool"
+axiomatization
+ append :: "['a list, 'a list, 'a list] => bool" and
+ reverse :: "['a list, 'a list] => bool" and
- mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool"
- mapfun :: "[('a => 'b), 'a list, 'b list] => bool"
+ mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool" and
+ mapfun :: "[('a => 'b), 'a list, 'b list] => bool" and
- bob :: person
- sue :: person
- ned :: person
+ bob :: person and
+ sue :: person and
+ ned :: person and
- nat23 :: nat ("23")
- nat24 :: nat ("24")
- nat25 :: nat ("25")
+ nat23 :: nat ("23") and
+ nat24 :: nat ("24") and
+ nat25 :: nat ("25") and
- age :: "[person, nat] => bool"
+ age :: "[person, nat] => bool" and
- eq :: "['a, 'a] => bool"
+ eq :: "['a, 'a] => bool" and
- empty :: "['b] => bool"
- add :: "['a, 'b, 'b] => bool"
- remove :: "['a, 'b, 'b] => bool"
+ empty :: "['b] => bool" and
+ add :: "['a, 'b, 'b] => bool" and
+ remove :: "['a, 'b, 'b] => bool" and
bag_appl:: "['a, 'a, 'a, 'a] => bool"
-
-axioms
- append: "append [] xs xs ..
- append (x#xs) ys (x#zs) :- append xs ys zs"
- reverse: "reverse L1 L2 :- (!rev_aux.
+where
+ append: "\<And>x xs ys zs. append [] xs xs ..
+ append (x#xs) ys (x#zs) :- append xs ys zs" and
+ reverse: "\<And>L1 L2. reverse L1 L2 :- (!rev_aux.
(!L. rev_aux [] L L )..
(!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
- => rev_aux L1 L2 [])"
+ => rev_aux L1 L2 [])" and
- mappred: "mappred P [] [] ..
- mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys"
- mapfun: "mapfun f [] [] ..
- mapfun f (x#xs) (f x#ys) :- mapfun f xs ys"
+ mappred: "\<And>x xs y ys P. mappred P [] [] ..
+ mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys" and
+ mapfun: "\<And>x xs ys f. mapfun f [] [] ..
+ mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" and
age: "age bob 24 ..
age sue 23 ..
- age ned 23"
+ age ned 23" and
- eq: "eq x x"
+ eq: "\<And>x. eq x x" and
(* actual definitions of empty and add is hidden -> yields abstract data type *)
- bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
+ bag_appl: "\<And>A B X Y. bag_appl A B X Y:- (? S1 S2 S3 S4 S5.
empty S1 &
add A S1 S2 &
add B S2 S3 &
--- a/src/HOL/Prolog/Type.thy Thu Feb 28 14:24:21 2013 +0100
+++ b/src/HOL/Prolog/Type.thy Thu Feb 28 14:29:54 2013 +0100
@@ -10,14 +10,13 @@
typedecl ty
-consts
- bool :: ty
- nat :: ty
- arrow :: "ty => ty => ty" (infixr "->" 20)
- typeof :: "[tm, ty] => bool"
+axiomatization
+ bool :: ty and
+ nat :: ty and
+ arrow :: "ty => ty => ty" (infixr "->" 20) and
+ typeof :: "[tm, ty] => bool" and
anyterm :: tm
-
-axioms common_typeof: "
+where common_typeof: "
typeof (app M N) B :- typeof M (A -> B) & typeof N A..
typeof (cond C L R) A :- typeof C bool & typeof L A & typeof R A..
@@ -35,13 +34,13 @@
typeof (M - N) nat :- typeof M nat & typeof N nat..
typeof (M * N) nat :- typeof M nat & typeof N nat"
-axioms good_typeof: "
+axiomatization where good_typeof: "
typeof (abs Bo) (A -> B) :- (!x. typeof x A => typeof (Bo x) B)"
-axioms bad1_typeof: "
+axiomatization where bad1_typeof: "
typeof (abs Bo) (A -> B) :- (typeof varterm A => typeof (Bo varterm) B)"
-axioms bad2_typeof: "
+axiomatization where bad2_typeof: "
typeof (abs Bo) (A -> B) :- (typeof anyterm A => typeof (Bo anyterm) B)"