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