1open HolKernel Parse boolLib bossLib;
2
3(*
4quietdec := true;
5
6val home_dir = (Globals.HOLDIR ^ "/examples/temporal_deep/");
7loadPath := (home_dir ^ "src/deep_embeddings") ::
8            (home_dir ^ "src/tools") :: !loadPath;
9
10map load
11 ["xprop_logicTheory", "prop_logicTheory", "infinite_pathTheory", "pred_setTheory", "listTheory", "pairTheory", "set_lemmataTheory",
12   "containerTheory", "prim_recTheory", "tuerk_tacticsLib", "temporal_deep_mixedTheory"];
13*)
14
15open infinite_pathTheory pred_setTheory listTheory pairTheory xprop_logicTheory
16     containerTheory prop_logicTheory set_lemmataTheory prim_recTheory
17     tuerk_tacticsLib temporal_deep_mixedTheory;
18open Sanity;
19
20val _ = hide "S";
21val _ = hide "I";
22
23(*
24show_assums := false;
25show_assums := true;
26show_types := true;
27show_types := false;
28quietdec := false;
29*)
30
31
32val _ = new_theory "semi_automaton";
33val _ = ParseExtras.temp_loose_equality()
34
35
36
37(*****************************************************************************)
38(* representation of non deterministic semi automata, that use               *)
39(* the powerset of a set of propositional varibales as inputs                *)
40(*****************************************************************************)
41val semi_automaton_def =
42 Hol_datatype
43  `semi_automaton =
44    <| S:  'state set;                         (*set of states *)
45       I:  'input set;                         (*set of inputs *)
46       S0: ('state # 'input set) set;          (*initial states*)
47       R:  ('state # 'input set # 'state # 'input set) set  (*transition relation*) |>`;
48
49
50
51val semi_automaton_S = DB.fetch "-" "semi_automaton_S";
52val semi_automaton_I = DB.fetch "-" "semi_automaton_I";
53val semi_automaton_S0 = DB.fetch "-" "semi_automaton_S0";
54val semi_automaton_R = DB.fetch "-" "semi_automaton_R";
55val semi_automaton_11 = DB.fetch "-" "semi_automaton_11";
56
57val semi_automaton_REWRITES = save_thm("semi_automaton_REWRITES", LIST_CONJ [semi_automaton_S, semi_automaton_I, semi_automaton_S0, semi_automaton_R, semi_automaton_11]);
58
59
60val IS_WELL_FORMED_SEMI_AUTOMATON_def =
61 Define
62  `IS_WELL_FORMED_SEMI_AUTOMATON A =
63    (FINITE A.S /\ FINITE A.I /\ A.S0 SUBSET (A.S CROSS (POW A.I)) /\
64     A.R SUBSET (A.S CROSS ((POW A.I) CROSS (A.S CROSS (POW A.I)))))`
65
66(*****************************************************************************)
67(* RUN A i w is true iff p is a run of i through A                             *)
68(*****************************************************************************)
69val IS_RUN_THROUGH_SEMI_AUTOMATON_def =
70 Define
71  `IS_RUN_THROUGH_SEMI_AUTOMATON A i w =
72    ((!n. w n IN A.S) /\
73     ((w 0, (i 0) INTER A.I) IN A.S0) /\
74    (!n. (w n, (i n) INTER A.I, w (SUC n), (i (SUC n)) INTER A.I) IN A.R))`;
75
76
77val IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE_def =
78 Define
79  `IS_RUN_THROUGH_SEMI_AUTOMATON_TO_STATE A i w s m =
80    ((!n. n <= m ==> (w n IN A.S)) /\
81     ((w 0, (i 0) INTER A.I) IN A.S0) /\ (w m = s) /\
82    (!n. n < m ==> ((w n, (i n) INTER A.I, w (SUC n), (i (SUC n)) INTER A.I) IN A.R)))`;
83
84
85val IS_DET_TOTAL_SEMI_AUTOMATON_def =
86 Define
87  `IS_DET_TOTAL_SEMI_AUTOMATON A =
88    ((!i. ?!x. (x, i INTER A.I) IN A.S0) /\
89     !s i i'. (s IN A.S /\ i SUBSET A.I /\ i' SUBSET A.I) ==>
90           (?!s'. (s, i, s', i') IN A.R))`;
91
92
93val IS_DET_TOTAL_SEMI_AUTOMATON___UNIQUE_RUN_EXISTS =
94  store_thm (
95    "IS_DET_TOTAL_SEMI_AUTOMATON___UNIQUE_RUN_EXISTS",
96
97    ``!A. (IS_DET_TOTAL_SEMI_AUTOMATON A /\
98    IS_WELL_FORMED_SEMI_AUTOMATON A) ==>
99    (!i. ?!w. IS_RUN_THROUGH_SEMI_AUTOMATON A i w)``,
100
101
102    SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_def,
103                    EXISTS_UNIQUE_DEF,
104                    IS_DET_TOTAL_SEMI_AUTOMATON_def,
105                    IS_WELL_FORMED_SEMI_AUTOMATON_def,
106                    SUBSET_DEF, IN_CROSS, IN_POW,
107    prove (``!P. (!x. P x) = (!x1 x2 x3 x4. P (x1,x2,x3, x4))``,
108            METIS_TAC[FST, SND, PAIR])
109    ] THEN
110    REPEAT GEN_TAC THEN STRIP_TAC THEN
111    GEN_TAC THEN
112    Q_SPEC_NO_ASSUM 5 `i 0` THEN
113    SIMP_ALL_TAC std_ss [] THEN
114    REPEAT STRIP_TAC THENL [
115      `?w. w = CHOOSEN_PATH {x} (\s n. ({s' | (s, i (PRE n) INTER A.I, s', (i n) INTER A.I) IN A.R}))` by METIS_TAC[] THEN
116      `!n. w n IN A.S` by (
117        Induct_on `n` THENL [
118          ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def, IN_SING] THEN
119          PROVE_TAC[FST],
120
121          ASM_SIMP_TAC std_ss [CHOOSEN_PATH_def] THEN
122          GSYM_NO_TAC 1 THEN
123          ASM_REWRITE_TAC[] THEN
124          SIMP_TAC std_ss [GSPECIFICATION] THEN
125          SELECT_ELIM_TAC THEN
126          REPEAT STRIP_TAC THENL [
127            Q_SPECL_NO_ASSUM 8 [`w n`, `i n INTER A.I`, `(i (SUC n)) INTER A.I`] THEN
128            UNDISCH_HD_TAC THEN
129            ASM_SIMP_TAC std_ss [IN_INTER],
130
131            METIS_TAC[]
132          ]
133        ]
134      ) THEN
135
136      Q_TAC EXISTS_TAC `w` THEN
137      REPEAT STRIP_TAC THENL [
138        PROVE_TAC[],
139
140        `w 0 = x` suffices_by METIS_TAC[] THEN
141        ASM_REWRITE_TAC [CHOOSEN_PATH_def, IN_SING] THEN
142        SIMP_TAC std_ss [],
143
144        ASM_REWRITE_TAC [CHOOSEN_PATH_def] THEN
145        GSYM_NO_TAC 1 THEN
146        ASM_REWRITE_TAC [CHOOSEN_PATH_def] THEN
147        SELECT_ELIM_TAC THEN
148        SIMP_TAC std_ss [GSPECIFICATION] THEN
149        Q_SPECL_NO_ASSUM 8 [`w n`, `i n INTER A.I`, `(i (SUC n)) INTER A.I`] THEN
150        UNDISCH_HD_TAC THEN
151        ASM_SIMP_TAC std_ss [IN_INTER]
152      ],
153
154
155
156      ONCE_REWRITE_TAC [FUN_EQ_THM] THEN
157      GEN_TAC THEN
158      Induct_on `x''` THENL [
159        PROVE_TAC[],
160
161        Q_SPECL_NO_ASSUM 13 [`y x''`, `i x'' INTER A.I`, `i (SUC x'') INTER A.I`] THEN
162        UNDISCH_HD_TAC THEN
163        ASM_SIMP_TAC std_ss [IN_INTER] THEN
164        REPEAT STRIP_TAC THEN
165        PROVE_TAC[]
166      ]
167    ]);
168
169
170
171
172
173
174val SEMI_AUTOMATON_STATE_VAR_RENAMING_def =
175 Define
176  `SEMI_AUTOMATON_STATE_VAR_RENAMING A f g =
177    (semi_automaton (IMAGE f A.S) A.I (\(s,i). (g s, i) IN A.S0)
178                     (\(s1, i, s2, i'). (g s1, i, g s2, i') IN A.R))`;
179
180val SEMI_AUTOMATON_STATE_VAR_RENAMING___RUN =
181  store_thm (
182    "SEMI_AUTOMATON_STATE_VAR_RENAMING___RUN",
183    ``(!A f g i w.
184          IS_WELL_FORMED_SEMI_AUTOMATON A /\ INJ f A.S UNIV /\
185          (!s. s IN A.S ==> (g (f s) = s)) /\ (!n. w n IN A.S) ==>
186          (IS_RUN_THROUGH_SEMI_AUTOMATON
187             (SEMI_AUTOMATON_STATE_VAR_RENAMING A f g) i
188             (PATH_MAP (\n. f) w) =
189           IS_RUN_THROUGH_SEMI_AUTOMATON A i w)) /\
190       (!A:('a, 'b) semi_automaton (f:'b -> 'c) g i w.
191         IS_WELL_FORMED_SEMI_AUTOMATON A /\ INJ f A.S UNIV /\
192         (!s. s IN A.S ==> (g (f s) = s)) /\
193         (!n. w n IN IMAGE f A.S) ==>
194         (IS_RUN_THROUGH_SEMI_AUTOMATON
195            (SEMI_AUTOMATON_STATE_VAR_RENAMING A f g) i w =
196          IS_RUN_THROUGH_SEMI_AUTOMATON A i (PATH_MAP (\n. g) w)))``,
197
198
199SIMP_TAC std_ss [IS_RUN_THROUGH_SEMI_AUTOMATON_def,
200                 SEMI_AUTOMATON_STATE_VAR_RENAMING_def,
201                 semi_automaton_REWRITES, IN_IMAGE,
202                 PATH_MAP_def,
203                 IS_WELL_FORMED_SEMI_AUTOMATON_def,
204                 INJ_DEF, SUBSET_DEF, IN_CROSS,
205  prove(``!P x1 x2 x3 x4. (x1, x2, x3, x4) IN (\(x1,x2,x3,x4). P x1 x2 x3 x4) = (P x1 x2 x3 x4)``,
206          SIMP_TAC std_ss [IN_DEF]),
207  prove(``!P x1 x2. (x1, x2) IN (\(x1,x2). P x1 x2) = (P x1 x2)``,
208          SIMP_TAC std_ss [IN_DEF])] THEN
209REPEAT STRIP_TAC THEN
210REPEAT BOOL_EQ_STRIP_TAC THEN
211METIS_TAC[FST, SND]);
212
213
214
215
216
217val _ = export_theory();
218