author | nipkow |
Mon, 27 Apr 1998 16:47:50 +0200 | |
changeset 4833 | 2e53109d4bc8 |
parent 4681 | a331c1f5a23e |
child 5068 | fb28eaa07e01 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefMappings.ML |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf Mueller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Refinement Mappings in HOLCF/IOA |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
11 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
12 |
|
3071 | 13 |
(* ---------------------------------------------------------------------------- *) |
14 |
||
15 |
section "transitions and moves"; |
|
16 |
||
17 |
||
18 |
goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t"; |
|
19 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
20 |
by (res_inst_tac [("x","(a,t)>>nil")] exI 1); |
4098 | 21 |
by (asm_full_simp_tac (simpset() addsimps [move_def]) 1); |
3071 | 22 |
qed"transition_is_ex"; |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
23 |
|
3071 | 24 |
|
25 |
goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t"; |
|
26 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
27 |
by (res_inst_tac [("x","nil")] exI 1); |
4098 | 28 |
by (asm_full_simp_tac (simpset() addsimps [move_def]) 1); |
3071 | 29 |
qed"nothing_is_ex"; |
30 |
||
31 |
||
32 |
goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \ |
|
33 |
\ ==> ? ex. move A ex s a s''"; |
|
34 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
35 |
by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1); |
4098 | 36 |
by (asm_full_simp_tac (simpset() addsimps [move_def]) 1); |
3071 | 37 |
qed"ei_transitions_are_ex"; |
38 |
||
39 |
||
40 |
goal thy |
|
41 |
"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\ |
|
42 |
\ (~a2:ext A) & (~a3:ext A) ==> \ |
|
43 |
\ ? ex. move A ex s1 a1 s4"; |
|
44 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
45 |
by (res_inst_tac [("x","(a1,s2)>>(a2,s3)>>(a3,s4)>>nil")] exI 1); |
4098 | 46 |
by (asm_full_simp_tac (simpset() addsimps [move_def]) 1); |
3071 | 47 |
qed"eii_transitions_are_ex"; |
48 |
||
49 |
||
50 |
(* ---------------------------------------------------------------------------- *) |
|
51 |
||
52 |
section "weak_ref_map and ref_map"; |
|
53 |
||
54 |
||
55 |
goalw thy [is_weak_ref_map_def,is_ref_map_def] |
|
56 |
"!!f. [| ext C = ext A; \ |
|
57 |
\ is_weak_ref_map f C A |] ==> is_ref_map f C A"; |
|
58 |
by (safe_tac set_cs); |
|
59 |
by (case_tac "a:ext A" 1); |
|
60 |
by (rtac transition_is_ex 1); |
|
61 |
by (Asm_simp_tac 1); |
|
62 |
by (rtac nothing_is_ex 1); |
|
63 |
by (Asm_simp_tac 1); |
|
64 |
qed"weak_ref_map2ref_map"; |
|
65 |
||
66 |
||
67 |
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; |
|
4423 | 68 |
by (fast_tac (claset() addDs prems) 1); |
3521 | 69 |
val lemma = result(); |
70 |
||
4833 | 71 |
Delsplits [split_if]; |
3071 | 72 |
goal thy "!!f.[| is_weak_ref_map f C A |]\ |
73 |
\ ==> (is_weak_ref_map f (rename C g) (rename A g))"; |
|
4098 | 74 |
by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); |
3071 | 75 |
by (rtac conjI 1); |
76 |
(* 1: start states *) |
|
4098 | 77 |
by (asm_full_simp_tac (simpset() addsimps [rename_def,rename_set_def,starts_of_def]) 1); |
3071 | 78 |
(* 2: reachable transitions *) |
79 |
by (REPEAT (rtac allI 1)); |
|
3521 | 80 |
by (rtac lemma 1); |
4098 | 81 |
by (simp_tac (simpset() addsimps [rename_def,rename_set_def]) 1); |
82 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def, |
|
3071 | 83 |
asig_outputs_def,asig_of_def,trans_of_def]) 1); |
4423 | 84 |
by Safe_tac; |
4833 | 85 |
by (stac split_if 1); |
3071 | 86 |
by (rtac conjI 1); |
87 |
by (rtac impI 1); |
|
88 |
by (etac disjE 1); |
|
89 |
by (etac exE 1); |
|
90 |
by (etac conjE 1); |
|
91 |
(* x is input *) |
|
92 |
by (dtac sym 1); |
|
93 |
by (dtac sym 1); |
|
94 |
by (Asm_full_simp_tac 1); |
|
95 |
by (REPEAT (hyp_subst_tac 1)); |
|
96 |
by (forward_tac [reachable_rename] 1); |
|
97 |
by (Asm_full_simp_tac 1); |
|
98 |
(* x is output *) |
|
99 |
by (etac exE 1); |
|
100 |
by (etac conjE 1); |
|
101 |
by (dtac sym 1); |
|
102 |
by (dtac sym 1); |
|
103 |
by (Asm_full_simp_tac 1); |
|
104 |
by (REPEAT (hyp_subst_tac 1)); |
|
105 |
by (forward_tac [reachable_rename] 1); |
|
106 |
by (Asm_full_simp_tac 1); |
|
107 |
(* x is internal *) |
|
4098 | 108 |
by (simp_tac (simpset() addcongs [conj_cong]) 1); |
3071 | 109 |
by (rtac impI 1); |
110 |
by (etac conjE 1); |
|
111 |
by (forward_tac [reachable_rename] 1); |
|
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset
|
112 |
by Auto_tac; |
3071 | 113 |
qed"rename_through_pmap"; |
4833 | 114 |
Addsplits [split_if]; |
3071 | 115 |
|
116 |