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.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
```