[f01853]: thys / TLA / PreFormulas.thy  Maximize  Restore  History

Download this file

229 lines (166 with data), 7.9 kB

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
(* Title: A Definitional Encoding of TLA in Isabelle/HOL
Authors: Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year: 2011
Maintainer: Gudmund Grov <ggrov at inf.ed.ac.uk>
*)
header "Reasoning about PreFormulas"
theory PreFormulas
imports Semantics
begin
text{*
Semantic separation of formulas and pre-formulas requires a deep embedding.
We introduce a syntactically distinct notion of validity, written @{text "|~ A"},
for pre-formulas. Although it is semantically identical to @{text "\<turnstile> A"}, it
helps users distinguish pre-formulas from formulas in \tlastar{} proofs.
*}
definition PreValid :: "('w::world) form \<Rightarrow> bool"
where "PreValid A \<equiv> \<forall> w. w \<Turnstile> A"
syntax
"_PreValid" :: "lift \<Rightarrow> bool" ("(|~ _)" 5)
translations
"_PreValid" \<rightleftharpoons> "CONST PreValid"
lemma prefD[dest]: "|~ A \<Longrightarrow> w \<Turnstile> A"
by (simp add: PreValid_def)
lemma prefI[intro!]: "(\<And> w. w \<Turnstile> A) \<Longrightarrow> |~ A"
by (simp add: PreValid_def)
method_setup pref_unlift = {* Scan.succeed
(K (SIMPLE_METHOD ((rtac @{thm prefI} THEN' rewrite_goal_tac @{thms intensional_rews}) 1))) *}
"int_unlift for PreFormulas"
lemma prefeq_reflection: assumes P1: "|~ x=y" shows "(x \<equiv> y)"
using P1 by (intro eq_reflection) force
lemma pref_True[simp]: "|~ #True"
by auto
lemma pref_eq: "|~ X = Y \<Longrightarrow> X = Y"
by (auto simp: prefeq_reflection)
lemma pref_iffI:
assumes "|~ F \<longrightarrow> G" and "|~ G \<longrightarrow> F"
shows "|~ F = G"
using assms by force
lemma pref_iffD1: assumes "|~ F = G" shows "|~ F \<longrightarrow> G"
using assms by auto
lemma pref_iffD2: assumes "|~ F = G" shows "|~ G \<longrightarrow> F"
using assms by auto
lemma unl_pref_imp:
assumes "|~ F \<longrightarrow> G" shows "\<And> w. w \<Turnstile> F \<Longrightarrow> w \<Turnstile> G"
using assms by auto
lemma pref_imp_trans:
assumes "|~ F \<longrightarrow> G" and "|~ G \<longrightarrow> H"
shows "|~ F \<longrightarrow> H"
using assms by force
subsection "Lemmas about @{text Unchanged}"
text {*
Many of the \tlastar{} axioms only require a state function witness
which leaves the state space unchanged. An obvious witness is the
@{term id} function. The lemmas require that the given formula is
invariant under stuttering.
*}
lemma pre_id_unch: assumes h: "stutinv F"
shows "|~ F \<and> Unchanged id \<longrightarrow> \<circ>F"
proof (pref_unlift, clarify)
fix s
assume a1: "s \<Turnstile> F" and a2: "s \<Turnstile> Unchanged id"
from a2 have "(id (second s) = id (first s))" by (simp add: unch_defs)
hence "s \<approx> (tail s)" by (simp add: addfirststut)
with h a1 have "(tail s) \<Turnstile> F" by (simp add: stutinv_def)
thus "s \<Turnstile> \<circ>F" by (unfold nexts_def)
qed
lemma pre_ex_unch:
assumes h: "stutinv F"
shows "\<exists>(v::'a::world \<Rightarrow> 'a). ( |~ F \<and> Unchanged v \<longrightarrow> \<circ>F)"
using pre_id_unch[OF h] by blast
lemma unch_pair: "|~ Unchanged (x,y) = (Unchanged x \<and> Unchanged y)"
by (auto simp: unch_def before_def after_def nexts_def)
lemmas unch_eq1 = unch_pair[THEN pref_eq]
lemmas unch_eq2 = unch_pair[THEN prefeq_reflection]
lemma angle_actrans_sem: "|~ \<langle>F\<rangle>_v = (F \<and> v$ \<noteq> $v)"
by (auto simp: angle_actrans_def actrans_def unch_def)
lemmas angle_actrans_sem_eq = angle_actrans_sem[THEN pref_eq]
subsection "Lemmas about @{text after}"
lemma after_const: "|~ (#c)` = #c"
by (auto simp: nexts_def before_def after_def)
lemma after_fun1: "|~ f<x>` = f<x`>"
by (auto simp: nexts_def before_def after_def)
lemma after_fun2: "|~ f<x,y>` = f <x`,y`>"
by (auto simp: nexts_def before_def after_def)
lemma after_fun3: "|~ f<x,y,z>` = f <x`,y`,z`>"
by (auto simp: nexts_def before_def after_def)
lemma after_fun4: "|~ f<x,y,z,zz>` = f <x`,y`,z`,zz`>"
by (auto simp: nexts_def before_def after_def)
lemma after_forall: "|~ (\<forall> x. P x)` = (\<forall> x. (P x)`)"
by (auto simp: nexts_def before_def after_def)
lemma after_exists: "|~ (\<exists> x. P x)` = (\<exists> x. (P x)`)"
by (auto simp: nexts_def before_def after_def)
lemma after_exists1: "|~ (\<exists>! x. P x)` = (\<exists>! x. (P x)`)"
by (auto simp: nexts_def before_def after_def)
lemmas all_after = after_const after_fun1 after_fun2 after_fun3 after_fun4
after_forall after_exists after_exists1
lemmas all_after_unl = all_after[THEN prefD]
lemmas all_after_eq = all_after[THEN prefeq_reflection]
subsection "Lemmas about @{text before}"
lemma before_const: "\<turnstile> $(#c) = #c"
by (auto simp: before_def)
lemma before_fun1: "\<turnstile> $(f<x>) = f <$x>"
by (auto simp: before_def)
lemma before_fun2: "\<turnstile> $(f<x,y>) = f <$x,$y>"
by (auto simp: before_def)
lemma before_fun3: "\<turnstile> $(f<x,y,z>) = f <$x,$y,$z>"
by (auto simp: before_def)
lemma before_fun4: "\<turnstile> $(f<x,y,z,zz>) = f <$x,$y,$z,$zz>"
by (auto simp: before_def)
lemma before_forall: "\<turnstile> $(\<forall> x. P x) = (\<forall> x. $(P x))"
by (auto simp: before_def)
lemma before_exists: "\<turnstile> $(\<exists> x. P x) = (\<exists> x. $(P x))"
by (auto simp: before_def)
lemma before_exists1: "\<turnstile> $(\<exists>! x. P x) = (\<exists>! x. $(P x))"
by (auto simp: before_def)
lemmas all_before = before_const before_fun1 before_fun2 before_fun3 before_fun4
before_forall before_exists before_exists1
lemmas all_before_unl = all_before[THEN intD]
lemmas all_before_eq = all_before[THEN inteq_reflection]
subsection "Some general properties"
lemma angle_actrans_conj: "|~ (\<langle>F \<and> G\<rangle>_v) = (\<langle>F\<rangle>_v \<and> \<langle>G\<rangle>_v)"
by (auto simp: angle_actrans_def actrans_def unch_def)
lemma angle_actrans_disj: "|~ (\<langle>F \<or> G\<rangle>_v) = (\<langle>F\<rangle>_v \<or> \<langle>G\<rangle>_v)"
by (auto simp: angle_actrans_def actrans_def unch_def)
lemma int_eq_true: "\<turnstile> P \<Longrightarrow> \<turnstile> P = #True"
by auto
lemma pref_eq_true: "|~ P \<Longrightarrow> |~ P = #True"
by auto
subsection "Unlifting attributes and methods"
text {* Attribute which unlifts an intensional formula or preformula *}
ML {*
fun unl_rewr thm =
let
val unl = (thm RS @{thm intD}) handle _ => (thm RS @{thm prefD})
handle _ => thm
val rewr = rewrite_rule @{thms intensional_rews}
in
unl |> rewr
end;
val att_unl_tac = Thm.rule_attribute (fn _ => unl_rewr);
val att_unl_rule_tac = Thm.rule_attribute (fn _ => Object_Logic.rulify o unl_rewr);
*}
attribute_setup unlifted = {* Scan.succeed att_unl_tac *}
"attribute to unlift intensional formulas"
attribute_setup unlift_rule = {* Scan.succeed att_unl_rule_tac *}
"attribute to unlift and rulify intensional formulas"
text {*
Attribute which turns an intensional formula or preformula into a rewrite rule.
Formulas @{text F} that are not equalities are turned into @{text "F \<equiv> #True"}.
*}
ML {*
fun int_rewr thm =
(thm RS @{thm inteq_reflection})
handle _ => (thm RS @{thm prefeq_reflection})
handle _ => ((thm RS @{thm int_eq_true}) RS @{thm inteq_reflection})
handle _ => ((thm RS @{thm pref_eq_true}) RS @{thm prefeq_reflection});
val att_int_rew_tac =
Thm.rule_attribute (fn _ => int_rewr)
val int_simp_fn = Thm.declaration_attribute (fn th => Simplifier.map_ss (fn ss => Simplifier.addsimps (ss, [int_rewr th])));
*}
attribute_setup simp_unl = {* Attrib.add_del int_simp_fn I *} (* note only adding -- removing is ignored *)
"adds thm unlifted from rewrites from intensional formulas or preformulas"
attribute_setup int_rewrite = {* Scan.succeed att_int_rew_tac *}
"attribute to produce rewrites from intensional formulas or preformulas"
end

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks