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