(*
File: IntLemmas.ML
Author: Stephan Merz
Copyright: 1997 University of Munich
Lemmas and tactics for "intensional" logics.
Mostly a lifting of standard HOL lemmas. They are not required in standard
reasoning about intensional logics, which starts by unlifting proof goals
to the HOL level.
*)
qed_goal "substW" Intensional.thy
"[| x .= y; w |= (P::[('v::world) => 'a, 'w::world] => bool)(x) |] ==> w |= P(y)"
(fn [prem1,prem2] => [rtac (rewrite_rule ([prem1] RL [inteq_reflection]) prem2) 1]);
(* Lift HOL rules to intensional reasoning *)
qed_goal "reflW" Intensional.thy "x .= x"
(fn _ => [ rtac intI 1,
rewrite_goals_tac intensional_rews,
rtac refl 1 ]);
qed_goal "symW" Intensional.thy "s .= t ==> t .= s"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1, dtac intD 1,
rewrite_goals_tac intensional_rews,
etac sym 1 ]);
qed_goal "not_symW" Intensional.thy "s .~= t ==> t .~= s"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1, dtac intD 1,
rewrite_goals_tac intensional_rews,
etac not_sym 1 ]);
qed_goal "transW" Intensional.thy
"[| r .= s; s .= t |] ==> r .= t"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1, REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
etac trans 1,
atac 1 ]);
qed_goal "box_equalsW" Intensional.thy
"[| a .= b; a .= c; b .= d |] ==> c .= d"
(fn prems => [ (rtac transW 1),
(rtac transW 1),
(rtac symW 1),
(REPEAT (resolve_tac prems 1)) ]);
qed_goal "fun_congW" Intensional.thy
"(f::('a => 'b)) = g ==> f[x] .= g[x]"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
rewrite_goals_tac intensional_rews,
etac fun_cong 1 ]);
qed_goal "fun_cong2W" Intensional.thy
"(f::(['a,'b] => 'c)) = g ==> f[x,y] .= g[x,y]"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
rewrite_goals_tac intensional_rews,
asm_full_simp_tac HOL_ss 1 ]);
qed_goal "fun_cong3W" Intensional.thy
"(f::(['a,'b,'c] => 'd)) = g ==> f[x,y,z] .= g[x,y,z]"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
rewrite_goals_tac intensional_rews,
asm_full_simp_tac HOL_ss 1 ]);
qed_goal "arg_congW" Intensional.thy "x .= y ==> (f::'a=>'b)[x] .= f[y]"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
etac arg_cong 1 ]);
qed_goal "arg_cong2W" Intensional.thy
"[| u .= v; x .= y |] ==> (f::['a,'b]=>'c)[u,x] .= f[v,y]"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
REPEAT (etac subst 1),
rtac refl 1 ]);
qed_goal "arg_cong3W" Intensional.thy
"[| r .= s; u .= v; x .= y |] ==> (f::['a,'b,'c]=>'d)[r,u,x] .= f[s,v,y]"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
REPEAT (etac subst 1),
rtac refl 1 ]);
qed_goal "congW" Intensional.thy
"[| (f::'a=>'b) = g; x .= y |] ==> f[x] .= g[y]"
(fn prems => [ rtac box_equalsW 1,
rtac reflW 3,
rtac arg_congW 1,
resolve_tac prems 1,
rtac fun_congW 1,
rtac sym 1,
resolve_tac prems 1 ]);
qed_goal "cong2W" Intensional.thy
"[| (f::['a,'b]=>'c) = g; u .= v; x .= y |] ==> f[u,x] .= g[v,y]"
(fn prems => [ rtac box_equalsW 1,
rtac reflW 3,
rtac arg_cong2W 1,
REPEAT (resolve_tac prems 1),
rtac fun_cong2W 1,
rtac sym 1,
resolve_tac prems 1 ]);
qed_goal "cong3W" Intensional.thy
"[| (f::['a,'b,'c]=>'d) = g; r .= s; u .= v; x .= y |] ==> (f[r,u,x]) .= (g[s,v,y])"
(fn prems => [ rtac box_equalsW 1,
rtac reflW 3,
rtac arg_cong3W 1,
REPEAT (resolve_tac prems 1),
rtac fun_cong3W 1,
rtac sym 1,
resolve_tac prems 1 ]);
(** Lifted equivalence **)
(* Note the object-level implication in the hypothesis. Meta-level implication
would not be correct! *)
qed_goal "iffIW" Intensional.thy
"[| A .-> B; B .-> A |] ==> A .= B"
(fn prems => [ cut_facts_tac prems 1,
rtac intI 1,
REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
(fast_tac prop_cs 1) ]);
qed_goal "iffD2W" Intensional.thy
"[| (P::('w::world) form) .= Q; w |= Q |] ==> w |= P"
(fn prems =>
[cut_facts_tac prems 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
fast_tac prop_cs 1 ]);
val iffD1W = symW RS iffD2W;
(** #True **)
qed_goal "TrueIW" Intensional.thy "#True"
(fn _ => [rtac intI 1, rewrite_goals_tac intensional_rews, rtac TrueI 1]);
qed_goal "eqTrueIW" Intensional.thy "(P::('w::world) form) ==> P .= #True"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
asm_full_simp_tac HOL_ss 1] );
qed_goal "eqTrueEW" Intensional.thy "P .= #True ==> (P::('w::world) form)"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
asm_full_simp_tac HOL_ss 1] );
(** #False **)
qed_goal "FalseEW" Intensional.thy "#False ==> P::('w::world) form"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
etac FalseE 1]);
qed_goal "False_neq_TrueW" Intensional.thy
"(#False::('w::world) form) .= #True ==> P::('w::world) form"
(fn [prem] => [rtac (prem RS eqTrueEW RS FalseEW) 1]);
(** Negation **)
(* Again use object-level implication *)
qed_goal "notIW" Intensional.thy "(P .-> #False) ==> .~P"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
fast_tac prop_cs 1]);
qed_goal "notEWV" Intensional.thy
"[| .~P; P::('w::world) form |] ==> R::('w::world) form"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
etac notE 1, atac 1]);
(* The following rule is stronger: It is enough to detect an
inconsistency at *some* world to conclude R. Note also that P and R
are allowed to be (intensional) formulas of different types! *)
qed_goal "notEW" Intensional.thy
"[| w |= .~P; w |= P |] ==> R::('w::world) form"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
rewrite_goals_tac intensional_rews,
etac notE 1, atac 1]);
(** Implication **)
qed_goal "impIW" Intensional.thy "(!!w. (w |= A) ==> (w |= B)) ==> A .-> B"
(fn [prem] => [ rtac intI 1,
rewrite_goals_tac intensional_rews,
rtac impI 1,
etac prem 1 ]);
qed_goal "mpW" Intensional.thy "[| A .-> B; w |= A |] ==> w |= B"
(fn prems => [ cut_facts_tac prems 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
etac mp 1,
atac 1 ]);
qed_goal "impEW" Intensional.thy
"[| A .-> B; w |= A; w |= B ==> w |= C |] ==> w |= (C::('w::world) form)"
(fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
qed_goal "rev_mpW" Intensional.thy "[| w |= P; P .-> Q |] ==> w |= Q"
(fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
qed_goal "contraposW" Intensional.thy "[| w |= .~Q; P .-> Q |] ==> w |= .~P"
(fn [major,minor] => [rewrite_goals_tac intensional_rews,
rtac contrapos 1,
rtac (rewrite_rule intensional_rews major) 1,
etac rev_mpW 1,
rtac minor 1]);
qed_goal "iffEW" Intensional.thy
"[| (P::('w::world) form) .= Q; [| P .-> Q; Q .-> P |] ==> R::('w::world) form |] ==> R"
(fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2W, p1 RS iffD1W, p2, impIW])1)]);
(** Conjunction **)
qed_goal "conjIW" Intensional.thy "[| w |= P; w |= Q |] ==> w |= P .& Q"
(fn prems => [rewrite_goals_tac intensional_rews,
REPEAT (resolve_tac ([conjI]@prems) 1)]);
qed_goal "conjunct1W" Intensional.thy "(w |= P .& Q) ==> w |= P"
(fn prems => [cut_facts_tac prems 1,
rewrite_goals_tac intensional_rews,
etac conjunct1 1]);
qed_goal "conjunct2W" Intensional.thy "(w |= P .& Q) ==> w |= Q"
(fn prems => [cut_facts_tac prems 1,
rewrite_goals_tac intensional_rews,
etac conjunct2 1]);
qed_goal "conjEW" Intensional.thy
"[| w |= P .& Q; [| w |= P; w |= Q |] ==> w |= R |] ==> w |= (R::('w::world) form)"
(fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
etac conjunct1W 1, etac conjunct2W 1]);
(** Disjunction **)
qed_goal "disjI1W" Intensional.thy "w |= P ==> w |= P .| Q"
(fn [prem] => [rewrite_goals_tac intensional_rews,
rtac disjI1 1,
rtac prem 1]);
qed_goal "disjI2W" Intensional.thy "w |= Q ==> w |= P .| Q"
(fn [prem] => [rewrite_goals_tac intensional_rews,
rtac disjI2 1,
rtac prem 1]);
qed_goal "disjEW" Intensional.thy
"[| w |= P .| Q; P .-> R; Q .-> R |] ==> w |= R"
(fn prems => [cut_facts_tac prems 1,
REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
fast_tac prop_cs 1]);
(** Classical propositional logic **)
qed_goal "classicalW" Intensional.thy "(.~P .-> P) ==> P::('w::world)form"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
fast_tac prop_cs 1]);
qed_goal "notnotDW" Intensional.thy ".~.~P ==> P::('w::world) form"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
etac notnotD 1]);
qed_goal "disjCIW" Intensional.thy "(w |= .~Q .-> P) ==> (w |= P.|Q)"
(fn prems => [cut_facts_tac prems 1,
rewrite_goals_tac intensional_rews,
fast_tac prop_cs 1]);
qed_goal "impCEW" Intensional.thy
"[| P.->Q; (w |= .~P) ==> (w |= R); (w |= Q) ==> (w |= R) |] ==> w |= (R::('w::world) form)"
(fn [a1,a2,a3] =>
[rtac (excluded_middle RS disjE) 1,
etac (rewrite_rule intensional_rews a2) 1,
rtac a3 1,
etac (a1 RS mpW) 1]);
(* The following generates too many parse trees...
qed_goal "iffCEW" Intensional.thy
"[| P .= Q; \
\ [| (w |= P); (w |= Q) |] ==> (w |= R); \
\ [| (w |= .~P); (w |= .~Q) |] ==> (w |= R) \
\ |] ==> w |= (R::('w::world) form)"
*)
qed_goal "case_split_thmW" Intensional.thy
"[| P .-> Q; .~P .-> Q |] ==> Q::('w::world) form"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
REPEAT (dtac intD 1),
rewrite_goals_tac intensional_rews,
fast_tac prop_cs 1]);
fun case_tacW a = res_inst_tac [("P",a)] case_split_thmW;
(** Rigid quantifiers **)
qed_goal "allIW" Intensional.thy "(!!x. P(x)) ==> RALL x. P(x)"
(fn [prem] => [rtac intI 1,
rewrite_goals_tac intensional_rews,
rtac allI 1,
rtac (prem RS intE) 1]);
qed_goal "specW" Intensional.thy "(RALL x. P(x)) ==> P(x)"
(fn prems => [cut_facts_tac prems 1,
rtac intI 1,
dtac intD 1,
rewrite_goals_tac intensional_rews,
etac spec 1]);
qed_goal "allEW" Intensional.thy
"[| RALL x. P(x); P(x) ==> R |] ==> R::('w::world) form"
(fn major::prems=>
[ (REPEAT (resolve_tac (prems @ [major RS specW]) 1)) ]);
qed_goal "all_dupEW" Intensional.thy
"[| RALL x. P(x); [| P(x); RALL x. P(x) |] ==> R |] ==> R::('w::world) form"
(fn prems =>
[ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]);
qed_goal "exIW" Intensional.thy "P(x) ==> REX x. P(x)"
(fn [prem] => [rtac intI 1,
rewrite_goals_tac intensional_rews,
rtac exI 1,
rtac (prem RS intD) 1]);
qed_goal "exEW" Intensional.thy
"[| w |= REX x. P(x); !!x. P(x) .-> Q |] ==> w |= Q"
(fn [major,minor] => [rtac exE 1,
rtac (rewrite_rule intensional_rews major) 1,
etac rev_mpW 1,
rtac minor 1]);
(** Classical quantifier reasoning **)
qed_goal "exCIW" Intensional.thy
"(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x. P(x)"
(fn prems => [cut_facts_tac prems 1,
rewrite_goals_tac intensional_rews,
fast_tac HOL_cs 1]);