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