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

5976 44290b71a85f tuning to assimiliate it with PhD; mueller parents: 4559 diff changeset	1	(* Title: HOLCF/IOA/meta_theory/Pred.thy
12218 6597093b77e7 GPLed; wenzelm parents: 12114 diff changeset	2	Author: Olaf M�ller
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	3	*)
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	4
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	5	header {* Logical Connectives lifted to predicates *}
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	6
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	7	theory Pred
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	8	imports Main
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	9	begin
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	10
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	11	defaultsort type
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	12
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	13	types
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	14	'a predicate = "'a => bool"
4559 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)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	19	valid ::"'a predicate => bool" (* ("\|-") *)
4559 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)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	34	"NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	35	"AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	36	"OR" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<or>" 30)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 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)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	40	"satisfies" ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
4559 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)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	43	"NOT" ::"'a predicate => 'a predicate" ("\<not> _" [40] 40)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	44	"AND" ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<and>" 35)
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 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
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	50	satisfies_def:
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	51	"s \|= P == P s"
4559 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 *)
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	54	valid_def:
4559 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
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	57	NOT_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	58	"NOT P s == ~ (P s)"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	59
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	60	AND_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	61	"(P .& Q) s == (P s) & (Q s)"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	62
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	63	OR_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	64	"(P .\| Q) s == (P s) \| (Q s)"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	65
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	66	IMPLIES_def:
4559 8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	67	"(P .--> Q) s == (P s) --> (Q s)"
8e604d885b54 added files containing temproal logic and abstraction; mueller parents: diff changeset	68
7661 8c3190b173aa depend on Main; wenzelm parents: 6340 diff changeset	69	end

author	huffman
	Wed, 17 Feb 2010 10:00:22 -0800
changeset 35174	e15040ae75d7
parent 19741	f65265d71426
child 35355	613e133966ea
permissions	-rw-r--r--