isabelle: src/HOLCF/IOA/meta_theory/Pred.thy@6f79698f294d (annotated)

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 6597093b77e7 GPLed; wenzelm parents: 12114 diff changeset	3	Author: Olaf M�ller
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	4	*)
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	5
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	6	header {* Logical Connectives lifted to predicates *}
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	7
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	8	theory Pred
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	9	imports Main
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	10	begin
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	11
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	12	defaultsort type
4559 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	types
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	15	'a predicate = "'a => bool"
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	16
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	17	consts
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	18
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	19	satisfies ::"'a => 'a predicate => bool" ("_ \|= _" [100,9] 8)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	20	valid ::"'a predicate => bool" (* ("\|-") *)
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	21
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	22	NOT ::"'a predicate => 'a predicate" (".~ _" [40] 40)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	23	AND ::"'a predicate => 'a predicate => 'a predicate" (infixr ".&" 35)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	24	OR ::"'a predicate => 'a predicate => 'a predicate" (infixr ".\|" 30)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	25	IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr ".-->" 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
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	28	syntax ("" output)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	29	"NOT" ::"'a predicate => 'a predicate" ("~ _" [40] 40)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	30	"AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "&" 35)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	31	"OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\|" 30)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	32	"IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "-->" 25)
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	33
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 7661 diff changeset	34	syntax (xsymbols output)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	35	"NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	36	"AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	37	"OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	38	"IMPLIES" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<longrightarrow>" 25)
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	39
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 7661 diff changeset	40	syntax (xsymbols)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	41	"satisfies" ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	42
6340 7d5cbd5819a0 HTML output; wenzelm parents: 5976 diff changeset	43	syntax (HTML output)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	44	"NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	45	"AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	46	"OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
6340 7d5cbd5819a0 HTML output; wenzelm parents: 5976 diff changeset	47
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	48
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	49	defs
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	50
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	51	satisfies_def:
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	52	"s \|= P == P s"
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	53
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	54	(* priority einfuegen, da clash mit \|=, wenn graphisches Symbol *)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	55	valid_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	56	"valid P == (! s. (s \|= P))"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	57
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	58	NOT_def:
4559 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
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	61	AND_def:
4559 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
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	64	OR_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	65	"(P .\| Q) s == (P s) \| (Q s)"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	66
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	67	IMPLIES_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	68	"(P .--> Q) s == (P s) --> (Q s)"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	69
7661 8c3190b173aa depend on Main; wenzelm parents: 6340 diff changeset	70	end

author	wenzelm
	Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456	6f79698f294d
parent 19741	f65265d71426
child 35174	e15040ae75d7
permissions	-rw-r--r--