1(* Title: HOL/TLA/Intensional.thy 2 Author: Stephan Merz 3 Copyright: 1998 University of Munich 4*) 5 6section \<open>A framework for "intensional" (possible-world based) logics 7 on top of HOL, with lifting of constants and functions\<close> 8 9theory Intensional 10imports Main 11begin 12 13class world 14 15(** abstract syntax **) 16 17type_synonym ('w,'a) expr = "'w \<Rightarrow> 'a" (* intention: 'w::world, 'a::type *) 18type_synonym 'w form = "('w, bool) expr" 19 20definition Valid :: "('w::world) form \<Rightarrow> bool" 21 where "Valid A \<equiv> \<forall>w. A w" 22 23definition const :: "'a \<Rightarrow> ('w::world, 'a) expr" 24 where unl_con: "const c w \<equiv> c" 25 26definition lift :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr" 27 where unl_lift: "lift f x w \<equiv> f (x w)" 28 29definition lift2 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr" 30 where unl_lift2: "lift2 f x y w \<equiv> f (x w) (y w)" 31 32definition lift3 :: "['a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr" 33 where unl_lift3: "lift3 f x y z w \<equiv> f (x w) (y w) (z w)" 34 35(* "Rigid" quantification (logic level) *) 36definition RAll :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rall " 10) 37 where unl_Rall: "(Rall x. A x) w \<equiv> \<forall>x. A x w" 38definition REx :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex " 10) 39 where unl_Rex: "(Rex x. A x) w \<equiv> \<exists>x. A x w" 40definition REx1 :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form" (binder "Rex! " 10) 41 where unl_Rex1: "(Rex! x. A x) w \<equiv> \<exists>!x. A x w" 42 43 44(** concrete syntax **) 45 46nonterminal lift and liftargs 47 48syntax 49 "" :: "id \<Rightarrow> lift" ("_") 50 "" :: "longid \<Rightarrow> lift" ("_") 51 "" :: "var \<Rightarrow> lift" ("_") 52 "_applC" :: "[lift, cargs] \<Rightarrow> lift" ("(1_/ _)" [1000, 1000] 999) 53 "" :: "lift \<Rightarrow> lift" ("'(_')") 54 "_lambda" :: "[idts, 'a] \<Rightarrow> lift" ("(3\<lambda>_./ _)" [0, 3] 3) 55 "_constrain" :: "[lift, type] \<Rightarrow> lift" ("(_::_)" [4, 0] 3) 56 "" :: "lift \<Rightarrow> liftargs" ("_") 57 "_liftargs" :: "[lift, liftargs] \<Rightarrow> liftargs" ("_,/ _") 58 "_Valid" :: "lift \<Rightarrow> bool" ("(\<turnstile> _)" 5) 59 "_holdsAt" :: "['a, lift] \<Rightarrow> bool" ("(_ \<Turnstile> _)" [100,10] 10) 60 61 (* Syntax for lifted expressions outside the scope of \<turnstile> or |= *) 62 "_LIFT" :: "lift \<Rightarrow> 'a" ("LIFT _") 63 64 (* generic syntax for lifted constants and functions *) 65 "_const" :: "'a \<Rightarrow> lift" ("(#_)" [1000] 999) 66 "_lift" :: "['a, lift] \<Rightarrow> lift" ("(_<_>)" [1000] 999) 67 "_lift2" :: "['a, lift, lift] \<Rightarrow> lift" ("(_<_,/ _>)" [1000] 999) 68 "_lift3" :: "['a, lift, lift, lift] \<Rightarrow> lift" ("(_<_,/ _,/ _>)" [1000] 999) 69 70 (* concrete syntax for common infix functions: reuse same symbol *) 71 "_liftEqu" :: "[lift, lift] \<Rightarrow> lift" ("(_ =/ _)" [50,51] 50) 72 "_liftNeq" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<noteq>/ _)" [50,51] 50) 73 "_liftNot" :: "lift \<Rightarrow> lift" ("(\<not> _)" [40] 40) 74 "_liftAnd" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<and>/ _)" [36,35] 35) 75 "_liftOr" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<or>/ _)" [31,30] 30) 76 "_liftImp" :: "[lift, lift] \<Rightarrow> lift" ("(_ \<longrightarrow>/ _)" [26,25] 25) 77 "_liftIf" :: "[lift, lift, lift] \<Rightarrow> lift" ("(if (_)/ then (_)/ else (_))" 10) 78 "_liftPlus" :: "[lift, lift] \<Rightarrow> lift" ("(_ +/ _)" [66,65] 65) 79 "_liftMinus" :: "[lift, lift] \<Rightarrow> lift" ("(_ -/ _)" [66,65] 65) 80 "_liftTimes" :: "[lift, lift] \<Rightarrow> lift" ("(_ */ _)" [71,70] 70) 81 "_liftDiv" :: "[lift, lift] \<Rightarrow> lift" ("(_ div _)" [71,70] 70) 82 "_liftMod" :: "[lift, lift] \<Rightarrow> lift" ("(_ mod _)" [71,70] 70) 83 "_liftLess" :: "[lift, lift] \<Rightarrow> lift" ("(_/ < _)" [50, 51] 50) 84 "_liftLeq" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<le> _)" [50, 51] 50) 85 "_liftMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<in> _)" [50, 51] 50) 86 "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift" ("(_/ \<notin> _)" [50, 51] 50) 87 "_liftFinset" :: "liftargs \<Rightarrow> lift" ("{(_)}") 88 (** TODO: syntax for lifted collection / comprehension **) 89 "_liftPair" :: "[lift,liftargs] \<Rightarrow> lift" ("(1'(_,/ _'))") 90 (* infix syntax for list operations *) 91 "_liftCons" :: "[lift, lift] \<Rightarrow> lift" ("(_ #/ _)" [65,66] 65) 92 "_liftApp" :: "[lift, lift] \<Rightarrow> lift" ("(_ @/ _)" [65,66] 65) 93 "_liftList" :: "liftargs \<Rightarrow> lift" ("[(_)]") 94 95 (* Rigid quantification (syntax level) *) 96 "_RAll" :: "[idts, lift] \<Rightarrow> lift" ("(3\<forall>_./ _)" [0, 10] 10) 97 "_REx" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>_./ _)" [0, 10] 10) 98 "_REx1" :: "[idts, lift] \<Rightarrow> lift" ("(3\<exists>!_./ _)" [0, 10] 10) 99 100translations 101 "_const" == "CONST const" 102 "_lift" == "CONST lift" 103 "_lift2" == "CONST lift2" 104 "_lift3" == "CONST lift3" 105 "_Valid" == "CONST Valid" 106 "_RAll x A" == "Rall x. A" 107 "_REx x A" == "Rex x. A" 108 "_REx1 x A" == "Rex! x. A" 109 110 "w \<Turnstile> A" => "A w" 111 "LIFT A" => "A::_\<Rightarrow>_" 112 113 "_liftEqu" == "_lift2 (=)" 114 "_liftNeq u v" == "_liftNot (_liftEqu u v)" 115 "_liftNot" == "_lift (CONST Not)" 116 "_liftAnd" == "_lift2 (\<and>)" 117 "_liftOr" == "_lift2 (\<or>)" 118 "_liftImp" == "_lift2 (\<longrightarrow>)" 119 "_liftIf" == "_lift3 (CONST If)" 120 "_liftPlus" == "_lift2 (+)" 121 "_liftMinus" == "_lift2 (-)" 122 "_liftTimes" == "_lift2 ((*))" 123 "_liftDiv" == "_lift2 (div)" 124 "_liftMod" == "_lift2 (mod)" 125 "_liftLess" == "_lift2 (<)" 126 "_liftLeq" == "_lift2 (\<le>)" 127 "_liftMem" == "_lift2 (\<in>)" 128 "_liftNotMem x xs" == "_liftNot (_liftMem x xs)" 129 "_liftFinset (_liftargs x xs)" == "_lift2 (CONST insert) x (_liftFinset xs)" 130 "_liftFinset x" == "_lift2 (CONST insert) x (_const {})" 131 "_liftPair x (_liftargs y z)" == "_liftPair x (_liftPair y z)" 132 "_liftPair" == "_lift2 (CONST Pair)" 133 "_liftCons" == "CONST lift2 (CONST Cons)" 134 "_liftApp" == "CONST lift2 (@)" 135 "_liftList (_liftargs x xs)" == "_liftCons x (_liftList xs)" 136 "_liftList x" == "_liftCons x (_const [])" 137 138 "w \<Turnstile> \<not>A" <= "_liftNot A w" 139 "w \<Turnstile> A \<and> B" <= "_liftAnd A B w" 140 "w \<Turnstile> A \<or> B" <= "_liftOr A B w" 141 "w \<Turnstile> A \<longrightarrow> B" <= "_liftImp A B w" 142 "w \<Turnstile> u = v" <= "_liftEqu u v w" 143 "w \<Turnstile> \<forall>x. A" <= "_RAll x A w" 144 "w \<Turnstile> \<exists>x. A" <= "_REx x A w" 145 "w \<Turnstile> \<exists>!x. A" <= "_REx1 x A w" 146 147 148subsection \<open>Lemmas and tactics for "intensional" logics.\<close> 149 150lemmas intensional_rews [simp] = 151 unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1 152 153lemma inteq_reflection: "\<turnstile> x=y \<Longrightarrow> (x==y)" 154 apply (unfold Valid_def unl_lift2) 155 apply (rule eq_reflection) 156 apply (rule ext) 157 apply (erule spec) 158 done 159 160lemma intI [intro!]: "(\<And>w. w \<Turnstile> A) \<Longrightarrow> \<turnstile> A" 161 apply (unfold Valid_def) 162 apply (rule allI) 163 apply (erule meta_spec) 164 done 165 166lemma intD [dest]: "\<turnstile> A \<Longrightarrow> w \<Turnstile> A" 167 apply (unfold Valid_def) 168 apply (erule spec) 169 done 170 171(** Lift usual HOL simplifications to "intensional" level. **) 172 173lemma int_simps: 174 "\<turnstile> (x=x) = #True" 175 "\<turnstile> (\<not>#True) = #False" "\<turnstile> (\<not>#False) = #True" "\<turnstile> (\<not>\<not> P) = P" 176 "\<turnstile> ((\<not>P) = P) = #False" "\<turnstile> (P = (\<not>P)) = #False" 177 "\<turnstile> (P \<noteq> Q) = (P = (\<not>Q))" 178 "\<turnstile> (#True=P) = P" "\<turnstile> (P=#True) = P" 179 "\<turnstile> (#True \<longrightarrow> P) = P" "\<turnstile> (#False \<longrightarrow> P) = #True" 180 "\<turnstile> (P \<longrightarrow> #True) = #True" "\<turnstile> (P \<longrightarrow> P) = #True" 181 "\<turnstile> (P \<longrightarrow> #False) = (\<not>P)" "\<turnstile> (P \<longrightarrow> \<not>P) = (\<not>P)" 182 "\<turnstile> (P \<and> #True) = P" "\<turnstile> (#True \<and> P) = P" 183 "\<turnstile> (P \<and> #False) = #False" "\<turnstile> (#False \<and> P) = #False" 184 "\<turnstile> (P \<and> P) = P" "\<turnstile> (P \<and> \<not>P) = #False" "\<turnstile> (\<not>P \<and> P) = #False" 185 "\<turnstile> (P \<or> #True) = #True" "\<turnstile> (#True \<or> P) = #True" 186 "\<turnstile> (P \<or> #False) = P" "\<turnstile> (#False \<or> P) = P" 187 "\<turnstile> (P \<or> P) = P" "\<turnstile> (P \<or> \<not>P) = #True" "\<turnstile> (\<not>P \<or> P) = #True" 188 "\<turnstile> (\<forall>x. P) = P" "\<turnstile> (\<exists>x. P) = P" 189 "\<turnstile> (\<not>Q \<longrightarrow> \<not>P) = (P \<longrightarrow> Q)" 190 "\<turnstile> (P\<or>Q \<longrightarrow> R) = ((P\<longrightarrow>R)\<and>(Q\<longrightarrow>R))" 191 apply (unfold Valid_def intensional_rews) 192 apply blast+ 193 done 194 195declare int_simps [THEN inteq_reflection, simp] 196 197lemma TrueW [simp]: "\<turnstile> #True" 198 by (simp add: Valid_def unl_con) 199 200 201 202(* ======== Functions to "unlift" intensional implications into HOL rules ====== *) 203 204ML \<open> 205(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g. 206 \<turnstile> F = G becomes F w = G w 207 \<turnstile> F \<longrightarrow> G becomes F w \<longrightarrow> G w 208*) 209 210fun int_unlift ctxt th = 211 rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th); 212 213(* Turn \<turnstile> F = G into meta-level rewrite rule F == G *) 214fun int_rewrite ctxt th = 215 zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection})) 216 217(* flattening turns "\<longrightarrow>" into "\<Longrightarrow>" and eliminates conjunctions in the 218 antecedent. For example, 219 220 P & Q \<longrightarrow> (R | S \<longrightarrow> T) becomes \<lbrakk> P; Q; R | S \<rbrakk> \<Longrightarrow> T 221 222 Flattening can be useful with "intensional" lemmas (after unlifting). 223 Naive resolution with mp and conjI may run away because of higher-order 224 unification, therefore the code is a little awkward. 225*) 226fun flatten t = 227 let 228 (* analogous to RS, but using matching instead of resolution *) 229 fun matchres tha i thb = 230 case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of 231 ([th],_) => th 232 | ([],_) => raise THM("matchres: no match", i, [tha,thb]) 233 | _ => raise THM("matchres: multiple unifiers", i, [tha,thb]) 234 235 (* match tha with some premise of thb *) 236 fun matchsome tha thb = 237 let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb]) 238 | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1) 239 in hmatch (Thm.nprems_of thb) end 240 241 fun hflatten t = 242 case Thm.concl_of t of 243 Const _ $ (Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _) => hflatten (t RS mp) 244 | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t 245 in 246 hflatten t 247 end 248 249fun int_use ctxt th = 250 case Thm.concl_of th of 251 Const _ $ (Const (\<^const_name>\<open>Valid\<close>, _) $ _) => 252 (flatten (int_unlift ctxt th) handle THM _ => th) 253 | _ => th 254\<close> 255 256attribute_setup int_unlift = 257 \<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close> 258attribute_setup int_rewrite = 259 \<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close> 260attribute_setup flatten = 261 \<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close> 262attribute_setup int_use = 263 \<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close> 264 265lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)" 266 by (simp add: Valid_def) 267 268lemma Not_Rex: "\<turnstile> (\<not> (\<exists>x. F x)) = (\<forall>x. \<not> F x)" 269 by (simp add: Valid_def) 270 271end 272