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