summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/TLA/Intensional.thy

author | wenzelm |

Sat Dec 14 17:28:05 2013 +0100 (2013-12-14) | |

changeset 54742 | 7a86358a3c0b |

parent 42814 | 5af15f1e2ef6 |

child 55382 | 9218fa411c15 |

permissions | -rw-r--r-- |

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;

clarified tool context in some boundary cases;

clarified tool context in some boundary cases;

1 (* Title: HOL/TLA/Intensional.thy

2 Author: Stephan Merz

3 Copyright: 1998 University of Munich

4 *)

6 header {* A framework for "intensional" (possible-world based) logics

7 on top of HOL, with lifting of constants and functions *}

9 theory Intensional

10 imports Main

11 begin

13 classes world

14 classrel world < type

16 (** abstract syntax **)

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

19 type_synonym 'w form = "('w, bool) expr"

21 consts

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"

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)

33 (** concrete syntax **)

35 nonterminal lift and liftargs

37 syntax

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)

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

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

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

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)

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

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" ("{(_)}")

77 (** TODO: syntax for lifted collection / comprehension **)

78 "_liftPair" :: "[lift,liftargs] => lift" ("(1'(_,/ _'))")

79 (* infix syntax for list operations *)

80 "_liftCons" :: "[lift, lift] => lift" ("(_ #/ _)" [65,66] 65)

81 "_liftApp" :: "[lift, lift] => lift" ("(_ @/ _)" [65,66] 65)

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

84 (* Rigid quantification (syntax level) *)

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)

92 translations

93 "_const" == "CONST const"

94 "_lift" == "CONST lift"

95 "_lift2" == "CONST lift2"

96 "_lift3" == "CONST lift3"

97 "_Valid" == "CONST Valid"

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"

105 "w |= A" => "A w"

106 "LIFT A" => "A::_=>_"

108 "_liftEqu" == "_lift2 (op =)"

109 "_liftNeq u v" == "_liftNot (_liftEqu u v)"

110 "_liftNot" == "_lift (CONST Not)"

111 "_liftAnd" == "_lift2 (op &)"

112 "_liftOr" == "_lift2 (op | )"

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

114 "_liftIf" == "_lift3 (CONST If)"

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)"

124 "_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)"

125 "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"

126 "_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)"

127 "_liftPair" == "_lift2 (CONST Pair)"

128 "_liftCons" == "CONST lift2 (CONST Cons)"

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

130 "_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)"

131 "_liftList x" == "_liftCons x (_const [])"

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"

140 "w |= ALL x. A" <= "_RAll x A w"

141 "w |= EX x. A" <= "_REx x A w"

142 "w |= EX! x. A" <= "_REx1 x A w"

144 syntax (xsymbols)

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)

159 syntax (HTML output)

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)

171 defs

172 Valid_def: "|- A == ALL w. w |= A"

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

175 unl_lift: "lift f x w == f (x w)"

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)"

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)"

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

186 lemmas intensional_rews [simp] =

187 unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1

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

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

197 apply (unfold Valid_def)

198 apply (rule allI)

199 apply (erule meta_spec)

200 done

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

203 apply (unfold Valid_def)

204 apply (erule spec)

205 done

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

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 "|- (P|Q --> R) = ((P-->R)&(Q-->R))"

227 apply (unfold Valid_def intensional_rews)

228 apply blast+

229 done

231 declare int_simps [THEN inteq_reflection, simp]

233 lemma TrueW [simp]: "|- #True"

234 by (simp add: Valid_def unl_con)

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

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 *)

246 fun int_unlift ctxt th =

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

249 (* Turn |- F = G into meta-level rewrite rule F == G *)

250 fun int_rewrite ctxt th =

251 zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))

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

254 antecedent. For example,

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

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

259 Naive resolution with mp and conjI may run away because of higher-order

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 =

266 case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of

267 ([th],_) => th

268 | ([],_) => raise THM("matchres: no match", i, [tha,thb])

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

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 (n-1)

275 in hmatch (nprems_of thb) end

277 fun hflatten t =

278 case (concl_of t) of

279 Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)

280 | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t

281 in

282 hflatten t

283 end

285 fun int_use ctxt th =

286 case (concl_of th) of

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

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

289 | _ => th

290 *}

292 attribute_setup int_unlift =

293 {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}

294 attribute_setup int_rewrite =

295 {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}

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

297 attribute_setup int_use =

298 {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}

300 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"

301 by (simp add: Valid_def)

303 lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)"

304 by (simp add: Valid_def)

306 end