author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42814  5af15f1e2ef6 
child 54742  7a86358a3c0b 
permissions  rwrr 
35108  1 
(* Title: HOL/TLA/Intensional.thy 
2 
Author: Stephan Merz 

3 
Copyright: 1998 University of Munich 

21624  4 
*) 
3807  5 

21624  6 
header {* A framework for "intensional" (possibleworld based) logics 
7 
on top of HOL, with lifting of constants and functions *} 

3807  8 

17309  9 
theory Intensional 
10 
imports Main 

11 
begin 

3807  12 

35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset

13 
classes world 
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset

14 
classrel world < type 
6255  15 

16 
(** abstract syntax **) 

3807  17 

42018  18 
type_synonym ('w,'a) expr = "'w => 'a" (* intention: 'w::world, 'a::type *) 
19 
type_synonym 'w form = "('w, bool) expr" 

3807  20 

21 
consts 

17309  22 
Valid :: "('w::world) form => bool" 
23 
const :: "'a => ('w::world, 'a) expr" 

24 
lift :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr" 

25 
lift2 :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr" 

26 
lift3 :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr" 

3807  27 

6255  28 
(* "Rigid" quantification (logic level) *) 
29 
RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10) 

30 
REx :: "('a => ('w::world) form) => 'w form" (binder "Rex " 10) 

31 
REx1 :: "('a => ('w::world) form) => 'w form" (binder "Rex! " 10) 

3807  32 

6255  33 
(** concrete syntax **) 
3807  34 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
38786
diff
changeset

35 
nonterminal lift and liftargs 
3807  36 

37 
syntax 

17309  38 
"" :: "id => lift" ("_") 
39 
"" :: "longid => lift" ("_") 

40 
"" :: "var => lift" ("_") 

41 
"_applC" :: "[lift, cargs] => lift" ("(1_/ _)" [1000, 1000] 999) 

42 
"" :: "lift => lift" ("'(_')") 

43 
"_lambda" :: "[idts, 'a] => lift" ("(3%_./ _)" [0, 3] 3) 

44 
"_constrain" :: "[lift, type] => lift" ("(_::_)" [4, 0] 3) 

45 
"" :: "lift => liftargs" ("_") 

46 
"_liftargs" :: "[lift, liftargs] => liftargs" ("_,/ _") 

47 
"_Valid" :: "lift => bool" ("( _)" 5) 

48 
"_holdsAt" :: "['a, lift] => bool" ("(_ = _)" [100,10] 10) 

6255  49 

50 
(* Syntax for lifted expressions outside the scope of  or = *) 

35354  51 
"_LIFT" :: "lift => 'a" ("LIFT _") 
6255  52 

53 
(* generic syntax for lifted constants and functions *) 

17309  54 
"_const" :: "'a => lift" ("(#_)" [1000] 999) 
55 
"_lift" :: "['a, lift] => lift" ("(_<_>)" [1000] 999) 

56 
"_lift2" :: "['a, lift, lift] => lift" ("(_<_,/ _>)" [1000] 999) 

57 
"_lift3" :: "['a, lift, lift, lift] => lift" ("(_<_,/ _,/ _>)" [1000] 999) 

6255  58 

59 
(* concrete syntax for common infix functions: reuse same symbol *) 

17309  60 
"_liftEqu" :: "[lift, lift] => lift" ("(_ =/ _)" [50,51] 50) 
61 
"_liftNeq" :: "[lift, lift] => lift" ("(_ ~=/ _)" [50,51] 50) 

62 
"_liftNot" :: "lift => lift" ("(~ _)" [40] 40) 

63 
"_liftAnd" :: "[lift, lift] => lift" ("(_ &/ _)" [36,35] 35) 

64 
"_liftOr" :: "[lift, lift] => lift" ("(_ / _)" [31,30] 30) 

65 
"_liftImp" :: "[lift, lift] => lift" ("(_ >/ _)" [26,25] 25) 

66 
"_liftIf" :: "[lift, lift, lift] => lift" ("(if (_)/ then (_)/ else (_))" 10) 

67 
"_liftPlus" :: "[lift, lift] => lift" ("(_ +/ _)" [66,65] 65) 

68 
"_liftMinus" :: "[lift, lift] => lift" ("(_ / _)" [66,65] 65) 

