src/HOL/TLA/IntLemmas.ML

 (* 
     File:	 IntLemmas.ML
     Author:      Stephan Merz
-    Copyright:   1997 University of Munich
+    Copyright:   1998 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)"
+  "[| |- x = y; w |= P(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"
+qed_goal "reflW" Intensional.thy "|- x = x"
+  (fn _ => [Simp_tac 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"
+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"
+  "[| |- 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"
+   "[| |- a = b; |- a = c; |- b = d |] ==> |- c = d"
    (fn prems => [ (rtac transW 1),
                   (rtac transW 1),
                   (rtac symW 1),
                   (REPEAT (resolve_tac prems 1)) ]);
 
 
+(* NB: Antecedent is a standard HOL (non-intensional) formula. *)
 qed_goal "fun_congW" Intensional.thy 
-   "(f::('a => 'b)) = g ==> f[x] .= g[x]"
+   "f = 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 ]);
+   "f = g ==> |- f<x,y> = g<x,y>"
+   (fn prems => [ cut_facts_tac prems 1,
+                  rtac intI 1,
+                  Asm_full_simp_tac 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]"
+   "f = g ==> |- f<x,y,z> = g<x,y,z>"
+   (fn prems => [ cut_facts_tac prems 1,
+                  rtac intI 1,
+                  Asm_full_simp_tac 1 ]);
+
+
+qed_goal "arg_congW" Intensional.thy "|- x = y ==> |- f<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]"
+   "[| |- u = v; |- x = y |] ==> |- f<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]"
+   "[| |- r = s; |- u = v; |- x = y |] ==> |- f<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]"
+   "[| f = 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]"
+   "[| f = 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])"
+   "[| f = 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,

 
 
 (** Lifted equivalence **)
 
 (* Note the object-level implication in the hypothesis. Meta-level implication
-   would not be correct! *)
+   would be incorrect! *)
 qed_goal "iffIW" Intensional.thy 
-  "[| A .-> B; B .-> A |] ==> A .= B"
+  "[| |- 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) ]);
+                 rewrite_goals_tac (Valid_def::intensional_rews),
+                 Blast_tac 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 ]);
+  "[| |- P = Q; w |= Q |] ==> w |= P"
+ (fn prems => [ cut_facts_tac prems 1,
+	        rewrite_goals_tac (Valid_def::intensional_rews),
+                Blast_tac 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] );
+qed_goal "eqTrueIW" Intensional.thy "|- P ==> |- P = #True"
+  (fn prems => [cut_facts_tac prems 1,
+                rtac intI 1,
+                dtac intD 1,
+		Asm_full_simp_tac 1]);
+
+qed_goal "eqTrueEW" Intensional.thy "|- P = #True ==> |- P"
+  (fn prems => [cut_facts_tac prems 1,
+                rtac intI 1,
+                dtac intD 1,
+		Asm_full_simp_tac 1]);
 
 (** #False **)
 
-qed_goal "FalseEW" Intensional.thy "#False ==> P::('w::world) form"
+qed_goal "FalseEW" Intensional.thy "|- #False ==> |- P"
   (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"
+ "|- #False = #True ==> |- P"
  (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 "notIW" Intensional.thy "|- P --> #False ==> |- ~P"
+  (fn prems => [cut_facts_tac prems 1,
+		rewrite_goals_tac (Valid_def::intensional_rews),
+		Blast_tac 1]);
 
 qed_goal "notEWV" Intensional.thy 
-  "[| .~P; P::('w::world) form |] ==> R::('w::world) form"
+  "[| |- ~P; |- P |] ==> |- R"
   (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"
+   "[| w |= ~P; w |= P |] ==> |- R"
   (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"
+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"
+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)"
+  "[| |- A --> B; w |= A; w |= B ==> w |= C |] ==> w |= C"
   (fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
 
-qed_goal "rev_mpW" Intensional.thy "[| w |= P; P .-> Q |] ==> w |= Q"
+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,
+qed_goalw "contraposW" Intensional.thy intensional_rews
+  "[| w |= ~Q; |- P --> Q |] ==> w |= ~P"
+  (fn [major,minor] => [rtac (major RS contrapos) 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"
+    "[| |- P = Q; [| |- P --> Q; |- Q --> P |] ==> R |] ==> 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"
+qed_goalw "conjIW" Intensional.thy intensional_rews "[| w |= P; w |= Q |] ==> w |= P & Q"
+  (fn prems => [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"
+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)"
+  "[| w |= P & Q; [| w |= P; w |= Q |] ==> w |= R |] ==> w |= R"
   (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_goalw "disjI1W" Intensional.thy intensional_rews "w |= P ==> w |= P | Q"
+  (fn [prem] => [REPEAT (resolve_tac [disjI1,prem] 1)]);
+
+qed_goalw "disjI2W" Intensional.thy intensional_rews "w |= Q ==> w |= P | Q"
+  (fn [prem] => [REPEAT (resolve_tac [disjI2,prem] 1)]);
 
 qed_goal "disjEW" Intensional.thy 
-         "[| w |= P .| Q; P .-> R; Q .-> R |] ==> w |= R"
+         "[| 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]);
+		Blast_tac 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,
+qed_goalw "classicalW" Intensional.thy (Valid_def::intensional_rews)
+  "!!P. |- ~P --> P  ==>  |- P"
+  (fn prems => [Blast_tac 1]);
+
+qed_goal "notnotDW" Intensional.thy "!!P. |- ~~P  ==>  |- P"
+  (fn prems => [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 "disjCIW" Intensional.thy "!!P Q. (w |= ~Q --> P) ==> (w |= P|Q)"
+  (fn prems => [rewrite_goals_tac intensional_rews,
+                Blast_tac 1]);
 
 qed_goal "impCEW" Intensional.thy 
-   "[| P.->Q; (w |= .~P) ==> (w |= R); (w |= Q) ==> (w |= R) |] ==> w |= (R::('w::world) form)"
+   "[| |- P --> Q; (w |= ~P) ==> (w |= R); (w |= Q) ==> (w |= R) |] ==> w |= R"
   (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;      \
+qed_goalw "iffCEW" Intensional.thy intensional_rews
+   "[| |- P = Q;      \
 \      [| (w |= P); (w |= Q) |] ==> (w |= R);   \
-\      [| (w |= .~P); (w |= .~Q) |] ==> (w |= R)  \
-\   |] ==> w |= (R::('w::world) form)"
-
-*)
+\      [| (w |= ~P); (w |= ~Q) |] ==> (w |= R)  \
+\   |] ==> w |= R"
+   (fn [a1,a2,a3] =>
+      [rtac iffCE 1,
+       etac a2 2, atac 2,
+       etac a3 2, atac 2,
+       rtac (int_unlift a1) 1]);
 
 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]);
+   "!!P. [| |- P --> Q; |- ~P --> Q |] ==> |- Q"
+  (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews),
+	    Blast_tac 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)"
+qed_goal "allIW" Intensional.thy "(!!x. |- P x) ==> |- ! 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)"
+                 rtac (prem RS intD) 1]);
+
+qed_goal "specW" Intensional.thy "|- ! 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"
+         "[| |- ! x. P x;  |- P x ==> |- R |] ==> |- R"
  (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"
+    "[| |- ! x. P x;  [| |- P x; |- ! x. P x |] ==> |- R |] ==> |- R"
  (fn prems =>
   [ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]);
 
 
-qed_goal "exIW" Intensional.thy "P(x) ==> REX x. P(x)"
+qed_goal "exIW" Intensional.thy "|- P x ==> |- ? 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"
+  "[| w |= ? 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]);
-
+  "!!P. w |= (! x. ~P x) --> P a ==> w |= ? x. P x"
+  (fn prems => [rewrite_goals_tac intensional_rews,
+                Blast_tac 1]);
+