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

src/HOL/TLA/Intensional.thy

author | haftmann |

Mon Aug 14 13:46:06 2006 +0200 (2006-08-14) | |

changeset 20380 | 14f9f2a1caa6 |

parent 17309 | c43ed29bd197 |

child 21020 | 9af9ceb16d58 |

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

simplified code generator setup

1 (*

2 File: TLA/Intensional.thy

3 ID: $Id$

4 Author: Stephan Merz

5 Copyright: 1998 University of Munich

7 Theory Name: Intensional

8 Logic Image: HOL

10 Define a framework for "intensional" (possible-world based) logics

11 on top of HOL, with lifting of constants and functions.

12 *)

14 theory Intensional

15 imports Main

16 begin

18 axclass

19 world < type

21 (** abstract syntax **)

23 types

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

25 'w form = "('w, bool) expr"

27 consts

28 Valid :: "('w::world) form => bool"

29 const :: "'a => ('w::world, 'a) expr"

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

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

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

34 (* "Rigid" quantification (logic level) *)

35 RAll :: "('a => ('w::world) form) => 'w form" (binder "Rall " 10)

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

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

39 (** concrete syntax **)

41 nonterminals

42 lift

43 liftargs

45 syntax

46 "" :: "id => lift" ("_")

47 "" :: "longid => lift" ("_")

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

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

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

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

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

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

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

55 "_Valid" :: "lift => bool" ("(|- _)" 5)

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

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

59 "LIFT" :: "lift => 'a" ("LIFT _")

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

62 "_const" :: "'a => lift" ("(#_)" [1000] 999)

63 "_lift" :: "['a, lift] => lift" ("(_<_>)" [1000] 999)

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

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

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

68 "_liftEqu" :: "[lift, lift] => lift" ("(_ =/ _)" [50,51] 50)

69 "_liftNeq" :: "[lift, lift] => lift" ("(_ ~=/ _)" [50,51] 50)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

87 (* infix syntax for list operations *)

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

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

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

92 (* Rigid quantification (syntax level) *)

93 "_ARAll" :: "[idts, lift] => lift" ("(3! _./ _)" [0, 10] 10)

94 "_AREx" :: "[idts, lift] => lift" ("(3? _./ _)" [0, 10] 10)

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

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

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

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

100 translations

101 "_const" == "const"

102 "_lift" == "lift"

103 "_lift2" == "lift2"

104 "_lift3" == "lift3"

105 "_Valid" == "Valid"

106 "_RAll x A" == "Rall x. A"

107 "_REx x A" == "Rex x. A"

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

109 "_ARAll" => "_RAll"

110 "_AREx" => "_REx"

111 "_AREx1" => "_REx1"

113 "w |= A" => "A w"

114 "LIFT A" => "A::_=>_"

116 "_liftEqu" == "_lift2 (op =)"

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

118 "_liftNot" == "_lift Not"

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

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

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

122 "_liftIf" == "_lift3 If"

123 "_liftPlus" == "_lift2 (op +)"

124 "_liftMinus" == "_lift2 (op -)"

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

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

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

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

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

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

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

132 "_liftFinset (_liftargs x xs)" == "_lift2 insert x (_liftFinset xs)"

133 "_liftFinset x" == "_lift2 insert x (_const {})"

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

135 "_liftPair" == "_lift2 Pair"

136 "_liftCons" == "lift2 Cons"

137 "_liftApp" == "lift2 (op @)"

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

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

143 "w |= ~A" <= "_liftNot A w"

144 "w |= A & B" <= "_liftAnd A B w"

145 "w |= A | B" <= "_liftOr A B w"

146 "w |= A --> B" <= "_liftImp A B w"

147 "w |= u = v" <= "_liftEqu u v w"

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

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

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

152 syntax (xsymbols)

153 "_Valid" :: "lift => bool" ("(\<turnstile> _)" 5)

154 "_holdsAt" :: "['a, lift] => bool" ("(_ \<Turnstile> _)" [100,10] 10)

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

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

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

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

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

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

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

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

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

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

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

167 syntax (HTML output)

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

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

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

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

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

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

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

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

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

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

179 axioms

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

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

183 unl_lift: "LIFT f<x> w == f (x w)"

184 unl_lift2: "LIFT f<x, y> w == f (x w) (y w)"

185 unl_lift3: "LIFT f<x, y, z> w == f (x w) (y w) (z w)"

187 unl_Rall: "w |= ALL x. A x == ALL x. (w |= A x)"

188 unl_Rex: "w |= EX x. A x == EX x. (w |= A x)"

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

191 ML {* use_legacy_bindings (the_context ()) *}

193 end