69 
"_liftTimes" :: "[lift, lift] => lift" ("(_ */ _)" [71,70] 70) 

70 
"_liftDiv" :: "[lift, lift] => lift" ("(_ div _)" [71,70] 70) 

71 
"_liftMod" :: "[lift, lift] => lift" ("(_ mod _)" [71,70] 70) 

72 
"_liftLess" :: "[lift, lift] => lift" ("(_/ < _)" [50, 51] 50) 

73 
"_liftLeq" :: "[lift, lift] => lift" ("(_/ <= _)" [50, 51] 50) 

74 
"_liftMem" :: "[lift, lift] => lift" ("(_/ : _)" [50, 51] 50) 

75 
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ ~: _)" [50, 51] 50) 

76 
"_liftFinset" :: "liftargs => lift" ("{(_)}") 

6255  77 
(** TODO: syntax for lifted collection / comprehension **) 
17309  78 
"_liftPair" :: "[lift,liftargs] => lift" ("(1'(_,/ _'))") 
6255  79 
(* infix syntax for list operations *) 
17309  80 
"_liftCons" :: "[lift, lift] => lift" ("(_ #/ _)" [65,66] 65) 
81 
"_liftApp" :: "[lift, lift] => lift" ("(_ @/ _)" [65,66] 65) 

82 
"_liftList" :: "liftargs => lift" ("[(_)]") 

6255  83 

84 
(* Rigid quantification (syntax level) *) 

17309  85 
"_ARAll" :: "[idts, lift] => lift" ("(3! _./ _)" [0, 10] 10) 
86 
"_AREx" :: "[idts, lift] => lift" ("(3? _./ _)" [0, 10] 10) 

87 
"_AREx1" :: "[idts, lift] => lift" ("(3?! _./ _)" [0, 10] 10) 

88 
"_RAll" :: "[idts, lift] => lift" ("(3ALL _./ _)" [0, 10] 10) 

89 
"_REx" :: "[idts, lift] => lift" ("(3EX _./ _)" [0, 10] 10) 

90 
"_REx1" :: "[idts, lift] => lift" ("(3EX! _./ _)" [0, 10] 10) 

3807  91 

92 
translations 

35108  93 
"_const" == "CONST const" 
94 
"_lift" == "CONST lift" 

95 
"_lift2" == "CONST lift2" 

96 
"_lift3" == "CONST lift3" 

97 
"_Valid" == "CONST Valid" 

6255  98 
"_RAll x A" == "Rall x. A" 
99 
"_REx x A" == "Rex x. A" 

100 
"_REx1 x A" == "Rex! x. A" 

101 
"_ARAll" => "_RAll" 

102 
"_AREx" => "_REx" 

103 
"_AREx1" => "_REx1" 

3807  104 

6255  105 
"w = A" => "A w" 
106 
"LIFT A" => "A::_=>_" 

3807  107 

6255  108 
"_liftEqu" == "_lift2 (op =)" 
109 
"_liftNeq u v" == "_liftNot (_liftEqu u v)" 

35108  110 
"_liftNot" == "_lift (CONST Not)" 
6255  111 
"_liftAnd" == "_lift2 (op &)" 
112 
"_liftOr" == "_lift2 (op  )" 

113 
"_liftImp" == "_lift2 (op >)" 

35108  114 
"_liftIf" == "_lift3 (CONST If)" 
6255  115 
"_liftPlus" == "_lift2 (op +)" 
116 
"_liftMinus" == "_lift2 (op )" 

117 
"_liftTimes" == "_lift2 (op *)" 

118 
"_liftDiv" == "_lift2 (op div)" 

119 
"_liftMod" == "_lift2 (op mod)" 

120 
"_liftLess" == "_lift2 (op <)" 

121 
"_liftLeq" == "_lift2 (op <=)" 

122 
"_liftMem" == "_lift2 (op :)" 

123 
"_liftNotMem x xs" == "_liftNot (_liftMem x xs)" 

35108  124 
"_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)" 
125 
"_liftFinset x" == "_lift2 (CONST insert) x (_const {})" 

6255  126 
"_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)" 
35108  127 
"_liftPair" == "_lift2 (CONST Pair)" 
128 
"_liftCons" == "CONST lift2 (CONST Cons)" 

129 
"_liftApp" == "CONST lift2 (op @)" 

6255  130 
"_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)" 
131 
"_liftList x" == "_liftCons x (_const [])" 

3807  132 

17309  133 

3807  134 

6255  135 
"w = ~A" <= "_liftNot A w" 
136 
"w = A & B" <= "_liftAnd A B w" 

137 
"w = A  B" <= "_liftOr A B w" 

138 
"w = A > B" <= "_liftImp A B w" 

139 
"w = u = v" <= "_liftEqu u v w" 

9517
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset

140 
"w = ALL x. A" <= "_RAll x A w" 
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset

141 
"w = EX x. A" <= "_REx x A w" 
f58863b1406a
tuned version by Stephan Merz (unbatchified etc.);
wenzelm
parents:
7224
diff
changeset

142 
"w = EX! x. A" <= "_REx1 x A w" 
3807  143 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9517
diff
changeset

144 
syntax (xsymbols) 
17309  145 
"_Valid" :: "lift => bool" ("(\<turnstile> _)" 5) 
146 
"_holdsAt" :: "['a, lift] => bool" ("(_ \<Turnstile> _)" [100,10] 10) 

147 
"_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50) 

148 
"_liftNot" :: "lift => lift" ("\<not> _" [40] 40) 

149 
"_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35) 

150 
"_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30) 

151 
"_liftImp" :: "[lift, lift] => lift" (infixr "\<longrightarrow>" 25) 

152 
"_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10) 

153 
"_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10) 

154 
"_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10) 

155 
"_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50) 

156 
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50) 

157 
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50) 

3808  158 

6340  159 
syntax (HTML output) 
17309  160 
"_liftNeq" :: "[lift, lift] => lift" (infixl "\<noteq>" 50) 
161 
"_liftNot" :: "lift => lift" ("\<not> _" [40] 40) 

162 
"_liftAnd" :: "[lift, lift] => lift" (infixr "\<and>" 35) 

163 
"_liftOr" :: "[lift, lift] => lift" (infixr "\<or>" 30) 

164 
"_RAll" :: "[idts, lift] => lift" ("(3\<forall>_./ _)" [0, 10] 10) 

165 
"_REx" :: "[idts, lift] => lift" ("(3\<exists>_./ _)" [0, 10] 10) 

166 
"_REx1" :: "[idts, lift] => lift" ("(3\<exists>!_./ _)" [0, 10] 10) 

167 
"_liftLeq" :: "[lift, lift] => lift" ("(_/ \<le> _)" [50, 51] 50) 

168 
"_liftMem" :: "[lift, lift] => lift" ("(_/ \<in> _)" [50, 51] 50) 

169 
"_liftNotMem" :: "[lift, lift] => lift" ("(_/ \<notin> _)" [50, 51] 50) 

6340  170 

35318
e1b61c5fd494
dropped axclass, going back to purely syntactic type classes
haftmann
parents:
35108
diff
changeset

171 
defs 
17309  172 
Valid_def: " A == ALL w. w = A" 
173 

174 
unl_con: "LIFT #c w == c" 

21020  175 
unl_lift: "lift f x w == f (x w)" 
17309  176 
unl_lift2: "LIFT f<x, y> w == f (x w) (y w)" 
177 
unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)" 

3807  178 

17309  179 
unl_Rall: "w = ALL x. A x == ALL x. (w = A x)" 
180 
unl_Rex: "w = EX x. A x == EX x. (w = A x)" 

181 
unl_Rex1: "w = EX! x. A x == EX! x. (w = A x)" 

3807  182 

21624  183 

184 
subsection {* Lemmas and tactics for "intensional" logics. *} 

185 

186 
lemmas intensional_rews [simp] = 

187 
unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1 

188 

189 
lemma inteq_reflection: " x=y ==> (x==y)" 

190 
apply (unfold Valid_def unl_lift2) 

191 
apply (rule eq_reflection) 

192 
apply (rule ext) 

193 
apply (erule spec) 

194 
done 

195 

196 
lemma intI [intro!]: "(!!w. w = A) ==>  A" 

197 
apply (unfold Valid_def) 

198 
apply (rule allI) 

199 
apply (erule meta_spec) 

200 
done 

201 

202 
lemma intD [dest]: " A ==> w = A" 

203 
apply (unfold Valid_def) 

204 
apply (erule spec) 

205 
done 

206 

207 
(** Lift usual HOL simplifications to "intensional" level. **) 

208 

209 
lemma int_simps: 

210 
" (x=x) = #True" 

211 
" (~#True) = #False" " (~#False) = #True" " (~~ P) = P" 

212 
" ((~P) = P) = #False" " (P = (~P)) = #False" 

213 
" (P ~= Q) = (P = (~Q))" 

214 
" (#True=P) = P" " (P=#True) = P" 

215 
" (#True > P) = P" " (#False > P) = #True" 

216 
" (P > #True) = #True" " (P > P) = #True" 

217 
" (P > #False) = (~P)" " (P > ~P) = (~P)" 

218 
" (P & #True) = P" " (#True & P) = P" 

219 
" (P & #False) = #False" " (#False & P) = #False" 

220 
" (P & P) = P" " (P & ~P) = #False" " (~P & P) = #False" 

221 
" (P  #True) = #True" " (#True  P) = #True" 

222 
" (P  #False) = P" " (#False  P) = P" 

223 
" (P  P) = P" " (P  ~P) = #True" " (~P  P) = #True" 

224 
" (! x. P) = P" " (? x. P) = P" 

225 
" (~Q > ~P) = (P > Q)" 

226 
" (PQ > R) = ((P>R)&(Q>R))" 

227 
apply (unfold Valid_def intensional_rews) 

228 
apply blast+ 

229 
done 

230 

231 
declare int_simps [THEN inteq_reflection, simp] 

232 

233 
lemma TrueW [simp]: " #True" 

234 
by (simp add: Valid_def unl_con) 

235 

236 

237 

238 
(* ======== Functions to "unlift" intensional implications into HOL rules ====== *) 

239 

240 
ML {* 

241 
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. 

242 
 F = G becomes F w = G w 

243 
 F > G becomes F w > G w 

244 
*) 

245 

246 
fun int_unlift th = 

24180  247 
rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th); 
21624  248 

249 
(* Turn  F = G into metalevel rewrite rule F == G *) 

250 
fun int_rewrite th = 

24180  251 
zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection})) 
21624  252 

253 
(* flattening turns ">" into "==>" and eliminates conjunctions in the 

254 
antecedent. For example, 

255 

256 
P & Q > (R  S > T) becomes [ P; Q; R  S ] ==> T 

257 

258 
Flattening can be useful with "intensional" lemmas (after unlifting). 

259 
Naive resolution with mp and conjI may run away because of higherorder 

260 
unification, therefore the code is a little awkward. 

261 
*) 

262 
fun flatten t = 

263 
let 

264 
(* analogous to RS, but using matching instead of resolution *) 

265 
fun matchres tha i thb = 

31945  266 
case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of 
21624  267 
([th],_) => th 
268 
 ([],_) => raise THM("matchres: no match", i, [tha,thb]) 

269 
 _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) 

270 

271 
(* match tha with some premise of thb *) 

272 
fun matchsome tha thb = 

273 
let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) 

274 
 hmatch n = matchres tha n thb handle THM _ => hmatch (n1) 

275 
in hmatch (nprems_of thb) end 

276 

277 
fun hflatten t = 

278 
case (concl_of t) of 

38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38549
diff
changeset

279 
Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp) 
21624  280 
 _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t 
281 
in 

282 
hflatten t 

283 
end 

284 

285 
fun int_use th = 

286 
case (concl_of th) of 

287 
Const _ $ (Const ("Intensional.Valid", _) $ _) => 

288 
(flatten (int_unlift th) handle THM _ => th) 

289 
 _ => th 

290 
*} 

291 

42814  292 
attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} 
293 
attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} 

294 
attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} 

295 
attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} 

21624  296 

297 
lemma Not_Rall: " (~(! x. F x)) = (? x. ~F x)" 

298 
by (simp add: Valid_def) 

299 

300 
lemma Not_Rex: " (~ (? x. F x)) = (! x. ~ F x)" 

301 
by (simp add: Valid_def) 

302 

303 
end 