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