# HG changeset patch # User clasohm # Date 823527849 -3600 # Node ID 3f7d67927fe2d18fbf9de27480a3117bfe7d6f19 # Parent e8d4606e6502e5d26bf1dad4abb51f20190fd272 expanded tabs diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/CCL.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/ccl.thy +(* Title: CCL/ccl.thy ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1993 University of Cambridge Classical Computational Logic for Untyped Lambda Calculus with reduction to diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Fix.thy --- a/src/CCL/Fix.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Fix.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/Lazy/fix.thy +(* Title: CCL/Lazy/fix.thy ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1993 University of Cambridge Tentative attempt at including fixed point induction. @@ -11,7 +11,7 @@ consts - idgen :: "[i]=>i" + idgen :: "[i]=>i" INCL :: "[i=>o]=>o" rules diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Gfp.thy --- a/src/CCL/Gfp.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Gfp.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/gfp.thy +(* Title: HOL/gfp.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Greatest fixed points diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Hered.thy --- a/src/CCL/Hered.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Hered.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/hered.thy +(* Title: CCL/hered.thy ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1993 University of Cambridge Hereditary Termination - cf. Martin Lo\"f diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Lfp.thy --- a/src/CCL/Lfp.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Lfp.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: HOL/lfp.thy +(* Title: HOL/lfp.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge The Knaster-Tarski Theorem diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Term.thy --- a/src/CCL/Term.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Term.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/terms.thy +(* Title: CCL/terms.thy ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1993 University of Cambridge Definitions of usual program constructs in CCL. @@ -38,16 +38,16 @@ letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" - [0,0,60] 60) + [0,0,60] 60) "@letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" - [0,0,0,60] 60) + [0,0,0,60] 60) "@letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" - [0,0,0,0,60] 60) + [0,0,0,0,60] 60) "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" - [0,0,0,0,0,60] 60) + [0,0,0,0,0,60] 60) napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) @@ -66,7 +66,7 @@ succ_def "succ(n) == inr(n)" ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))" nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)" - nil_def "[] == inl(one)" + nil_def "[] == inl(one)" cons_def "h$t == inr()" lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))" lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)" diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Trancl.thy --- a/src/CCL/Trancl.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Trancl.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/trancl.thy +(* Title: CCL/trancl.thy ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Transitive closure of a relation @@ -9,20 +9,20 @@ Trancl = CCL + consts - trans :: "i set => o" (*transitivity predicate*) - id :: "i set" - rtrancl :: "i set => i set" ("(_^*)" [100] 100) - trancl :: "i set => i set" ("(_^+)" [100] 100) - O :: "[i set,i set] => i set" (infixr 60) + trans :: "i set => o" (*transitivity predicate*) + id :: "i set" + rtrancl :: "i set => i set" ("(_^*)" [100] 100) + trancl :: "i set => i set" ("(_^+)" [100] 100) + O :: "[i set,i set] => i set" (infixr 60) rules -trans_def "trans(r) == (ALL x y z. :r --> :r --> :r)" -comp_def (*composition of relations*) - "r O s == {xz. EX x y z. xz = & :s & :r}" -id_def (*the identity relation*) - "id == {p. EX x. p = }" -rtrancl_def "r^* == lfp(%s. id Un (r O s))" -trancl_def "r^+ == r O rtrancl(r)" +trans_def "trans(r) == (ALL x y z. :r --> :r --> :r)" +comp_def (*composition of relations*) + "r O s == {xz. EX x y z. xz = & :s & :r}" +id_def (*the identity relation*) + "id == {p. EX x. p = }" +rtrancl_def "r^* == lfp(%s. id Un (r O s))" +trancl_def "r^+ == r O rtrancl(r)" end diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Type.thy --- a/src/CCL/Type.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Type.thy Mon Feb 05 14:44:09 1996 +0100 @@ -28,10 +28,10 @@ SPLIT :: "[i, [i, i] => i set] => i set" "@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" - [0,0,60] 60) + [0,0,60] 60) "@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" - [0,0,60] 60) + [0,0,60] 60) "@->" :: "[i set, i set] => i set" ("(_ ->/ _)" [54, 53] 53) "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/Wfd.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/wfd.thy +(* Title: CCL/wfd.thy ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Well-founded relations in CCL. diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/ex/Flag.thy --- a/src/CCL/ex/Flag.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/ex/Flag.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/ex/flag.thy +(* Title: CCL/ex/flag.thy ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Dutch national flag program - except that the point of Dijkstra's example was to use diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/ex/List.thy --- a/src/CCL/ex/List.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/ex/List.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/ex/list.thy +(* Title: CCL/ex/list.thy ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Programs defined over lists. diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/ex/Nat.thy --- a/src/CCL/ex/Nat.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/ex/Nat.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/ex/nat.thy +(* Title: CCL/ex/nat.thy ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Programs defined over the natural numbers diff -r e8d4606e6502 -r 3f7d67927fe2 src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CCL/ex/Stream.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CCL/ex/stream.thy +(* Title: CCL/ex/stream.thy ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory + Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Programs defined over streams. diff -r e8d4606e6502 -r 3f7d67927fe2 src/CTT/Arith.thy --- a/src/CTT/Arith.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CTT/Arith.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CTT/arith +(* Title: CTT/arith ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Arithmetic operators and their definitions @@ -11,8 +11,8 @@ Arith = CTT + -consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) - "#*",div,mod :: "[i,i]=>i" (infixr 70) +consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) + "#*",div,mod :: "[i,i]=>i" (infixr 70) rules add_def "a#+b == rec(a, b, %u v.succ(v))" diff -r e8d4606e6502 -r 3f7d67927fe2 src/CTT/Bool.thy --- a/src/CTT/Bool.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/CTT/Bool.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: CTT/bool +(* Title: CTT/bool ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge The two-element type (booleans and conditionals) @@ -8,12 +8,12 @@ Bool = CTT + -consts Bool :: "t" - true,false :: "i" - cond :: "[i,i,i]=>i" +consts Bool :: "t" + true,false :: "i" + cond :: "[i,i,i]=>i" rules - Bool_def "Bool == T+T" - true_def "true == inl(tt)" - false_def "false == inr(tt)" - cond_def "cond(a,b,c) == when(a, %u.b, %u.c)" + Bool_def "Bool == T+T" + true_def "true == inl(tt)" + false_def "false == inr(tt)" + cond_def "cond(a,b,c) == when(a, %u.b, %u.c)" end diff -r e8d4606e6502 -r 3f7d67927fe2 src/LCF/LCF.thy --- a/src/LCF/LCF.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/LCF/LCF.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: LCF/lcf.thy +(* Title: LCF/lcf.thy ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1992 University of Cambridge Natural Deduction Rules for LCF @@ -15,61 +15,61 @@ types tr void - ('a,'b) "*" (infixl 6) - ('a,'b) "+" (infixl 5) + ('a,'b) "*" (infixl 6) + ('a,'b) "+" (infixl 5) arities fun, "*", "+" :: (cpo,cpo)cpo tr,void :: cpo consts - UU :: "'a" - TT,FF :: "tr" - FIX :: "('a => 'a) => 'a" - FST :: "'a*'b => 'a" - SND :: "'a*'b => 'b" + UU :: "'a" + TT,FF :: "tr" + FIX :: "('a => 'a) => 'a" + FST :: "'a*'b => 'a" + SND :: "'a*'b => 'b" INL :: "'a => 'a+'b" INR :: "'b => 'a+'b" WHEN :: "['a=>'c, 'b=>'c, 'a+'b] => 'c" - adm :: "('a => o) => o" - VOID :: "void" ("'(')") - PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) - COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) - "<<" :: "['a,'a] => o" (infixl 50) + adm :: "('a => o) => o" + VOID :: "void" ("'(')") + PAIR :: "['a,'b] => 'a*'b" ("(1<_,/_>)" [0,0] 100) + COND :: "[tr,'a,'a] => 'a" ("(_ =>/ (_ |/ _))" [60,60,60] 60) + "<<" :: "['a,'a] => o" (infixl 50) rules (** DOMAIN THEORY **) - eq_def "x=y == x << y & y << x" + eq_def "x=y == x << y & y << x" - less_trans "[| x << y; y << z |] ==> x << z" + less_trans "[| x << y; y << z |] ==> x << z" - less_ext "(ALL x. f(x) << g(x)) ==> f << g" + less_ext "(ALL x. f(x) << g(x)) ==> f << g" - mono "[| f << g; x << y |] ==> f(x) << g(y)" + mono "[| f << g; x << y |] ==> f(x) << g(y)" - minimal "UU << x" + minimal "UU << x" - FIX_eq "f(FIX(f)) = FIX(f)" + FIX_eq "f(FIX(f)) = FIX(f)" (** TR **) - tr_cases "p=UU | p=TT | p=FF" + tr_cases "p=UU | p=TT | p=FF" not_TT_less_FF "~ TT << FF" not_FF_less_TT "~ FF << TT" not_TT_less_UU "~ TT << UU" not_FF_less_UU "~ FF << UU" - COND_UU "UU => x | y = UU" - COND_TT "TT => x | y = x" - COND_FF "FF => x | y = y" + COND_UU "UU => x | y = UU" + COND_TT "TT => x | y = x" + COND_FF "FF => x | y = y" (** PAIRS **) - surj_pairing " = z" + surj_pairing " = z" - FST "FST() = x" - SND "SND() = y" + FST "FST() = x" + SND "SND() = y" (*** STRICT SUM ***) @@ -88,23 +88,23 @@ (** VOID **) - void_cases "(x::void) = UU" + void_cases "(x::void) = UU" (** INDUCTION **) - induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" + induct "[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))" (** Admissibility / Chain Completeness **) (* All rules can be found on pages 199--200 of Larry's LCF book. Note that "easiness" of types is not taken into account because it cannot be expressed schematically; flatness could be. *) - adm_less "adm(%x.t(x) << u(x))" - adm_not_less "adm(%x.~ t(x) << u)" + adm_less "adm(%x.t(x) << u(x))" + adm_not_less "adm(%x.~ t(x) << u)" adm_not_free "adm(%x.A)" - adm_subst "adm(P) ==> adm(%x.P(t(x)))" - adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))" - adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))" - adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))" - adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))" + adm_subst "adm(P) ==> adm(%x.P(t(x)))" + adm_conj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))" + adm_disj "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))" + adm_imp "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))" + adm_all "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))" end diff -r e8d4606e6502 -r 3f7d67927fe2 src/LK/LK.thy --- a/src/LK/LK.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/LK/LK.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: LK/lk.thy +(* Title: LK/lk.thy ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge Classical First-Order Sequent Calculus @@ -19,51 +19,51 @@ o :: logic consts - True,False :: "o" - "=" :: "['a,'a] => o" (infixl 50) - "Not" :: "o => o" ("~ _" [40] 40) - "&" :: "[o,o] => o" (infixr 35) - "|" :: "[o,o] => o" (infixr 30) - "-->","<->" :: "[o,o] => o" (infixr 25) - The :: "('a => o) => 'a" (binder "THE " 10) - All :: "('a => o) => o" (binder "ALL " 10) - Ex :: "('a => o) => o" (binder "EX " 10) + True,False :: "o" + "=" :: "['a,'a] => o" (infixl 50) + "Not" :: "o => o" ("~ _" [40] 40) + "&" :: "[o,o] => o" (infixr 35) + "|" :: "[o,o] => o" (infixr 30) + "-->","<->" :: "[o,o] => o" (infixr 25) + The :: "('a => o) => 'a" (binder "THE " 10) + All :: "('a => o) => o" (binder "ALL " 10) + Ex :: "('a => o) => o" (binder "EX " 10) (*Representation of sequents*) - Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop" - Seqof :: "o => sobj=>sobj" - "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5) - "@MtSeq" :: "sequence" ("" [] 1000) - "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000) - "@MtSeqCont" :: "seqcont" ("" [] 1000) - "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000) - "" :: "o => seqobj" ("_" [] 1000) - "@SeqId" :: "id => seqobj" ("$_" [] 1000) - "@SeqVar" :: "var => seqobj" ("$_") + Trueprop :: "[sobj=>sobj,sobj=>sobj] => prop" + Seqof :: "o => sobj=>sobj" + "@Trueprop" :: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5) + "@MtSeq" :: "sequence" ("" [] 1000) + "@NmtSeq" :: "[seqobj,seqcont] => sequence" ("__" [] 1000) + "@MtSeqCont" :: "seqcont" ("" [] 1000) + "@SeqCont" :: "[seqobj,seqcont] => seqcont" (",/ __" [] 1000) + "" :: "o => seqobj" ("_" [] 1000) + "@SeqId" :: "id => seqobj" ("$_" [] 1000) + "@SeqVar" :: "var => seqobj" ("$_") rules (*Structural rules*) - basic "$H, P, $G |- $E, P, $F" + basic "$H, P, $G |- $E, P, $F" - thinR "$H |- $E, $F ==> $H |- $E, P, $F" - thinL "$H, $G |- $E ==> $H, P, $G |- $E" + thinR "$H |- $E, $F ==> $H |- $E, P, $F" + thinL "$H, $G |- $E ==> $H, P, $G |- $E" - cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" + cut "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" (*Propositional rules*) - conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" - conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" + conjR "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" + conjL "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" - disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" - disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" + disjR "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" + disjL "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" - impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" - impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" + impR "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" + impL "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" - notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F" - notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E" + notR "$H, P |- $E, $F ==> $H |- $E, ~P, $F" + notL "$H, $G |- $E, P ==> $H, ~P, $G |- $E" FalseL "$H, False, $G |- $E" @@ -72,15 +72,15 @@ (*Quantifiers*) - allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F" - allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E" + allR "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F" + allL "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E" - exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F" - exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E" + exR "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F" + exL "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E" (*Equality*) - refl "$H |- $E, a=a, $F" + refl "$H |- $E, a=a, $F" sym "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F" trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F" diff -r e8d4606e6502 -r 3f7d67927fe2 src/Modal/Modal0.thy --- a/src/Modal/Modal0.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/Modal/Modal0.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,24 +1,24 @@ -(* Title: 91/Modal/modal0 +(* Title: 91/Modal/modal0 ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1991 University of Cambridge *) Modal0 = LK + consts - box :: "o=>o" ("[]_" [50] 50) - dia :: "o=>o" ("<>_" [50] 50) - "--<",">-<" :: "[o,o]=>o" (infixr 25) - "@Lstar" :: "[sequence,sequence]=>prop" ("(_)|L>(_)" [6,6] 5) - "@Rstar" :: "[sequence,sequence]=>prop" ("(_)|R>(_)" [6,6] 5) - Lstar,Rstar :: "[sobj=>sobj,sobj=>sobj]=>prop" + box :: "o=>o" ("[]_" [50] 50) + dia :: "o=>o" ("<>_" [50] 50) + "--<",">-<" :: "[o,o]=>o" (infixr 25) + "@Lstar" :: "[sequence,sequence]=>prop" ("(_)|L>(_)" [6,6] 5) + "@Rstar" :: "[sequence,sequence]=>prop" ("(_)|R>(_)" [6,6] 5) + Lstar,Rstar :: "[sobj=>sobj,sobj=>sobj]=>prop" rules (* Definitions *) - strimp_def "P --< Q == [](P --> Q)" - streqv_def "P >-< Q == (P --< Q) & (Q --< P)" + strimp_def "P --< Q == [](P --> Q)" + streqv_def "P >-< Q == (P --< Q) & (Q --< P)" end ML diff -r e8d4606e6502 -r 3f7d67927fe2 src/Modal/S4.thy --- a/src/Modal/S4.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/Modal/S4.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: 91/Modal/S4 +(* Title: 91/Modal/S4 ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1991 University of Cambridge *) diff -r e8d4606e6502 -r 3f7d67927fe2 src/Modal/S43.thy --- a/src/Modal/S43.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/Modal/S43.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: 91/Modal/S43 +(* Title: 91/Modal/S43 ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1991 University of Cambridge This implements Rajeev Gore's sequent calculus for S43. @@ -9,10 +9,10 @@ S43 = Modal0 + consts - S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj, - sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop" + S43pi :: "[sobj=>sobj, sobj=>sobj, sobj=>sobj, + sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop" "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence, - sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5) + sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5) rules (* Definition of the star operation using a set of Horn clauses *) @@ -69,9 +69,9 @@ val tr' = LK.seq_tr1'; fun s43pi_tr[s1,s2,s3,s4,s5,s6]= - Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6; + Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6; fun s43pi_tr'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3), - Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] = + Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] = Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6; in val parse_translation = [(SS43pi,s43pi_tr)]; diff -r e8d4606e6502 -r 3f7d67927fe2 src/Modal/T.thy --- a/src/Modal/T.thy Mon Feb 05 13:44:28 1996 +0100 +++ b/src/Modal/T.thy Mon Feb 05 14:44:09 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: 91/Modal/T +(* Title: 91/Modal/T ID: $Id$ - Author: Martin Coen + Author: Martin Coen Copyright 1991 University of Cambridge *)