src/HOL/TLA/Intensional.ML

document setup;

(* 
    File:	 Intensional.ML
    Author:      Stephan Merz
    Copyright:   1998 University of Munich

Lemmas and tactics for "intensional" logics.
*)

val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex,unl_Rex1];

Goalw [Valid_def,unl_lift2] "|- x=y  ==>  (x==y)";
by (rtac eq_reflection 1);
by (rtac ext 1);
by (etac spec 1);
qed "inteq_reflection";

val [prem] = goalw thy [Valid_def] "(!!w. w |= A) ==> |- A";
by (REPEAT (resolve_tac [allI,prem] 1));
qed "intI";

Goalw [Valid_def] "|- A ==> w |= A";
by (etac spec 1);
qed "intD";

(** Lift usual HOL simplifications to "intensional" level. **)
local

fun prover s = (prove_goal Intensional.thy s 
                 (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews), 
                           blast_tac HOL_cs 1])) RS inteq_reflection

in

val int_simps = map prover
 [ "|- (x=x) = #True",
   "|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P",
   "|- ((~P) = P) = #False", "|- (P = (~P)) = #False", 
   "|- (P ~= Q) = (P = (~Q))",
   "|- (#True=P) = P", "|- (P=#True) = P",
   "|- (#True --> P) = P", "|- (#False --> P) = #True", 
   "|- (P --> #True) = #True", "|- (P --> P) = #True",
   "|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)",
   "|- (P & #True) = P", "|- (#True & P) = P", 
   "|- (P & #False) = #False", "|- (#False & P) = #False", 
   "|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False",
   "|- (P | #True) = #True", "|- (#True | P) = #True", 
   "|- (P | #False) = P", "|- (#False | P) = P", 
   "|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True",
   "|- (! x. P) = P", "|- (? x. P) = P", 
   "|- (~Q --> ~P) = (P --> Q)",
   "|- (P|Q --> R) = ((P-->R)&(Q-->R))" ]
end;

Goal "|- #True";
by (simp_tac (simpset() addsimps [Valid_def,unl_con]) 1);
qed "TrueW";

Addsimps (TrueW::intensional_rews);
Addsimps int_simps;
AddSIs [intI];
AddDs  [intD];


(* ======== Functions to "unlift" intensional implications into HOL rules ====== *)

(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
   |- F = G    becomes   F w = G w
   |- F --> G  becomes   F w --> G w
*)

fun int_unlift th =
  rewrite_rule intensional_rews ((th RS intD) handle _ => th);

(* Turn  |- F = G  into meta-level rewrite rule  F == G *)
fun int_rewrite th = 
    zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection));

(* flattening turns "-->" into "==>" and eliminates conjunctions in the
   antecedent. For example,

         P & Q --> (R | S --> T)    becomes   [| P; Q; R | S |] ==> T

   Flattening can be useful with "intensional" lemmas (after unlifting).
   Naive resolution with mp and conjI may run away because of higher-order
   unification, therefore the code is a little awkward.
*)
fun flatten t =
  let 
    (* analogous to RS, but using matching instead of resolution *)
    fun matchres tha i thb =
      case Seq.chop (2, biresolution true [(false,tha)] i thb) of
	  ([th],_) => th
	| ([],_)   => raise THM("matchres: no match", i, [tha,thb])
	|      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])

    (* match tha with some premise of thb *)
    fun matchsome tha thb =
      let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
	    | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
      in hmatch (nprems_of thb) end

    fun hflatten t =
        case (concl_of t) of
          Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
        | _ => (hflatten (matchsome conjI t)) handle _ => zero_var_indexes t
  in
    hflatten t
end;

fun int_use th =
    case (concl_of th) of
      Const _ $ (Const ("Intensional.Valid", _) $ _) =>
              ((flatten (int_unlift th)) handle _ => th)
    | _ => th;

(* ========================================================================= *)

Goalw [Valid_def] "|- (~(! x. F x)) = (? x. ~F x)";
by (Simp_tac 1);
qed "Not_Rall";

Goalw [Valid_def] "|- (~ (? x. F x)) = (! x. ~ F x)";
by (Simp_tac 1);
qed "Not_Rex";