src/LCF/LCF.thy
author wenzelm
Sat Sep 03 17:54:10 2005 +0200 (2005-09-03)
changeset 17248 81bf91654e73
parent 3837 d7f033c74b38
child 17249 e89fbfd778c1
permissions -rw-r--r--
converted to Isar theory format;
clasohm@1474
     1
(*  Title:      LCF/lcf.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1474
     3
    Author:     Tobias Nipkow
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
wenzelm@17248
     7
header {* LCF on top of First-Order Logic *}
clasohm@0
     8
wenzelm@17248
     9
theory LCF
wenzelm@17248
    10
imports FOL
wenzelm@17248
    11
uses ("pair.ML") ("fix.ML")
wenzelm@17248
    12
begin
clasohm@0
    13
wenzelm@17248
    14
text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
clasohm@0
    15
wenzelm@17248
    16
subsection {* Natural Deduction Rules for LCF *}
wenzelm@17248
    17
wenzelm@17248
    18
classes cpo < "term"
wenzelm@17248
    19
defaultsort cpo
wenzelm@17248
    20
wenzelm@17248
    21
typedecl tr
wenzelm@17248
    22
typedecl void
wenzelm@17248
    23
typedecl ('a,'b) "*"    (infixl 6)
wenzelm@17248
    24
typedecl ('a,'b) "+"    (infixl 5)
clasohm@0
    25
lcp@283
    26
arities
wenzelm@17248
    27
  fun :: (cpo, cpo) cpo
wenzelm@17248
    28
  "*" :: (cpo, cpo) cpo
wenzelm@17248
    29
  "+" :: (cpo, cpo) cpo
wenzelm@17248
    30
  tr :: cpo
wenzelm@17248
    31
  void :: cpo
clasohm@0
    32
clasohm@0
    33
consts
clasohm@1474
    34
 UU     :: "'a"
wenzelm@17248
    35
 TT     :: "tr"
wenzelm@17248
    36
 FF     :: "tr"
clasohm@1474
    37
 FIX    :: "('a => 'a) => 'a"
clasohm@1474
    38
 FST    :: "'a*'b => 'a"
clasohm@1474
    39
 SND    :: "'a*'b => 'b"
clasohm@0
    40
 INL    :: "'a => 'a+'b"
clasohm@0
    41
 INR    :: "'b => 'a+'b"
clasohm@0
    42
 WHEN   :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
clasohm@1474
    43
 adm    :: "('a => o) => o"
clasohm@1474
    44
 VOID   :: "void"               ("'(')")
clasohm@1474
    45
 PAIR   :: "['a,'b] => 'a*'b"   ("(1<_,/_>)" [0,0] 100)
clasohm@1474
    46
 COND   :: "[tr,'a,'a] => 'a"   ("(_ =>/ (_ |/ _))" [60,60,60] 60)
clasohm@1474
    47
 "<<"   :: "['a,'a] => o"       (infixl 50)
wenzelm@17248
    48
wenzelm@17248
    49
axioms
clasohm@0
    50
  (** DOMAIN THEORY **)
clasohm@0
    51
wenzelm@17248
    52
  eq_def:        "x=y == x << y & y << x"
clasohm@0
    53
wenzelm@17248
    54
  less_trans:    "[| x << y; y << z |] ==> x << z"
clasohm@0
    55
wenzelm@17248
    56
  less_ext:      "(ALL x. f(x) << g(x)) ==> f << g"
clasohm@0
    57
wenzelm@17248
    58
  mono:          "[| f << g; x << y |] ==> f(x) << g(y)"
clasohm@0
    59
wenzelm@17248
    60
  minimal:       "UU << x"
clasohm@0
    61
wenzelm@17248
    62
  FIX_eq:        "f(FIX(f)) = FIX(f)"
clasohm@0
    63
clasohm@0
    64
  (** TR **)
clasohm@0
    65
wenzelm@17248
    66
  tr_cases:      "p=UU | p=TT | p=FF"
clasohm@0
    67
wenzelm@17248
    68
  not_TT_less_FF: "~ TT << FF"
wenzelm@17248
    69
  not_FF_less_TT: "~ FF << TT"
wenzelm@17248
    70
  not_TT_less_UU: "~ TT << UU"
wenzelm@17248
    71
  not_FF_less_UU: "~ FF << UU"
clasohm@0
    72
wenzelm@17248
    73
  COND_UU:       "UU => x | y  =  UU"
wenzelm@17248
    74
  COND_TT:       "TT => x | y  =  x"
wenzelm@17248
    75
  COND_FF:       "FF => x | y  =  y"
clasohm@0
    76
clasohm@0
    77
  (** PAIRS **)
clasohm@0
    78
wenzelm@17248
    79
  surj_pairing:  "<FST(z),SND(z)> = z"
clasohm@0
    80
wenzelm@17248
    81
  FST:   "FST(<x,y>) = x"
wenzelm@17248
    82
  SND:   "SND(<x,y>) = y"
clasohm@0
    83
clasohm@0
    84
  (*** STRICT SUM ***)
clasohm@0
    85
wenzelm@17248
    86
  INL_DEF: "~x=UU ==> ~INL(x)=UU"
wenzelm@17248
    87
  INR_DEF: "~x=UU ==> ~INR(x)=UU"
clasohm@0
    88
wenzelm@17248
    89
  INL_STRICT: "INL(UU) = UU"
wenzelm@17248
    90
  INR_STRICT: "INR(UU) = UU"
clasohm@0
    91
wenzelm@17248
    92
  WHEN_UU:  "WHEN(f,g,UU) = UU"
wenzelm@17248
    93
  WHEN_INL: "~x=UU ==> WHEN(f,g,INL(x)) = f(x)"
wenzelm@17248
    94
  WHEN_INR: "~x=UU ==> WHEN(f,g,INR(x)) = g(x)"
clasohm@0
    95
wenzelm@17248
    96
  SUM_EXHAUSTION:
clasohm@0
    97
    "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))"
clasohm@0
    98
clasohm@0
    99
  (** VOID **)
clasohm@0
   100
wenzelm@17248
   101
  void_cases:    "(x::void) = UU"
clasohm@0
   102
clasohm@0
   103
  (** INDUCTION **)
clasohm@0
   104
wenzelm@17248
   105
  induct:        "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
clasohm@0
   106
clasohm@0
   107
  (** Admissibility / Chain Completeness **)
clasohm@0
   108
  (* All rules can be found on pages 199--200 of Larry's LCF book.
clasohm@0
   109
     Note that "easiness" of types is not taken into account
clasohm@0
   110
     because it cannot be expressed schematically; flatness could be. *)
clasohm@0
   111
wenzelm@17248
   112
  adm_less:      "adm(%x. t(x) << u(x))"
wenzelm@17248
   113
  adm_not_less:  "adm(%x.~ t(x) << u)"
wenzelm@17248
   114
  adm_not_free:  "adm(%x. A)"
wenzelm@17248
   115
  adm_subst:     "adm(P) ==> adm(%x. P(t(x)))"
wenzelm@17248
   116
  adm_conj:      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
wenzelm@17248
   117
  adm_disj:      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
wenzelm@17248
   118
  adm_imp:       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
wenzelm@17248
   119
  adm_all:       "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
wenzelm@17248
   120
wenzelm@17248
   121
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17248
   122
wenzelm@17248
   123
use "LCF_lemmas.ML"
wenzelm@17248
   124
wenzelm@17248
   125
wenzelm@17248
   126
subsection {* Ordered pairs and products *}
wenzelm@17248
   127
wenzelm@17248
   128
use "pair.ML"
wenzelm@17248
   129
wenzelm@17248
   130
wenzelm@17248
   131
subsection {* Fixedpoint theory *}
wenzelm@17248
   132
wenzelm@17248
   133
use "fix.ML"
wenzelm@17248
   134
clasohm@0
   135
end