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

src/HOL/TLA/Intensional.thy

author | oheimb |

Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) | |

changeset 11008 | f7333f055ef6 |

parent 9517 | f58863b1406a |

child 12114 | a8e860c86252 |

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

improved theory reference in comment

1 (*

2 File: TLA/Intensional.thy

3 Author: Stephan Merz

4 Copyright: 1998 University of Munich

6 Theory Name: Intensional

7 Logic Image: HOL

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

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

11 *)

13 Intensional = Main +

15 axclass

16 world < term

18 (** abstract syntax **)

20 types

21 ('w,'a) expr = 'w => 'a (* intention: 'w::world, 'a::term *)

22 'w form = ('w, bool) expr

24 consts

25 Valid :: ('w::world) form => bool

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

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

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

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

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

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

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

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

36 (** concrete syntax **)

38 nonterminals

39 lift

40 liftargs

42 syntax

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

84 (* infix syntax for list operations *)

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

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

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

89 (* Rigid quantification (syntax level) *)

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

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

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

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

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

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

97 translations

98 "_const" == "const"

99 "_lift" == "lift"

100 "_lift2" == "lift2"

101 "_lift3" == "lift3"

102 "_Valid" == "Valid"

103 "_RAll x A" == "Rall x. A"

104 "_REx x A" == "Rex x. A"

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

106 "_ARAll" => "_RAll"

107 "_AREx" => "_REx"

108 "_AREx1" => "_REx1"

110 "w |= A" => "A w"

111 "LIFT A" => "A::_=>_"

113 "_liftEqu" == "_lift2 (op =)"

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

115 "_liftNot" == "_lift Not"

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

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

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

119 "_liftIf" == "_lift3 If"

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

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

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

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

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

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

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

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

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

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

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

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

132 "_liftPair" == "_lift2 Pair"

133 "_liftCons" == "lift2 Cons"

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

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

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

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

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

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

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

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

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

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

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

149 syntax (symbols)

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

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

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

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

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

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

156 "_liftImp" :: [lift, lift] => lift (infixr "\\<midarrow>\\<rightarrow>" 25)

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

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

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

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

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

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

164 syntax (HTML output)

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

167 rules

168 Valid_def "|- A == ALL w. w |= A"

170 unl_con "LIFT #c w == c"

171 unl_lift "LIFT f<x> w == f (x w)"

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

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

175 unl_Rall "w |= ALL x. A x == ALL x. (w |= A x)"

176 unl_Rex "w |= EX x. A x == EX x. (w |= A x)"

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

178 end