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