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