(* Title: HOL/Prolog/Test.thy
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
section \<open>Basic examples\<close>
theory Test
imports HOHH
begin
typedecl nat
typedecl 'a list
consts
Nil :: "'a list" ("[]")
Cons :: "'a => 'a list => 'a list" (infixr "#" 65)
syntax
(* list Enumeration *)
"_list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
typedecl person
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" and
mapfun :: "[('a => 'b), 'a list, 'b list] => bool" and
bob :: person and
sue :: person and
ned :: person and
nat23 :: nat ("23") and
nat24 :: nat ("24") and
nat25 :: nat ("25") and
age :: "[person, nat] => bool" and
eq :: "['a, 'a] => bool" and
empty :: "['b] => bool" and
add :: "['a, 'b, 'b] => bool" and
remove :: "['a, 'b, 'b] => bool" and
bag_appl:: "['a, 'a, 'a, 'a] => bool"
where
append: "\x xs ys zs. append [] xs xs ..
append (x#xs) ys (x#zs) :- append xs ys zs" and
reverse: "\L1 L2. reverse L1 L2 :- (\rev_aux.
(\<forall>L. rev_aux [] L L )..
(\<forall>X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
=> rev_aux L1 L2 [])" and
mappred: "\x xs y ys P. mappred P [] [] ..
mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys" and
mapfun: "\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" and
eq: "\x. eq x x" and
(* actual definitions of empty and add is hidden -> yields abstract data type *)
bag_appl: "\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 &
remove X S3 S4 &
remove Y S4 S5 &
empty S5)"
lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
schematic_goal "append ?x ?y [a,b,c,d]"
apply (prolog prog_Test)
back
back
back
back
done
schematic_goal "append [a,b] y ?L"
apply (prolog prog_Test)
done
schematic_goal "\y. append [a,b] y (?L y)"
apply (prolog prog_Test)
done
schematic_goal "reverse [] ?L"
apply (prolog prog_Test)
done
schematic_goal "reverse [23] ?L"
apply (prolog prog_Test)
done
schematic_goal "reverse [23,24,?x] ?L"
apply (prolog prog_Test)
done
schematic_goal "reverse ?L [23,24,?x]"
apply (prolog prog_Test)
done
schematic_goal "mappred age ?x [23,24]"
apply (prolog prog_Test)
back
done
schematic_goal "mappred (\x y. \z. age z y) ?x [23,24]"
apply (prolog prog_Test)
done
schematic_goal "mappred ?P [bob,sue] [24,23]"
apply (prolog prog_Test)
done
schematic_goal "mapfun f [bob,bob,sue] [?x,?y,?z]"
apply (prolog prog_Test)
done
schematic_goal "mapfun (%x. h x 25) [bob,sue] ?L"
apply (prolog prog_Test)
done
schematic_goal "mapfun ?F [24,25] [h bob 24,h bob 25]"
apply (prolog prog_Test)
done
schematic_goal "mapfun ?F [24] [h 24 24]"
apply (prolog prog_Test)
back
back
back
done
lemma "True"
apply (prolog prog_Test)
done
schematic_goal "age ?x 24 & age ?y 23"
apply (prolog prog_Test)
back
done
schematic_goal "age ?x 24 | age ?x 23"
apply (prolog prog_Test)
back
back
done
lemma "\x y. age x y"
apply (prolog prog_Test)
done
lemma "\x y. append [] x x"
apply (prolog prog_Test)
done
schematic_goal "age sue 24 .. age bob 23 => age ?x ?y"
apply (prolog prog_Test)
back
back
back
back
done
(*set trace_DEPTH_FIRST;*)
lemma "age bob 25 :- age bob 24 => age bob 25"
apply (prolog prog_Test)
done
(*reset trace_DEPTH_FIRST;*)
schematic_goal "(\x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
apply (prolog prog_Test)
back
back
back
done
lemma "\x. \y. eq x y"
apply (prolog prog_Test)
done
schematic_goal "\P. P \ eq P ?x"
apply (prolog prog_Test)
(*
back
back
back
back
back
back
back
back
*)
done
lemma "\P. eq P (True & True) \ P"
apply (prolog prog_Test)
done
lemma "\P. eq P (\) \ P k True"
apply (prolog prog_Test)
done
lemma "\P. eq P (Q => True) \ P"
apply (prolog prog_Test)
done
(* P flexible: *)
lemma "(\P k l. P k l :- eq P Q) => Q a b"
apply (prolog prog_Test)
done
(*
loops:
lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
*)
(* implication and disjunction in atom: *)
lemma "\Q. (\p q. R(q :- p) => R(Q p q)) \ Q (t | s) (s | t)"
by fast
(* disjunction in atom: *)
lemma "(\P. g P :- (P => b \ a)) => g(a \ b)"
apply (tactic "step_tac (put_claset HOL_cs \<^context>) 1")
apply (tactic "step_tac (put_claset HOL_cs \<^context>) 1")
apply (tactic "step_tac (put_claset HOL_cs \<^context>) 1")
prefer 2
apply fast
apply fast
done
(*
hangs:
lemma "(!P. g P :- (P => b | a)) => g(a | b)"
by fast
*)
schematic_goal "\Emp Stk.(
empty (Emp::'b) ..
(\<forall>(X::nat) S. add X (S::'b) (Stk X S)) ..
(\<forall>(X::nat) S. remove X ((Stk X S)::'b) S))
=> bag_appl 23 24 ?X ?Y"
oops
schematic_goal "\Qu. (
(\<forall>L. empty (Qu L L)) ..
(\<forall>(X::nat) L K. add X (Qu L (X#K)) (Qu L K)) ..
(\<forall>(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
=> bag_appl 23 24 ?X ?Y"
oops
lemma "D \ (\y. E) :- (\x. True \ True) :- True => D"
apply (prolog prog_Test)
done
schematic_goal "P x .. P y => P ?X"
apply (prolog prog_Test)
back
done
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
