turned translation for 1::nat into def.
introduced 1' and replaced most occurrences of 1 by 1'.
(*
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";