src/HOL/UNITY/Extend.thy
 author nipkow Tue Jan 09 15:32:27 2001 +0100 (2001-01-09) changeset 10834 a7897aebbffc parent 10064 1a77667b21ef child 13790 8d7e9fce8c50 permissions -rw-r--r--
*** empty log message ***
 paulson@6297 1 (* Title: HOL/UNITY/Extend.thy paulson@6297 2 ID: \$Id\$ paulson@6297 3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@6297 4 Copyright 1998 University of Cambridge paulson@6297 5 paulson@6297 6 Extending of state sets paulson@6297 7 function f (forget) maps the extended state to the original state paulson@6297 8 function g (forgotten) maps the extended state to the "extending part" paulson@6297 9 *) paulson@6297 10 paulson@7399 11 Extend = Guar + paulson@6297 12 paulson@6297 13 constdefs paulson@6297 14 paulson@8948 15 (*MOVE to Relation.thy?*) paulson@8948 16 Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set" paulson@8948 17 "Restrict A r == r Int (A <*> UNIV)" paulson@8948 18 paulson@7482 19 good_map :: "['a*'b => 'c] => bool" paulson@7482 20 "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)" paulson@7482 21 (*Using the locale constant "f", this is f (h (x,y))) = x*) paulson@7482 22 paulson@6297 23 extend_set :: "['a*'b => 'c, 'a set] => 'c set" nipkow@10834 24 "extend_set h A == h ` (A <*> UNIV)" paulson@6297 25 paulson@7342 26 project_set :: "['a*'b => 'c, 'c set] => 'a set" paulson@7342 27 "project_set h C == {x. EX y. h(x,y) : C}" paulson@7342 28 paulson@7342 29 extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set" paulson@7826 30 "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}" paulson@6297 31 paulson@7878 32 project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" paulson@7878 33 "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}" paulson@7342 34 paulson@6297 35 extend :: "['a*'b => 'c, 'a program] => 'c program" paulson@6297 36 "extend h F == mk_program (extend_set h (Init F), nipkow@10834 37 extend_act h ` Acts F, nipkow@10834 38 project_act h -` AllowedActs F)" paulson@6297 39 paulson@7878 40 (*Argument C allows weak safety laws to be projected*) paulson@7880 41 project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" paulson@10064 42 "project h C F == paulson@10064 43 mk_program (project_set h (Init F), nipkow@10834 44 project_act h ` Restrict C ` Acts F, paulson@10064 45 {act. Restrict (project_set h C) act : nipkow@10834 46 project_act h ` Restrict C ` AllowedActs F})" paulson@7342 47 paulson@6297 48 locale Extend = paulson@6297 49 fixes paulson@6297 50 f :: 'c => 'a paulson@6297 51 g :: 'c => 'b paulson@6297 52 h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *) paulson@6297 53 slice :: ['c set, 'b] => 'a set paulson@6297 54 paulson@6297 55 assumes paulson@7482 56 good_h "good_map h" paulson@6297 57 defines paulson@6297 58 f_def "f z == fst (inv h z)" paulson@6297 59 g_def "g z == snd (inv h z)" paulson@6297 60 slice_def "slice Z y == {x. h(x,y) : Z}" paulson@6297 61 paulson@6297 62 end