1 (* Title: HOL/UNITY/Extend.thy |
1 (* Title: HOL/UNITY/Extend.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
5 |
4 |
6 Extending of state setsExtending of state sets |
5 Extending of state setsExtending of state sets |
7 function f (forget) maps the extended state to the original state |
6 function f (forget) maps the extended state to the original state |
34 project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" |
33 project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" |
35 "project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}" |
34 "project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}" |
36 |
35 |
37 extend :: "['a*'b => 'c, 'a program] => 'c program" |
36 extend :: "['a*'b => 'c, 'a program] => 'c program" |
38 "extend h F == mk_program (extend_set h (Init F), |
37 "extend h F == mk_program (extend_set h (Init F), |
39 extend_act h ` Acts F, |
38 extend_act h ` Acts F, |
40 project_act h -` AllowedActs F)" |
39 project_act h -` AllowedActs F)" |
41 |
40 |
42 (*Argument C allows weak safety laws to be projected*) |
41 (*Argument C allows weak safety laws to be projected*) |
43 project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" |
42 project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" |
44 "project h C F == |
43 "project h C F == |
45 mk_program (project_set h (Init F), |
44 mk_program (project_set h (Init F), |
46 project_act h ` Restrict C ` Acts F, |
45 project_act h ` Restrict C ` Acts F, |
47 {act. Restrict (project_set h C) act : |
46 {act. Restrict (project_set h C) act : |
48 project_act h ` Restrict C ` AllowedActs F})" |
47 project_act h ` Restrict C ` AllowedActs F})" |
49 |
48 |
50 locale Extend = |
49 locale Extend = |
51 fixes f :: "'c => 'a" |
50 fixes f :: "'c => 'a" |
52 and g :: "'c => 'b" |
51 and g :: "'c => 'b" |
53 and h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *) |
52 and h :: "'a*'b => 'c" (*isomorphism between 'a * 'b and 'c *) |
102 by blast |
101 by blast |
103 |
102 |
104 (*Possibly easier than reasoning about "inv h"*) |
103 (*Possibly easier than reasoning about "inv h"*) |
105 lemma good_mapI: |
104 lemma good_mapI: |
106 assumes surj_h: "surj h" |
105 assumes surj_h: "surj h" |
107 and prem: "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'" |
106 and prem: "!! x x' y y'. h(x,y) = h(x',y') ==> x=x'" |
108 shows "good_map h" |
107 shows "good_map h" |
109 apply (simp add: good_map_def) |
108 apply (simp add: good_map_def) |
110 apply (safe intro!: surj_h) |
109 apply (safe intro!: surj_h) |
111 apply (rule prem) |
110 apply (rule prem) |
112 apply (subst surjective_pairing [symmetric]) |
111 apply (subst surjective_pairing [symmetric]) |
118 by (unfold good_map_def, auto) |
117 by (unfold good_map_def, auto) |
119 |
118 |
120 (*A convenient way of finding a closed form for inv h*) |
119 (*A convenient way of finding a closed form for inv h*) |
121 lemma fst_inv_equalityI: |
120 lemma fst_inv_equalityI: |
122 assumes surj_h: "surj h" |
121 assumes surj_h: "surj h" |
123 and prem: "!! x y. g (h(x,y)) = x" |
122 and prem: "!! x y. g (h(x,y)) = x" |
124 shows "fst (inv h z) = g z" |
123 shows "fst (inv h z) = g z" |
125 apply (unfold inv_def) |
124 apply (unfold inv_def) |
126 apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE]) |
125 apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE]) |
127 apply (rule someI2) |
126 apply (rule someI2) |
128 apply (drule_tac [2] f = g in arg_cong) |
127 apply (drule_tac [2] f = g in arg_cong) |