src/HOL/TLA/Intensional.ML
author wenzelm
Mon Jun 12 21:19:00 2006 +0200 (2006-06-12)
changeset 19861 620d90091788
parent 17309 c43ed29bd197
permissions -rw-r--r--
tuned Seq/Envir/Unify interfaces;
     1 (*
     2     File:        Intensional.ML
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1998 University of Munich
     6 
     7 Lemmas and tactics for "intensional" logics.
     8 *)
     9 
    10 val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex,unl_Rex1];
    11 
    12 Goalw [Valid_def,unl_lift2] "|- x=y  ==>  (x==y)";
    13 by (rtac eq_reflection 1);
    14 by (rtac ext 1);
    15 by (etac spec 1);
    16 qed "inteq_reflection";
    17 
    18 val [prem] = goalw (the_context ()) [Valid_def] "(!!w. w |= A) ==> |- A";
    19 by (REPEAT (resolve_tac [allI,prem] 1));
    20 qed "intI";
    21 
    22 Goalw [Valid_def] "|- A ==> w |= A";
    23 by (etac spec 1);
    24 qed "intD";
    25 
    26 (** Lift usual HOL simplifications to "intensional" level. **)
    27 local
    28 
    29 fun prover s = (prove_goal (the_context ()) s
    30                  (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews),
    31                            blast_tac HOL_cs 1])) RS inteq_reflection
    32 
    33 in
    34 
    35 val int_simps = map prover
    36  [ "|- (x=x) = #True",
    37    "|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P",
    38    "|- ((~P) = P) = #False", "|- (P = (~P)) = #False",
    39    "|- (P ~= Q) = (P = (~Q))",
    40    "|- (#True=P) = P", "|- (P=#True) = P",
    41    "|- (#True --> P) = P", "|- (#False --> P) = #True",
    42    "|- (P --> #True) = #True", "|- (P --> P) = #True",
    43    "|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)",
    44    "|- (P & #True) = P", "|- (#True & P) = P",
    45    "|- (P & #False) = #False", "|- (#False & P) = #False",
    46    "|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False",
    47    "|- (P | #True) = #True", "|- (#True | P) = #True",
    48    "|- (P | #False) = P", "|- (#False | P) = P",
    49    "|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True",
    50    "|- (! x. P) = P", "|- (? x. P) = P",
    51    "|- (~Q --> ~P) = (P --> Q)",
    52    "|- (P|Q --> R) = ((P-->R)&(Q-->R))" ]
    53 end;
    54 
    55 Goal "|- #True";
    56 by (simp_tac (simpset() addsimps [Valid_def,unl_con]) 1);
    57 qed "TrueW";
    58 
    59 Addsimps (TrueW::intensional_rews);
    60 Addsimps int_simps;
    61 AddSIs [intI];
    62 AddDs  [intD];
    63 
    64 
    65 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
    66 
    67 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    68    |- F = G    becomes   F w = G w
    69    |- F --> G  becomes   F w --> G w
    70 *)
    71 
    72 fun int_unlift th =
    73   rewrite_rule intensional_rews ((th RS intD) handle _ => th);
    74 
    75 (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
    76 fun int_rewrite th =
    77     zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection));
    78 
    79 (* flattening turns "-->" into "==>" and eliminates conjunctions in the
    80    antecedent. For example,
    81 
    82          P & Q --> (R | S --> T)    becomes   [| P; Q; R | S |] ==> T
    83 
    84    Flattening can be useful with "intensional" lemmas (after unlifting).
    85    Naive resolution with mp and conjI may run away because of higher-order
    86    unification, therefore the code is a little awkward.
    87 *)
    88 fun flatten t =
    89   let
    90     (* analogous to RS, but using matching instead of resolution *)
    91     fun matchres tha i thb =
    92       case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
    93           ([th],_) => th
    94         | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
    95         |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
    96 
    97     (* match tha with some premise of thb *)
    98     fun matchsome tha thb =
    99       let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
   100             | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
   101       in hmatch (nprems_of thb) end
   102 
   103     fun hflatten t =
   104         case (concl_of t) of
   105           Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
   106         | _ => (hflatten (matchsome conjI t)) handle _ => zero_var_indexes t
   107   in
   108     hflatten t
   109 end;
   110 
   111 fun int_use th =
   112     case (concl_of th) of
   113       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   114               ((flatten (int_unlift th)) handle _ => th)
   115     | _ => th;
   116 
   117 (* ========================================================================= *)
   118 
   119 Goalw [Valid_def] "|- (~(! x. F x)) = (? x. ~F x)";
   120 by (Simp_tac 1);
   121 qed "Not_Rall";
   122 
   123 Goalw [Valid_def] "|- (~ (? x. F x)) = (! x. ~ F x)";
   124 by (Simp_tac 1);
   125 qed "Not_Rex";