src/FOL/ex/Prolog.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 19819 14de4d05d275
child 26287 df8e5362cff9
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1473
e8d4606e6502 expanded tabs
clasohm
parents: 1322
diff changeset
     1
(*  Title:      FOL/ex/prolog.thy
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1473
e8d4606e6502 expanded tabs
clasohm
parents: 1322
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
     7
header {* First-Order Logic: PROLOG examples *}
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
     8
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
     9
theory Prolog
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    10
imports FOL
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    11
begin
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    12
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    13
typedecl 'a list
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    14
arities list :: ("term") "term"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    15
consts
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    16
  Nil     :: "'a list"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    17
  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60)
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    18
  app     :: "['a list, 'a list, 'a list] => o"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    19
  rev     :: "['a list, 'a list] => o"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    20
axioms
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    21
  appNil:  "app(Nil,ys,ys)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    22
  appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    23
  revNil:  "rev(Nil,Nil)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    24
  revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    25
19819
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    26
lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    27
apply (rule appNil appCons)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    28
apply (rule appNil appCons)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    29
apply (rule appNil appCons)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    30
apply (rule appNil appCons)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    31
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    32
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    33
lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    34
apply (rule appNil appCons)+
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    35
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    36
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    37
lemma "app(?x, ?y, a:b:c:d:Nil)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    38
apply (rule appNil appCons)+
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    39
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    40
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    41
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    42
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    43
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    44
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    45
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    46
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    47
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    48
lemmas rules = appNil appCons revNil revCons
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    49
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    50
lemma "rev(a:b:c:d:Nil, ?x)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    51
apply (rule rules)+
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    52
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    53
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    54
lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    55
apply (rule rules)+
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    56
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    57
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    58
lemma "rev(?x, a:b:c:Nil)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    59
apply (rule rules)+  -- {* does not solve it directly! *}
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    60
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    61
back
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    62
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    63
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    64
(*backtracking version*)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    65
ML {*
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    66
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    67
*}
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    68
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    69
lemma "rev(?x, a:b:c:Nil)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    70
apply (tactic prolog_tac)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    71
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    72
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    73
lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    74
apply (tactic prolog_tac)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    75
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    76
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    77
(*rev([a..p], ?w) requires 153 inferences *)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    78
lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    79
apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    80
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    81
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    82
(*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    83
  total inferences = 2 + 1 + 17 + 561 = 581*)
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    84
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)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    85
apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})
14de4d05d275 removed obsolete ML files;
wenzelm
parents: 17245
diff changeset
    86
done
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 1473
diff changeset
    87
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
end