isabelle: src/HOL/IOA/Solve.thy@947d3a694654 (annotated)

4530 ac1821645636 corrected Title oheimb parents: 3078 diff changeset	1	(* Title: HOL/IOA/Solve.thy
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	2	ID: $Id$
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	3	Author: Tobias Nipkow & Konrad Slind
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	4	Copyright 1994 TU Muenchen
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	5	*)
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	6
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	7	header {* Weak possibilities mapping (abstraction) *}
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	8
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	9	theory Solve
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	10	imports IOA
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	11	begin
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	12
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	13	constdefs
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	14
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	15	is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	16	"is_weak_pmap f C A ==
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	17	(!s:starts_of(C). f(s):starts_of(A)) &
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	18	(!s t a. reachable C s &
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	19	(s,a,t):trans_of(C)
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	20	--> (if a:externals(asig_of(C)) then
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	21	(f(s),a,f(t)):trans_of(A)
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	22	else f(s)=f(t)))"
984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	23
17288 aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	24	ML {* use_legacy_bindings (the_context ()) *}
aa3833fb7bee converted to Isar theory format; wenzelm parents: 4530 diff changeset	25
3078 984866a8f905 old IOA meta theory (see also new version in HOLCF/IOA/meta_theory); mueller parents: diff changeset	26	end

author	wenzelm
	Mon, 06 Feb 2006 20:59:10 +0100
changeset 18943	947d3a694654
parent 17288	aa3833fb7bee
child 19801	b2af2549efd1
permissions	-rw-r--r--