1(*  Title:    HOL/Prolog/Test.thy
2    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
3*)
4
5section \<open>Basic examples\<close>
6
7theory Test
8imports HOHH
9begin
10
11typedecl nat
12
13typedecl 'a list
14
15consts
16  Nil   :: "'a list"                                  ("[]")
17  Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
18
19syntax
20  (* list Enumeration *)
21  "_list"     :: "args => 'a list"                          ("[(_)]")
22
23translations
24  "[x, xs]"     == "x#[xs]"
25  "[x]"         == "x#[]"
26
27typedecl person
28
29axiomatization
30  append  :: "['a list, 'a list, 'a list]            => bool" and
31  reverse :: "['a list, 'a list]                     => bool" and
32
33  mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool" and
34  mapfun  :: "[('a => 'b), 'a list, 'b list]         => bool" and
35
36  bob     :: person and
37  sue     :: person and
38  ned     :: person and
39
40  nat23   :: nat          ("23") and
41  nat24   :: nat          ("24") and
42  nat25   :: nat          ("25") and
43
44  age     :: "[person, nat]                          => bool" and
45
46  eq      :: "['a, 'a]                               => bool" and
47
48  empty   :: "['b]                                   => bool" and
49  add     :: "['a, 'b, 'b]                           => bool" and
50  remove  :: "['a, 'b, 'b]                           => bool" and
51  bag_appl:: "['a, 'a, 'a, 'a]                       => bool"
52where
53        append:  "\<And>x xs ys zs. append  []    xs  xs    ..
54                  append (x#xs) ys (x#zs) :- append xs ys zs" and
55        reverse: "\<And>L1 L2. reverse L1 L2 :- (\<forall>rev_aux.
56                  (\<forall>L.          rev_aux  []    L  L )..
57                  (\<forall>X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3))
58                  => rev_aux L1 L2 [])" and
59
60        mappred: "\<And>x xs y ys P. mappred P  []     []    ..
61                  mappred P (x#xs) (y#ys) :- P x y  &  mappred P xs ys" and
62        mapfun:  "\<And>x xs ys f. mapfun f  []     []      ..
63                  mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" and
64
65        age:     "age bob 24 ..
66                  age sue 23 ..
67                  age ned 23" and
68
69        eq:      "\<And>x. eq x x" and
70
71(* actual definitions of empty and add is hidden -> yields abstract data type *)
72
73        bag_appl: "\<And>A B X Y. bag_appl A B X Y:- (\<exists>S1 S2 S3 S4 S5.
74                                empty    S1    &
75                                add A    S1 S2 &
76                                add B    S2 S3 &
77                                remove X S3 S4 &
78                                remove Y S4 S5 &
79                                empty    S5)"
80
81lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
82
83schematic_goal "append ?x ?y [a,b,c,d]"
84  apply (prolog prog_Test)
85  back
86  back
87  back
88  back
89  done
90
91schematic_goal "append [a,b] y ?L"
92  apply (prolog prog_Test)
93  done
94
95schematic_goal "\<forall>y. append [a,b] y (?L y)"
96  apply (prolog prog_Test)
97  done
98
99schematic_goal "reverse [] ?L"
100  apply (prolog prog_Test)
101  done
102
103schematic_goal "reverse [23] ?L"
104  apply (prolog prog_Test)
105  done
106
107schematic_goal "reverse [23,24,?x] ?L"
108  apply (prolog prog_Test)
109  done
110
111schematic_goal "reverse ?L [23,24,?x]"
112  apply (prolog prog_Test)
113  done
114
115schematic_goal "mappred age ?x [23,24]"
116  apply (prolog prog_Test)
117  back
118  done
119
120schematic_goal "mappred (\<lambda>x y. \<exists>z. age z y) ?x [23,24]"
121  apply (prolog prog_Test)
122  done
123
124schematic_goal "mappred ?P [bob,sue] [24,23]"
125  apply (prolog prog_Test)
126  done
127
128schematic_goal "mapfun f [bob,bob,sue] [?x,?y,?z]"
129  apply (prolog prog_Test)
130  done
131
132schematic_goal "mapfun (%x. h x 25) [bob,sue] ?L"
133  apply (prolog prog_Test)
134  done
135
136schematic_goal "mapfun ?F [24,25] [h bob 24,h bob 25]"
137  apply (prolog prog_Test)
138  done
139
140schematic_goal "mapfun ?F [24] [h 24 24]"
141  apply (prolog prog_Test)
142  back
143  back
144  back
145  done
146
147lemma "True"
148  apply (prolog prog_Test)
149  done
150
151schematic_goal "age ?x 24 & age ?y 23"
152  apply (prolog prog_Test)
153  back
154  done
155
156schematic_goal "age ?x 24 | age ?x 23"
157  apply (prolog prog_Test)
158  back
159  back
160  done
161
162lemma "\<exists>x y. age x y"
163  apply (prolog prog_Test)
164  done
165
166lemma "\<forall>x y. append [] x x"
167  apply (prolog prog_Test)
168  done
169
170schematic_goal "age sue 24 .. age bob 23 => age ?x ?y"
171  apply (prolog prog_Test)
172  back
173  back
174  back
175  back
176  done
177
178(*set trace_DEPTH_FIRST;*)
179lemma "age bob 25 :- age bob 24 => age bob 25"
180  apply (prolog prog_Test)
181  done
182(*reset trace_DEPTH_FIRST;*)
183
184schematic_goal "(\<forall>x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"
185  apply (prolog prog_Test)
186  back
187  back
188  back
189  done
190
191lemma "\<forall>x. \<exists>y. eq x y"
192  apply (prolog prog_Test)
193  done
194
195schematic_goal "\<exists>P. P \<and> eq P ?x"
196  apply (prolog prog_Test)
197(*
198  back
199  back
200  back
201  back
202  back
203  back
204  back
205  back
206*)
207  done
208
209lemma "\<exists>P. eq P (True & True) \<and> P"
210  apply (prolog prog_Test)
211  done
212
213lemma "\<exists>P. eq P (\<or>) \<and> P k True"
214  apply (prolog prog_Test)
215  done
216
217lemma "\<exists>P. eq P (Q => True) \<and> P"
218  apply (prolog prog_Test)
219  done
220
221(* P flexible: *)
222lemma "(\<forall>P k l. P k l :- eq P Q) => Q a b"
223  apply (prolog prog_Test)
224  done
225(*
226loops:
227lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
228*)
229
230(* implication and disjunction in atom: *)
231lemma "\<exists>Q. (\<forall>p q. R(q :- p) => R(Q p q)) \<and> Q (t | s) (s | t)"
232  by fast
233
234(* disjunction in atom: *)
235lemma "(\<forall>P. g P :- (P => b \<or> a)) => g(a \<or> b)"
236  apply (tactic "step_tac (put_claset HOL_cs \<^context>) 1")
237  apply (tactic "step_tac (put_claset HOL_cs \<^context>) 1")
238  apply (tactic "step_tac (put_claset HOL_cs \<^context>) 1")
239   prefer 2
240   apply fast
241  apply fast
242  done
243
244(*
245hangs:
246lemma "(!P. g P :- (P => b | a)) => g(a | b)"
247  by fast
248*)
249
250schematic_goal "\<forall>Emp Stk.(
251                       empty    (Emp::'b) .. 
252         (\<forall>(X::nat) S. add    X (S::'b)         (Stk X S)) .. 
253         (\<forall>(X::nat) S. remove X ((Stk X S)::'b) S))
254 => bag_appl 23 24 ?X ?Y"
255  oops
256
257schematic_goal "\<forall>Qu. ( 
258          (\<forall>L.            empty    (Qu L L)) .. 
259          (\<forall>(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
260          (\<forall>(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
261 => bag_appl 23 24 ?X ?Y"
262  oops
263
264lemma "D \<and> (\<forall>y. E) :- (\<forall>x. True \<and> True) :- True => D"
265  apply (prolog prog_Test)
266  done
267
268schematic_goal "P x .. P y => P ?X"
269  apply (prolog prog_Test)
270  back
271  done
272
273end
274