src/HOL/Prolog/Test.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     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