author | wenzelm |
Fri, 04 Jun 1999 19:57:31 +0200 | |
changeset 6779 | 2912aff958bd |
parent 5184 | 9b8547a9496a |
child 6916 | 4957978b6f9e |
permissions | -rw-r--r-- |
4530 | 1 |
(* Title: HOL/IOA/Solve.ML |
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 |
Weak possibilities mapping (abstraction) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
7 |
*) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
8 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
9 |
open Solve; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
10 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
Addsimps [mk_trace_thm,trans_in_actions]; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
12 |
|
5069 | 13 |
Goalw [is_weak_pmap_def,traces_def] |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
14 |
"!!f. [| IOA(C); IOA(A); externals(asig_of(C)) = externals(asig_of(A)); \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
15 |
\ is_weak_pmap f C A |] ==> traces(C) <= traces(A)"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
16 |
|
4089 | 17 |
by (simp_tac(simpset() addsimps [has_trace_def])1); |
5132 | 18 |
by Safe_tac; |
4828 | 19 |
by (rename_tac "ex1 ex2" 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
20 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
21 |
(* choose same trace, therefore same NF *) |
4772
8c7e7eaffbdf
split_all_tac now fails if there is nothing to split
oheimb
parents:
4681
diff
changeset
|
22 |
by (res_inst_tac[("x","mk_trace C ex1")] exI 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
23 |
by (Asm_full_simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
24 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
25 |
(* give execution of abstract automata *) |
4772
8c7e7eaffbdf
split_all_tac now fails if there is nothing to split
oheimb
parents:
4681
diff
changeset
|
26 |
by (res_inst_tac[("x","(mk_trace A ex1,%i. f (ex2 i))")] bexI 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
27 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
28 |
(* Traces coincide *) |
4772
8c7e7eaffbdf
split_all_tac now fails if there is nothing to split
oheimb
parents:
4681
diff
changeset
|
29 |
by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
30 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
31 |
(* Use lemma *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
32 |
by (forward_tac [states_of_exec_reachable] 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
33 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
34 |
(* Now show that it's an execution *) |
4089 | 35 |
by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1); |
4153 | 36 |
by Safe_tac; |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
37 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
38 |
(* Start states map to start states *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
39 |
by (dtac bspec 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
40 |
by (atac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
41 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
42 |
(* Show that it's an execution fragment *) |
4089 | 43 |
by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1); |
4153 | 44 |
by Safe_tac; |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
45 |
|
4772
8c7e7eaffbdf
split_all_tac now fails if there is nothing to split
oheimb
parents:
4681
diff
changeset
|
46 |
by (eres_inst_tac [("x","ex2 n")] allE 1); |
8c7e7eaffbdf
split_all_tac now fails if there is nothing to split
oheimb
parents:
4681
diff
changeset
|
47 |
by (eres_inst_tac [("x","ex2 (Suc n)")] allE 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
48 |
by (eres_inst_tac [("x","a")] allE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
49 |
by (Asm_full_simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
50 |
qed "trace_inclusion"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
51 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
52 |
(* Lemmata *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
53 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
54 |
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; |
4153 | 55 |
by (fast_tac (claset() addDs prems) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
56 |
val imp_conj_lemma = result(); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
57 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
58 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
59 |
(* fist_order_tautology of externals_of_par *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
60 |
goal IOA.thy "a:externals(asig_of(A1||A2)) = \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
61 |
\ (a:externals(asig_of(A1)) & a:externals(asig_of(A2)) | \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
62 |
\ a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) | \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
63 |
\ a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))"; |
4089 | 64 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
65 |
by (Fast_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
66 |
val externals_of_par_extra = result(); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
67 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
68 |
Goal "[| reachable (C1||C2) s |] ==> reachable C1 (fst s)"; |
4089 | 69 |
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
70 |
by (etac bexE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
71 |
by (res_inst_tac [("x", |
3842 | 72 |
"(filter_oseq (%a. a:actions(asig_of(C1))) \ |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
73 |
\ (fst ex), \ |
3842 | 74 |
\ %i. fst (snd ex i))")] bexI 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
75 |
(* fst(s) is in projected execution *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
76 |
by (Simp_tac 1); |
4838 | 77 |
by (fast_tac (claset() delSWrapper"split_all_tac")1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
78 |
(* projected execution is indeed an execution *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
79 |
by (asm_full_simp_tac |
4089 | 80 |
(simpset() addsimps [executions_def,is_execution_fragment_def, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
81 |
par_def,starts_of_def,trans_of_def,filter_oseq_def] |
5184 | 82 |
addsplits [option.split]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
83 |
qed"comp1_reachable"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
84 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
85 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
86 |
(* Exact copy of proof of comp1_reachable for the second |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
87 |
component of a parallel composition. *) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
88 |
Goal "[| reachable (C1||C2) s|] ==> reachable C2 (snd s)"; |
4089 | 89 |
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
90 |
by (etac bexE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
91 |
by (res_inst_tac [("x", |
3842 | 92 |
"(filter_oseq (%a. a:actions(asig_of(C2)))\ |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
93 |
\ (fst ex), \ |
3842 | 94 |
\ %i. snd (snd ex i))")] bexI 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
95 |
(* fst(s) is in projected execution *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
96 |
by (Simp_tac 1); |
4838 | 97 |
by (fast_tac (claset() delSWrapper"split_all_tac")1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
98 |
(* projected execution is indeed an execution *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
99 |
by (asm_full_simp_tac |
4089 | 100 |
(simpset() addsimps [executions_def,is_execution_fragment_def, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
101 |
par_def,starts_of_def,trans_of_def,filter_oseq_def] |
5184 | 102 |
addsplits [option.split]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
103 |
qed"comp2_reachable"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
104 |
|
4831 | 105 |
Delsplits [split_if]; |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
106 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
107 |
(* Composition of possibility-mappings *) |
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
108 |
Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \ |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
109 |
\ externals(asig_of(A1))=externals(asig_of(C1)) &\ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
110 |
\ is_weak_pmap g C2 A2 & \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
111 |
\ externals(asig_of(A2))=externals(asig_of(C2)) & \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
112 |
\ compat_ioas C1 C2 & compat_ioas A1 A2 |] \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
113 |
\ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
114 |
by (rtac conjI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
115 |
(* start_states *) |
4089 | 116 |
by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
117 |
(* transitions *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
118 |
by (REPEAT (rtac allI 1)); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
119 |
by (rtac imp_conj_lemma 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
120 |
by (REPEAT(etac conjE 1)); |
4089 | 121 |
by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1); |
122 |
by (simp_tac (simpset() addsimps [par_def]) 1); |
|
123 |
by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1); |
|
4831 | 124 |
by (stac split_if 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
125 |
by (rtac conjI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
126 |
by (rtac impI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
127 |
by (etac disjE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
128 |
(* case 1 a:e(A1) | a:e(A2) *) |
4089 | 129 |
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
130 |
ext_is_act]) 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
131 |
by (etac disjE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
132 |
(* case 2 a:e(A1) | a~:e(A2) *) |
4089 | 133 |
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
134 |
ext_is_act,ext1_ext2_is_not_act2]) 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
135 |
(* case 3 a:~e(A1) | a:e(A2) *) |
4089 | 136 |
by (asm_full_simp_tac (simpset() addsimps [comp1_reachable,comp2_reachable, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
137 |
ext_is_act,ext1_ext2_is_not_act1]) 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
138 |
(* case 4 a:~e(A1) | a~:e(A2) *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
139 |
by (rtac impI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
140 |
by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
141 |
(* delete auxiliary subgoal *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
142 |
by (Asm_full_simp_tac 2); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
143 |
by (Fast_tac 2); |
4089 | 144 |
by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong] |
4831 | 145 |
addsplits [split_if]) 1); |
4153 | 146 |
by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN |
4089 | 147 |
asm_full_simp_tac(simpset() addsimps[comp1_reachable, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
148 |
comp2_reachable])1)); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
149 |
qed"fxg_is_weak_pmap_of_product_IOA"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
150 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
151 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
152 |
Goal "[| reachable (rename C g) s |] ==> reachable C s"; |
4089 | 153 |
by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
154 |
by (etac bexE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
155 |
by (res_inst_tac [("x", |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
156 |
"((%i. case (fst ex i) \ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
157 |
\ of None => None\ |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
158 |
\ | Some(x) => g x) ,snd ex)")] bexI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
159 |
by (Simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
160 |
(* execution is indeed an execution of C *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
161 |
by (asm_full_simp_tac |
4089 | 162 |
(simpset() addsimps [executions_def,is_execution_fragment_def, |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
163 |
par_def,starts_of_def,trans_of_def,rename_def] |
5184 | 164 |
addsplits [option.split]) 1); |
4089 | 165 |
by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
166 |
qed"reachable_rename_ioa"; |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
167 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
168 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5132
diff
changeset
|
169 |
Goal "[| is_weak_pmap f C A |]\ |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
170 |
\ ==> (is_weak_pmap f (rename C g) (rename A g))"; |
4089 | 171 |
by (asm_full_simp_tac (simpset() addsimps [is_weak_pmap_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
172 |
by (rtac conjI 1); |
4089 | 173 |
by (asm_full_simp_tac (simpset() addsimps [rename_def,starts_of_def]) 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
174 |
by (REPEAT (rtac allI 1)); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
175 |
by (rtac imp_conj_lemma 1); |
4089 | 176 |
by (simp_tac (simpset() addsimps [rename_def]) 1); |
177 |
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1); |
|
4153 | 178 |
by Safe_tac; |
4831 | 179 |
by (stac split_if 1); |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
180 |
by (rtac conjI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
181 |
by (rtac impI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
182 |
by (etac disjE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
183 |
by (etac exE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
184 |
by (etac conjE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
185 |
(* x is input *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
186 |
by (dtac sym 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
187 |
by (dtac sym 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
188 |
by (Asm_full_simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
189 |
by (REPEAT (hyp_subst_tac 1)); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
190 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
191 |
by (assume_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
192 |
by (Asm_full_simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
193 |
(* x is output *) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
194 |
by (etac exE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
195 |
by (etac conjE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
196 |
by (dtac sym 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
197 |
by (dtac sym 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
198 |
by (Asm_full_simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
199 |
by (REPEAT (hyp_subst_tac 1)); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
200 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
201 |
by (assume_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
202 |
by (Asm_full_simp_tac 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
203 |
(* x is internal *) |
4089 | 204 |
by (simp_tac (simpset() addsimps [de_Morgan_disj, de_Morgan_conj, not_ex] |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
205 |
addcongs [conj_cong]) 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
206 |
by (rtac impI 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
207 |
by (etac conjE 1); |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
208 |
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1); |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4153
diff
changeset
|
209 |
by Auto_tac; |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
210 |
qed"rename_through_pmap"; |
4681 | 211 |
|
4831 | 212 |
Addsplits [split_if]; |