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