src/HOL/Prolog/Test.thy
 author wenzelm Thu May 26 17:51:22 2016 +0200 (2016-05-26) changeset 63167 0909deb8059b parent 61337 4645502c3c64 child 67399 eab6ce8368fa permissions -rw-r--r--
isabelle update_cartouches -c -t;
```     1 (*  Title:    HOL/Prolog/Test.thy
```
```     2     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
```
```     3 *)
```
```     4
```
```     5 section \<open>Basic examples\<close>
```
```     6
```
```     7 theory Test
```
```     8 imports HOHH
```
```     9 begin
```
```    10
```
```    11 typedecl nat
```
```    12
```
```    13 typedecl 'a list
```
```    14
```
```    15 consts
```
```    16   Nil   :: "'a list"                                  ("[]")
```
```    17   Cons  :: "'a => 'a list => 'a list"                 (infixr "#"  65)
```
```    18
```
```    19 syntax
```
```    20   (* list Enumeration *)
```
```    21   "_list"     :: "args => 'a list"                          ("[(_)]")
```
```    22
```
```    23 translations
```
```    24   "[x, xs]"     == "x#[xs]"
```
```    25   "[x]"         == "x#[]"
```
```    26
```
```    27 typedecl person
```
```    28
```
```    29 axiomatization
```
```    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"
```
```    52 where
```
```    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 :- (!rev_aux.
```
```    56                   (!L.          rev_aux  []    L  L )..
```
```    57                   (!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:- (? 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
```
```    81 lemmas prog_Test = append reverse mappred mapfun age eq bag_appl
```
```    82
```
```    83 schematic_goal "append ?x ?y [a,b,c,d]"
```
```    84   apply (prolog prog_Test)
```
```    85   back
```
```    86   back
```
```    87   back
```
```    88   back
```
```    89   done
```
```    90
```
```    91 schematic_goal "append [a,b] y ?L"
```
```    92   apply (prolog prog_Test)
```
```    93   done
```
```    94
```
```    95 schematic_goal "!y. append [a,b] y (?L y)"
```
```    96   apply (prolog prog_Test)
```
```    97   done
```
```    98
```
```    99 schematic_goal "reverse [] ?L"
```
```   100   apply (prolog prog_Test)
```
```   101   done
```
```   102
```
```   103 schematic_goal "reverse [23] ?L"
```
```   104   apply (prolog prog_Test)
```
```   105   done
```
```   106
```
```   107 schematic_goal "reverse [23,24,?x] ?L"
```
```   108   apply (prolog prog_Test)
```
```   109   done
```
```   110
```
```   111 schematic_goal "reverse ?L [23,24,?x]"
```
```   112   apply (prolog prog_Test)
```
```   113   done
```
```   114
```
```   115 schematic_goal "mappred age ?x [23,24]"
```
```   116   apply (prolog prog_Test)
```
```   117   back
```
```   118   done
```
```   119
```
```   120 schematic_goal "mappred (%x y. ? z. age z y) ?x [23,24]"
```
```   121   apply (prolog prog_Test)
```
```   122   done
```
```   123
```
```   124 schematic_goal "mappred ?P [bob,sue] [24,23]"
```
```   125   apply (prolog prog_Test)
```
```   126   done
```
```   127
```
```   128 schematic_goal "mapfun f [bob,bob,sue] [?x,?y,?z]"
```
```   129   apply (prolog prog_Test)
```
```   130   done
```
```   131
```
```   132 schematic_goal "mapfun (%x. h x 25) [bob,sue] ?L"
```
```   133   apply (prolog prog_Test)
```
```   134   done
```
```   135
```
```   136 schematic_goal "mapfun ?F [24,25] [h bob 24,h bob 25]"
```
```   137   apply (prolog prog_Test)
```
```   138   done
```
```   139
```
```   140 schematic_goal "mapfun ?F [24] [h 24 24]"
```
```   141   apply (prolog prog_Test)
```
```   142   back
```
```   143   back
```
```   144   back
```
```   145   done
```
```   146
```
```   147 lemma "True"
```
```   148   apply (prolog prog_Test)
```
```   149   done
```
```   150
```
```   151 schematic_goal "age ?x 24 & age ?y 23"
```
```   152   apply (prolog prog_Test)
```
```   153   back
```
```   154   done
```
```   155
```
```   156 schematic_goal "age ?x 24 | age ?x 23"
```
```   157   apply (prolog prog_Test)
```
```   158   back
```
```   159   back
```
```   160   done
```
```   161
```
```   162 lemma "? x y. age x y"
```
```   163   apply (prolog prog_Test)
```
```   164   done
```
```   165
```
```   166 lemma "!x y. append [] x x"
```
```   167   apply (prolog prog_Test)
```
```   168   done
```
```   169
```
```   170 schematic_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;*)
```
```   179 lemma "age bob 25 :- age bob 24 => age bob 25"
```
```   180   apply (prolog prog_Test)
```
```   181   done
```
```   182 (*reset trace_DEPTH_FIRST;*)
```
```   183
```
```   184 schematic_goal "(!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
```
```   191 lemma "!x. ? y. eq x y"
```
```   192   apply (prolog prog_Test)
```
```   193   done
```
```   194
```
```   195 schematic_goal "? P. P & 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
```
```   209 lemma "? P. eq P (True & True) & P"
```
```   210   apply (prolog prog_Test)
```
```   211   done
```
```   212
```
```   213 lemma "? P. eq P op | & P k True"
```
```   214   apply (prolog prog_Test)
```
```   215   done
```
```   216
```
```   217 lemma "? P. eq P (Q => True) & P"
```
```   218   apply (prolog prog_Test)
```
```   219   done
```
```   220
```
```   221 (* P flexible: *)
```
```   222 lemma "(!P k l. P k l :- eq P Q) => Q a b"
```
```   223   apply (prolog prog_Test)
```
```   224   done
```
```   225 (*
```
```   226 loops:
```
```   227 lemma "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"
```
```   228 *)
```
```   229
```
```   230 (* implication and disjunction in atom: *)
```
```   231 lemma "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"
```
```   232   by fast
```
```   233
```
```   234 (* disjunction in atom: *)
```
```   235 lemma "(!P. g P :- (P => b | a)) => g(a | 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 (*
```
```   245 hangs:
```
```   246 lemma "(!P. g P :- (P => b | a)) => g(a | b)"
```
```   247   by fast
```
```   248 *)
```
```   249
```
```   250 schematic_goal "!Emp Stk.(
```
```   251                        empty    (Emp::'b) ..
```
```   252          (!(X::nat) S. add    X (S::'b)         (Stk X S)) ..
```
```   253          (!(X::nat) S. remove X ((Stk X S)::'b) S))
```
```   254  => bag_appl 23 24 ?X ?Y"
```
```   255   oops
```
```   256
```
```   257 schematic_goal "!Qu. (
```
```   258           (!L.            empty    (Qu L L)) ..
```
```   259           (!(X::nat) L K. add    X (Qu L (X#K)) (Qu L K)) ..
```
```   260           (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))
```
```   261  => bag_appl 23 24 ?X ?Y"
```
```   262   oops
```
```   263
```
```   264 lemma "D & (!y. E) :- (!x. True & True) :- True => D"
```
```   265   apply (prolog prog_Test)
```
```   266   done
```
```   267
```
```   268 schematic_goal "P x .. P y => P ?X"
```
```   269   apply (prolog prog_Test)
```
```   270   back
```
```   271   done
```
```   272
```
```   273 end
```