Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IOA/meta_theory/Pred.thy
author huffman
Fri, 27 May 2005 00:16:18 +0200
changeset 16093 cdcbf5a7f38d
parent 14981 e73f8140af78
child 17233 41eee2e7b465
permissions -rw-r--r--
use thelub_const lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5976
44290b71a85f tuning to assimiliate it with PhD;
mueller
parents: 4559
diff changeset 
     1
 
(*  Title:      HOLCF/IOA/meta_theory/Pred.thy
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset 
     2
 
    ID:         $Id$
12218
wenzelm
parents: 12114
diff changeset 
     3
 
    Author:     Olaf Müller
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset 
     4
 












8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




     5


Logical Connectives lifted to predicates.













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




     6


*)   













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




     7


	       








7661






8c3190b173aa
depend on Main;



wenzelm


parents: 
6340

diff
changeset




     8


Pred = Main +








4559






8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




     9









12338






de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");



wenzelm


parents: 
12218

diff
changeset




    10


default type








4559






8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    11














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    12


types













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    13














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    14


'a predicate      = "'a => bool"













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    15














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    16


consts













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    17














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    18


satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    19


valid        ::"'a predicate => bool"           (*  ("|-") *)         













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    20














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    21


NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    22


AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    23


OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    24


IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    25














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    26














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    27


syntax ("" output)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    28


  "NOT"     ::"'a predicate => 'a predicate" ("~ _" [40] 40)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    29


  "AND"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "&" 35)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    30


  "OR"      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "|" 30)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    31


  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "-->" 25)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    32









12114






a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;



wenzelm


parents: 
7661

diff
changeset




    33


syntax (xsymbols output)








4559






8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    34


  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    35


  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    36


  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)








12114






a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;



wenzelm


parents: 
7661

diff
changeset




    37


  "IMPLIES" ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<longrightarrow>" 25)








4559






8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    38









12114






a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;



wenzelm


parents: 
7661

diff
changeset




    39


syntax (xsymbols)








4559






8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    40


  "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    41









6340






7d5cbd5819a0
HTML output;



wenzelm


parents: 
5976

diff
changeset




    42


syntax (HTML output)













7d5cbd5819a0
HTML output;



wenzelm


parents: 
5976

diff
changeset




    43


  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)








14565






c6dc17aab88a
use more symbols in HTML output



kleing


parents: 
12338

diff
changeset




    44


  "AND"    ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<and>" 35)













c6dc17aab88a
use more symbols in HTML output



kleing


parents: 
12338

diff
changeset




    45


  "OR"     ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\\<or>" 30)








6340






7d5cbd5819a0
HTML output;



wenzelm


parents: 
5976

diff
changeset




    46









4559






8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    47














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    48


defs













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    49














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    50


satisfies_def













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    51


   "s |= P  == P s" 













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    52














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    53


(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    54


valid_def













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    55


   "valid P == (! s. (s |= P))"













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    56














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    57














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    58


NOT_def













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    59


  "NOT P s ==  ~ (P s)"













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    60














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    61


AND_def













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    62


  "(P .& Q) s == (P s) & (Q s)"













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    63














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    64














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    65


OR_def













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    66


  "(P .| Q) s ==  (P s) | (Q s)"













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    67














8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    68


IMPLIES_def













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    69


  "(P .--> Q) s == (P s) --> (Q s)"













8e604d885b54
added files containing temproal logic and abstraction;



mueller


parents: 

diff
changeset




    70









7661






8c3190b173aa
depend on Main;



wenzelm


parents: 
6340

diff
changeset




    71


end















isabelle