src/HOL/TLA/Intensional.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:	 Intensional.ML
     3     Author:      Stephan Merz
     4     Copyright:   1998 University of Munich
     5 
     6 Lemmas and tactics for "intensional" logics.
     7 *)
     8 
     9 val intensional_rews = [unl_con,unl_lift,unl_lift2,unl_lift3,unl_Rall,unl_Rex,unl_Rex1];
    10 
    11 qed_goalw "inteq_reflection" Intensional.thy  [Valid_def,unl_lift2]
    12   "|- x=y  ==>  (x==y)"
    13   (fn [prem] => [rtac eq_reflection 1, rtac ext 1, rtac (prem RS spec) 1 ]);
    14 
    15 qed_goalw "intI" Intensional.thy [Valid_def] "(!!w. w |= A) ==> |- A"
    16   (fn [prem] => [REPEAT (resolve_tac [allI,prem] 1)]);
    17 
    18 qed_goalw "intD" Intensional.thy [Valid_def] "|- A ==> w |= A"
    19   (fn [prem] => [rtac (prem RS spec) 1]);
    20 
    21 
    22 (** Lift usual HOL simplifications to "intensional" level. **)
    23 local
    24 
    25 fun prover s = (prove_goal Intensional.thy s 
    26                  (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews), 
    27                            blast_tac HOL_cs 1])) RS inteq_reflection
    28 
    29 in
    30 
    31 val int_simps = map prover
    32  [ "|- (x=x) = #True",
    33    "|- (~#True) = #False", "|- (~#False) = #True", "|- (~~ P) = P",
    34    "|- ((~P) = P) = #False", "|- (P = (~P)) = #False", 
    35    "|- (P ~= Q) = (P = (~Q))",
    36    "|- (#True=P) = P", "|- (P=#True) = P",
    37    "|- (#True --> P) = P", "|- (#False --> P) = #True", 
    38    "|- (P --> #True) = #True", "|- (P --> P) = #True",
    39    "|- (P --> #False) = (~P)", "|- (P --> ~P) = (~P)",
    40    "|- (P & #True) = P", "|- (#True & P) = P", 
    41    "|- (P & #False) = #False", "|- (#False & P) = #False", 
    42    "|- (P & P) = P", "|- (P & ~P) = #False", "|- (~P & P) = #False",
    43    "|- (P | #True) = #True", "|- (#True | P) = #True", 
    44    "|- (P | #False) = P", "|- (#False | P) = P", 
    45    "|- (P | P) = P", "|- (P | ~P) = #True", "|- (~P | P) = #True",
    46    "|- (! x. P) = P", "|- (? x. P) = P", 
    47    "|- (~Q --> ~P) = (P --> Q)",
    48    "|- (P|Q --> R) = ((P-->R)&(Q-->R))" ];
    49 end;
    50 
    51 qed_goal "TrueW" Intensional.thy "|- #True"
    52   (fn _ => [simp_tac (simpset() addsimps [Valid_def,unl_con]) 1]);
    53 
    54 Addsimps (TrueW::intensional_rews);
    55 Addsimps int_simps;
    56 AddSIs [intI];
    57 AddDs  [intD];
    58 
    59 
    60 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
    61 
    62 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    63    |- F = G    becomes   F w = G w
    64    |- F --> G  becomes   F w --> G w
    65 *)
    66 
    67 fun int_unlift th =
    68   rewrite_rule intensional_rews ((th RS intD) handle _ => th);
    69 
    70 (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
    71 fun int_rewrite th = 
    72     zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection));
    73 
    74 (* flattening turns "-->" into "==>" and eliminates conjunctions in the
    75    antecedent. For example,
    76 
    77          P & Q --> (R | S --> T)    becomes   [| P; Q; R | S |] ==> T
    78 
    79    Flattening can be useful with "intensional" lemmas (after unlifting).
    80    Naive resolution with mp and conjI may run away because of higher-order
    81    unification, therefore the code is a little awkward.
    82 *)
    83 fun flatten t =
    84   let 
    85     (* analogous to RS, but using matching instead of resolution *)
    86     fun matchres tha i thb =
    87       case Seq.chop (2, biresolution true [(false,tha)] i thb) of
    88 	  ([th],_) => th
    89 	| ([],_)   => raise THM("matchres: no match", i, [tha,thb])
    90 	|      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])
    91 
    92     (* match tha with some premise of thb *)
    93     fun matchsome tha thb =
    94       let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
    95 	    | hmatch n = (matchres tha n thb) handle _ => hmatch (n-1)
    96       in hmatch (nprems_of thb) end
    97 
    98     fun hflatten t =
    99         case (concl_of t) of
   100           Const _ $ (Const ("op -->", _) $ _ $ _) => hflatten (t RS mp)
   101         | _ => (hflatten (matchsome conjI t)) handle _ => zero_var_indexes t
   102   in
   103     hflatten t
   104 end;
   105 
   106 fun int_use th =
   107     case (concl_of th) of
   108       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
   109               ((flatten (int_unlift th)) handle _ => th)
   110     | _ => th;
   111 
   112 (***
   113 (* Make the simplifier accept "intensional" goals by either turning them into
   114    a meta-equality or by unlifting them.
   115 *)
   116 
   117 let 
   118   val ss = simpset_ref()
   119   fun try_rewrite th = (int_rewrite th) handle _ => (int_use th) handle _ => th
   120 in 
   121   ss := !ss setmksimps ((mksimps mksimps_pairs) o try_rewrite)
   122 end;
   123 ***)
   124 
   125 (* ========================================================================= *)
   126 
   127 qed_goal "Not_Rall" Intensional.thy
   128    "|- (~(! x. F x)) = (? x. ~F x)"
   129    (fn _ => [simp_tac (simpset() addsimps [Valid_def]) 1]);
   130 
   131 qed_goal "Not_Rex" Intensional.thy
   132    "|- (~ (? x. F x)) = (! x. ~ F x)"
   133    (fn _ => [simp_tac (simpset() addsimps [Valid_def]) 1]);
   134 
   135 (* IntLemmas.ML contains a collection of further lemmas about "intensional" logic.
   136    These are not loaded by default because they are not required for the
   137    standard proof procedures that first unlift proof goals to the HOL level.
   138 
   139 use "IntLemmas.ML";
   140 
   141 *)