src/HOL/TLA/Intensional.thy
changeset 21624 6f79647cf536
parent 21020 9af9ceb16d58
child 24180 9f818139951b
     1.1 --- a/src/HOL/TLA/Intensional.thy	Fri Dec 01 17:22:33 2006 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Sat Dec 02 02:52:02 2006 +0100
     1.3 @@ -3,13 +3,10 @@
     1.4      ID:          $Id$
     1.5      Author:      Stephan Merz
     1.6      Copyright:   1998 University of Munich
     1.7 -
     1.8 -    Theory Name: Intensional
     1.9 -    Logic Image: HOL
    1.10 +*)
    1.11  
    1.12 -Define a framework for "intensional" (possible-world based) logics
    1.13 -on top of HOL, with lifting of constants and functions.
    1.14 -*)
    1.15 +header {* A framework for "intensional" (possible-world based) logics
    1.16 +  on top of HOL, with lifting of constants and functions *}
    1.17  
    1.18  theory Intensional
    1.19  imports Main
    1.20 @@ -188,6 +185,136 @@
    1.21    unl_Rex:     "w |= EX x. A x   ==  EX x. (w |= A x)"
    1.22    unl_Rex1:    "w |= EX! x. A x  ==  EX! x. (w |= A x)"
    1.23  
    1.24 -ML {* use_legacy_bindings (the_context ()) *}
    1.25 +
    1.26 +subsection {* Lemmas and tactics for "intensional" logics. *}
    1.27 +
    1.28 +lemmas intensional_rews [simp] =
    1.29 +  unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1
    1.30 +
    1.31 +lemma inteq_reflection: "|- x=y  ==>  (x==y)"
    1.32 +  apply (unfold Valid_def unl_lift2)
    1.33 +  apply (rule eq_reflection)
    1.34 +  apply (rule ext)
    1.35 +  apply (erule spec)
    1.36 +  done
    1.37 +
    1.38 +lemma intI [intro!]: "(!!w. w |= A) ==> |- A"
    1.39 +  apply (unfold Valid_def)
    1.40 +  apply (rule allI)
    1.41 +  apply (erule meta_spec)
    1.42 +  done
    1.43 +
    1.44 +lemma intD [dest]: "|- A ==> w |= A"
    1.45 +  apply (unfold Valid_def)
    1.46 +  apply (erule spec)
    1.47 +  done
    1.48 +
    1.49 +(** Lift usual HOL simplifications to "intensional" level. **)
    1.50 +
    1.51 +lemma int_simps:
    1.52 +  "|- (x=x) = #True"
    1.53 +  "|- (~#True) = #False"  "|- (~#False) = #True"  "|- (~~ P) = P"
    1.54 +  "|- ((~P) = P) = #False"  "|- (P = (~P)) = #False"
    1.55 +  "|- (P ~= Q) = (P = (~Q))"
    1.56 +  "|- (#True=P) = P"  "|- (P=#True) = P"
    1.57 +  "|- (#True --> P) = P"  "|- (#False --> P) = #True"
    1.58 +  "|- (P --> #True) = #True"  "|- (P --> P) = #True"
    1.59 +  "|- (P --> #False) = (~P)"  "|- (P --> ~P) = (~P)"
    1.60 +  "|- (P & #True) = P"  "|- (#True & P) = P"
    1.61 +  "|- (P & #False) = #False"  "|- (#False & P) = #False"
    1.62 +  "|- (P & P) = P"  "|- (P & ~P) = #False"  "|- (~P & P) = #False"
    1.63 +  "|- (P | #True) = #True"  "|- (#True | P) = #True"
    1.64 +  "|- (P | #False) = P"  "|- (#False | P) = P"
    1.65 +  "|- (P | P) = P"  "|- (P | ~P) = #True"  "|- (~P | P) = #True"
    1.66 +  "|- (! x. P) = P"  "|- (? x. P) = P"
    1.67 +  "|- (~Q --> ~P) = (P --> Q)"
    1.68 +  "|- (P|Q --> R) = ((P-->R)&(Q-->R))"
    1.69 +  apply (unfold Valid_def intensional_rews)
    1.70 +  apply blast+
    1.71 +  done
    1.72 +
    1.73 +declare int_simps [THEN inteq_reflection, simp]
    1.74 +
    1.75 +lemma TrueW [simp]: "|- #True"
    1.76 +  by (simp add: Valid_def unl_con)
    1.77 +
    1.78 +
    1.79 +
    1.80 +(* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
    1.81 +
    1.82 +ML {*
    1.83 +
    1.84 +local
    1.85 +  val intD = thm "intD";
    1.86 +  val inteq_reflection = thm "inteq_reflection";
    1.87 +  val intensional_rews = thms "intensional_rews";
    1.88 +in
    1.89 +
    1.90 +(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    1.91 +   |- F = G    becomes   F w = G w
    1.92 +   |- F --> G  becomes   F w --> G w
    1.93 +*)
    1.94 +
    1.95 +fun int_unlift th =
    1.96 +  rewrite_rule intensional_rews (th RS intD handle THM _ => th);
    1.97 +
    1.98 +(* Turn  |- F = G  into meta-level rewrite rule  F == G *)
    1.99 +fun int_rewrite th =
   1.100 +  zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection))
   1.101 +
   1.102 +(* flattening turns "-->" into "==>" and eliminates conjunctions in the
   1.103 +   antecedent. For example,
   1.104 +
   1.105 +         P & Q --> (R | S --> T)    becomes   [| P; Q; R | S |] ==> T
   1.106 +
   1.107 +   Flattening can be useful with "intensional" lemmas (after unlifting).
   1.108 +   Naive resolution with mp and conjI may run away because of higher-order
   1.109 +   unification, therefore the code is a little awkward.
   1.110 +*)
   1.111 +fun flatten t =
   1.112 +  let
   1.113 +    (* analogous to RS, but using matching instead of resolution *)
   1.114 +    fun matchres tha i thb =
   1.115 +      case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
   1.116 +          ([th],_) => th
   1.117 +        | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
   1.118 +        |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
   1.119 +
   1.120 +    (* match tha with some premise of thb *)
   1.121 +    fun matchsome tha thb =
   1.122 +      let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
   1.123 +            | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1)
   1.124 +      in hmatch (nprems_of thb) end
   1.125 +
   1.126 +    fun hflatten t =
   1.127 +        case (concl_of t) of
   1.128 +          Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
   1.129 +        | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
   1.130 +  in
   1.131 +    hflatten t
   1.132 +  end
   1.133 +
   1.134 +fun int_use th =
   1.135 +    case (concl_of th) of
   1.136 +      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   1.137 +              (flatten (int_unlift th) handle THM _ => th)
   1.138 +    | _ => th
   1.139  
   1.140  end
   1.141 +*}
   1.142 +
   1.143 +setup {*
   1.144 +  Attrib.add_attributes [
   1.145 +    ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
   1.146 +    ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
   1.147 +    ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
   1.148 +    ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
   1.149 +*}
   1.150 +
   1.151 +lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   1.152 +  by (simp add: Valid_def)
   1.153 +
   1.154 +lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)"
   1.155 +  by (simp add: Valid_def)
   1.156 +
   1.157 +end