src/FOL/ex/Prolog.thy
author wenzelm
Fri Apr 23 23:35:43 2010 +0200 (2010-04-23)
changeset 36319 8feb2c4bef1a
parent 31974 e81979a703a4
child 41779 a68f503805ed
permissions -rw-r--r--
mark schematic statements explicitly;
     1 (*  Title:      FOL/ex/Prolog.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     4 *)
     5 
     6 header {* First-Order Logic: PROLOG examples *}
     7 
     8 theory Prolog
     9 imports FOL
    10 begin
    11 
    12 typedecl 'a list
    13 arities list :: ("term") "term"
    14 consts
    15   Nil     :: "'a list"
    16   Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60)
    17   app     :: "['a list, 'a list, 'a list] => o"
    18   rev     :: "['a list, 'a list] => o"
    19 axioms
    20   appNil:  "app(Nil,ys,ys)"
    21   appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
    22   revNil:  "rev(Nil,Nil)"
    23   revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
    24 
    25 schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
    26 apply (rule appNil appCons)
    27 apply (rule appNil appCons)
    28 apply (rule appNil appCons)
    29 apply (rule appNil appCons)
    30 done
    31 
    32 schematic_lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
    33 apply (rule appNil appCons)+
    34 done
    35 
    36 schematic_lemma "app(?x, ?y, a:b:c:d:Nil)"
    37 apply (rule appNil appCons)+
    38 back
    39 back
    40 back
    41 back
    42 done
    43 
    44 (*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
    45 (*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
    46 
    47 lemmas rules = appNil appCons revNil revCons
    48 
    49 schematic_lemma "rev(a:b:c:d:Nil, ?x)"
    50 apply (rule rules)+
    51 done
    52 
    53 schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
    54 apply (rule rules)+
    55 done
    56 
    57 schematic_lemma "rev(?x, a:b:c:Nil)"
    58 apply (rule rules)+  -- {* does not solve it directly! *}
    59 back
    60 back
    61 done
    62 
    63 (*backtracking version*)
    64 ML {*
    65 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1)
    66 *}
    67 
    68 schematic_lemma "rev(?x, a:b:c:Nil)"
    69 apply (tactic prolog_tac)
    70 done
    71 
    72 schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
    73 apply (tactic prolog_tac)
    74 done
    75 
    76 (*rev([a..p], ?w) requires 153 inferences *)
    77 schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
    78 apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
    79 done
    80 
    81 (*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
    82   total inferences = 2 + 1 + 17 + 561 = 581*)
    83 schematic_lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
    84 apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *})
    85 done
    86 
    87 end