src/HOL/TLA/IntLemmas.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:	 IntLemmas.ML
     3     Author:      Stephan Merz
     4     Copyright:   1998 University of Munich
     5 
     6 Lemmas and tactics for "intensional" logics. 
     7 
     8 Mostly a lifting of standard HOL lemmas. They are not required in standard
     9 reasoning about intensional logics, which starts by unlifting proof goals
    10 to the HOL level.
    11 *)
    12 
    13 
    14 qed_goal "substW" Intensional.thy
    15   "[| |- x = y; w |= P(x) |] ==> w |= P(y)"
    16   (fn [prem1,prem2] => [rtac (rewrite_rule ([prem1] RL [inteq_reflection]) prem2) 1]);
    17                         
    18 
    19 (* Lift HOL rules to intensional reasoning *)
    20 
    21 qed_goal "reflW" Intensional.thy "|- x = x"
    22   (fn _ => [Simp_tac 1]);
    23 
    24 qed_goal "symW" Intensional.thy "|- s = t  ==>  |- t = s"
    25   (fn prems => [ cut_facts_tac prems 1,
    26                  rtac intI 1, dtac intD 1,
    27                  rewrite_goals_tac intensional_rews,
    28                  etac sym 1 ]);
    29 
    30 qed_goal "not_symW" Intensional.thy "|- s ~= t  ==>  |- t ~= s"
    31   (fn prems => [ cut_facts_tac prems 1,
    32                  rtac intI 1, dtac intD 1,
    33                  rewrite_goals_tac intensional_rews,
    34                  etac not_sym 1 ]);
    35 
    36 qed_goal "transW" Intensional.thy 
    37   "[| |- r = s; |- s = t |] ==> |- r = t"
    38   (fn prems => [ cut_facts_tac prems 1,
    39                  rtac intI 1, REPEAT (dtac intD 1),
    40                  rewrite_goals_tac intensional_rews,
    41                  etac trans 1,
    42                  atac 1 ]);
    43 
    44 qed_goal "box_equalsW" Intensional.thy 
    45    "[| |- a = b; |- a = c; |- b = d |] ==> |- c = d"
    46    (fn prems => [ (rtac transW 1),
    47                   (rtac transW 1),
    48                   (rtac symW 1),
    49                   (REPEAT (resolve_tac prems 1)) ]);
    50 
    51 
    52 (* NB: Antecedent is a standard HOL (non-intensional) formula. *)
    53 qed_goal "fun_congW" Intensional.thy 
    54    "f = g ==> |- f<x> = g<x>"
    55    (fn prems => [ cut_facts_tac prems 1,
    56                   rtac intI 1,
    57                   rewrite_goals_tac intensional_rews,
    58                   etac fun_cong 1 ]);
    59 
    60 qed_goal "fun_cong2W" Intensional.thy 
    61    "f = g ==> |- f<x,y> = g<x,y>"
    62    (fn prems => [ cut_facts_tac prems 1,
    63                   rtac intI 1,
    64                   Asm_full_simp_tac 1 ]);
    65 
    66 qed_goal "fun_cong3W" Intensional.thy 
    67    "f = g ==> |- f<x,y,z> = g<x,y,z>"
    68    (fn prems => [ cut_facts_tac prems 1,
    69                   rtac intI 1,
    70                   Asm_full_simp_tac 1 ]);
    71 
    72 
    73 qed_goal "arg_congW" Intensional.thy "|- x = y ==> |- f<x> = f<y>"
    74    (fn prems => [ cut_facts_tac prems 1,
    75                   rtac intI 1,
    76                   dtac intD 1,
    77                   rewrite_goals_tac intensional_rews,
    78                   etac arg_cong 1 ]);
    79 
    80 qed_goal "arg_cong2W" Intensional.thy 
    81    "[| |- u = v; |- x = y |] ==> |- f<u,x> = f<v,y>"
    82    (fn prems => [ cut_facts_tac prems 1,
    83                   rtac intI 1,
    84                   REPEAT (dtac intD 1),
    85                   rewrite_goals_tac intensional_rews,
    86                   REPEAT (etac subst 1),
    87                   rtac refl 1 ]);
    88 
    89 qed_goal "arg_cong3W" Intensional.thy 
    90    "[| |- r = s; |- u = v; |- x = y |] ==> |- f<r,u,x> = f<s,v,y>"
    91    (fn prems => [ cut_facts_tac prems 1,
    92                   rtac intI 1,
    93                   REPEAT (dtac intD 1),
    94                   rewrite_goals_tac intensional_rews,
    95                   REPEAT (etac subst 1),
    96                   rtac refl 1 ]);
    97 
    98 qed_goal "congW" Intensional.thy 
    99    "[| f = g; |- x = y |] ==> |- f<x> = g<y>"
   100    (fn prems => [ rtac box_equalsW 1,
   101                   rtac reflW 3,
   102                   rtac arg_congW 1,
   103                   resolve_tac prems 1,
   104                   rtac fun_congW 1,
   105                   rtac sym 1,
   106                   resolve_tac prems 1 ]);
   107 
   108 qed_goal "cong2W" Intensional.thy 
   109    "[| f = g; |- u = v; |- x = y |] ==> |- f<u,x> = g<v,y>"
   110    (fn prems => [ rtac box_equalsW 1,
   111                   rtac reflW 3,
   112                   rtac arg_cong2W 1,
   113                   REPEAT (resolve_tac prems 1),
   114                   rtac fun_cong2W 1,
   115                   rtac sym 1,
   116                   resolve_tac prems 1 ]);
   117 
   118 qed_goal "cong3W" Intensional.thy 
   119    "[| f = g; |- r = s; |- u = v; |- x = y |] ==> |- f<r,u,x> = g<s,v,y>"
   120    (fn prems => [ rtac box_equalsW 1,
   121                   rtac reflW 3,
   122                   rtac arg_cong3W 1,
   123                   REPEAT (resolve_tac prems 1),
   124                   rtac fun_cong3W 1,
   125                   rtac sym 1,
   126                   resolve_tac prems 1 ]);
   127 
   128 
   129 (** Lifted equivalence **)
   130 
   131 (* Note the object-level implication in the hypothesis. Meta-level implication
   132    would be incorrect! *)
   133 qed_goal "iffIW" Intensional.thy 
   134   "[| |- A --> B; |- B --> A |] ==> |- A = B"
   135   (fn prems => [ cut_facts_tac prems 1,
   136                  rewrite_goals_tac (Valid_def::intensional_rews),
   137                  Blast_tac 1 ]);
   138 
   139 qed_goal "iffD2W" Intensional.thy 
   140   "[| |- P = Q; w |= Q |] ==> w |= P"
   141  (fn prems => [ cut_facts_tac prems 1,
   142 	        rewrite_goals_tac (Valid_def::intensional_rews),
   143                 Blast_tac 1 ]);
   144 
   145 val iffD1W = symW RS iffD2W;
   146 
   147 (** #True **)
   148 
   149 qed_goal "eqTrueIW" Intensional.thy "|- P ==> |- P = #True"
   150   (fn prems => [cut_facts_tac prems 1,
   151                 rtac intI 1,
   152                 dtac intD 1,
   153 		Asm_full_simp_tac 1]);
   154 
   155 qed_goal "eqTrueEW" Intensional.thy "|- P = #True ==> |- P"
   156   (fn prems => [cut_facts_tac prems 1,
   157                 rtac intI 1,
   158                 dtac intD 1,
   159 		Asm_full_simp_tac 1]);
   160 
   161 (** #False **)
   162 
   163 qed_goal "FalseEW" Intensional.thy "|- #False ==> |- P"
   164   (fn prems => [cut_facts_tac prems 1,
   165                 rtac intI 1,
   166                 dtac intD 1,
   167                 rewrite_goals_tac intensional_rews,
   168                 etac FalseE 1]);
   169 
   170 qed_goal "False_neq_TrueW" Intensional.thy 
   171  "|- #False = #True ==> |- P"
   172  (fn [prem] => [rtac (prem RS eqTrueEW RS FalseEW) 1]);
   173 
   174 
   175 (** Negation **)
   176 
   177 (* Again use object-level implication *)
   178 qed_goal "notIW" Intensional.thy "|- P --> #False ==> |- ~P"
   179   (fn prems => [cut_facts_tac prems 1,
   180 		rewrite_goals_tac (Valid_def::intensional_rews),
   181 		Blast_tac 1]);
   182 
   183 qed_goal "notEWV" Intensional.thy 
   184   "[| |- ~P; |- P |] ==> |- R"
   185   (fn prems => [cut_facts_tac prems 1,
   186 		rtac intI 1,
   187                 REPEAT (dtac intD 1),
   188                 rewrite_goals_tac intensional_rews,
   189                 etac notE 1, atac 1]);
   190 
   191 (* The following rule is stronger: It is enough to detect an 
   192    inconsistency at *some* world to conclude R. Note also that P and R
   193    are allowed to be (intensional) formulas of different types! *)
   194 
   195 qed_goal "notEW" Intensional.thy 
   196    "[| w |= ~P; w |= P |] ==> |- R"
   197   (fn prems => [cut_facts_tac prems 1,
   198                 rtac intI 1,
   199                 rewrite_goals_tac intensional_rews,
   200                 etac notE 1, atac 1]);
   201 
   202 (** Implication **)
   203 
   204 qed_goal "impIW" Intensional.thy "(!!w. (w |= A) ==> (w |= B)) ==> |- A --> B"
   205   (fn [prem] => [ rtac intI 1,
   206                  rewrite_goals_tac intensional_rews,
   207                  rtac impI 1,
   208                  etac prem 1 ]);
   209 
   210 
   211 qed_goal "mpW" Intensional.thy "[| |- A --> B; w |= A |] ==> w |= B"
   212    (fn prems => [ cut_facts_tac prems 1,
   213                   dtac intD 1,
   214                   rewrite_goals_tac intensional_rews,
   215                   etac mp 1,
   216                   atac 1 ]);
   217 
   218 qed_goal "impEW" Intensional.thy 
   219   "[| |- A --> B; w |= A; w |= B ==> w |= C |] ==> w |= C"
   220   (fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
   221 
   222 qed_goal "rev_mpW" Intensional.thy "[| w |= P; |- P --> Q |] ==> w |= Q"
   223   (fn prems => [ (REPEAT (resolve_tac (prems@[mpW]) 1)) ]);
   224 
   225 qed_goalw "contraposW" Intensional.thy intensional_rews
   226   "[| w |= ~Q; |- P --> Q |] ==> w |= ~P"
   227   (fn [major,minor] => [rtac (major RS contrapos) 1,
   228                         etac rev_mpW 1,
   229                         rtac minor 1]);
   230 
   231 qed_goal "iffEW" Intensional.thy
   232     "[| |- P = Q; [| |- P --> Q; |- Q --> P |] ==> R |] ==> R"
   233  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2W, p1 RS iffD1W, p2, impIW])1)]);
   234 
   235 
   236 (** Conjunction **)
   237 
   238 qed_goalw "conjIW" Intensional.thy intensional_rews "[| w |= P; w |= Q |] ==> w |= P & Q"
   239   (fn prems => [REPEAT (resolve_tac ([conjI]@prems) 1)]);
   240 
   241 qed_goal "conjunct1W" Intensional.thy "(w |= P & Q) ==> w |= P"
   242   (fn prems => [cut_facts_tac prems 1,
   243                 rewrite_goals_tac intensional_rews,
   244                 etac conjunct1 1]);
   245 
   246 qed_goal "conjunct2W" Intensional.thy "(w |= P & Q) ==> w |= Q"
   247   (fn prems => [cut_facts_tac prems 1,
   248                 rewrite_goals_tac intensional_rews,
   249                 etac conjunct2 1]);
   250 
   251 qed_goal "conjEW" Intensional.thy 
   252   "[| w |= P & Q; [| w |= P; w |= Q |] ==> w |= R |] ==> w |= R"
   253   (fn prems => [cut_facts_tac prems 1, resolve_tac prems 1,
   254 	        etac conjunct1W 1, etac conjunct2W 1]);
   255 
   256 
   257 (** Disjunction **)
   258 
   259 qed_goalw "disjI1W" Intensional.thy intensional_rews "w |= P ==> w |= P | Q"
   260   (fn [prem] => [REPEAT (resolve_tac [disjI1,prem] 1)]);
   261 
   262 qed_goalw "disjI2W" Intensional.thy intensional_rews "w |= Q ==> w |= P | Q"
   263   (fn [prem] => [REPEAT (resolve_tac [disjI2,prem] 1)]);
   264 
   265 qed_goal "disjEW" Intensional.thy 
   266          "[| w |= P | Q; |- P --> R; |- Q --> R |] ==> w |= R"
   267   (fn prems => [cut_facts_tac prems 1,
   268                 REPEAT (dtac intD 1),
   269                 rewrite_goals_tac intensional_rews,
   270 		Blast_tac 1]);
   271 
   272 (** Classical propositional logic **)
   273 
   274 qed_goalw "classicalW" Intensional.thy (Valid_def::intensional_rews)
   275   "!!P. |- ~P --> P  ==>  |- P"
   276   (fn prems => [Blast_tac 1]);
   277 
   278 qed_goal "notnotDW" Intensional.thy "!!P. |- ~~P  ==>  |- P"
   279   (fn prems => [rtac intI 1,
   280                 dtac intD 1,
   281                 rewrite_goals_tac intensional_rews,
   282                 etac notnotD 1]);
   283 
   284 qed_goal "disjCIW" Intensional.thy "!!P Q. (w |= ~Q --> P) ==> (w |= P|Q)"
   285   (fn prems => [rewrite_goals_tac intensional_rews,
   286                 Blast_tac 1]);
   287 
   288 qed_goal "impCEW" Intensional.thy 
   289    "[| |- P --> Q; (w |= ~P) ==> (w |= R); (w |= Q) ==> (w |= R) |] ==> w |= R"
   290   (fn [a1,a2,a3] => 
   291     [rtac (excluded_middle RS disjE) 1,
   292      etac (rewrite_rule intensional_rews a2) 1,
   293      rtac a3 1,
   294      etac (a1 RS mpW) 1]);
   295 
   296 qed_goalw "iffCEW" Intensional.thy intensional_rews
   297    "[| |- P = Q;      \
   298 \      [| (w |= P); (w |= Q) |] ==> (w |= R);   \
   299 \      [| (w |= ~P); (w |= ~Q) |] ==> (w |= R)  \
   300 \   |] ==> w |= R"
   301    (fn [a1,a2,a3] =>
   302       [rtac iffCE 1,
   303        etac a2 2, atac 2,
   304        etac a3 2, atac 2,
   305        rtac (int_unlift a1) 1]);
   306 
   307 qed_goal "case_split_thmW" Intensional.thy 
   308    "!!P. [| |- P --> Q; |- ~P --> Q |] ==> |- Q"
   309   (fn _ => [rewrite_goals_tac (Valid_def::intensional_rews),
   310 	    Blast_tac 1]);
   311 
   312 fun case_tacW a = res_inst_tac [("P",a)] case_split_thmW;
   313 
   314 
   315 (** Rigid quantifiers **)
   316 
   317 qed_goal "allIW" Intensional.thy "(!!x. |- P x) ==> |- ! x. P(x)"
   318   (fn [prem] => [rtac intI 1,
   319                  rewrite_goals_tac intensional_rews,
   320                  rtac allI 1,
   321                  rtac (prem RS intD) 1]);
   322 
   323 qed_goal "specW" Intensional.thy "|- ! x. P x ==> |- P x"
   324   (fn prems => [cut_facts_tac prems 1,
   325                 rtac intI 1,
   326                 dtac intD 1,
   327                 rewrite_goals_tac intensional_rews,
   328                 etac spec 1]);
   329 
   330 
   331 qed_goal "allEW" Intensional.thy 
   332          "[| |- ! x. P x;  |- P x ==> |- R |] ==> |- R"
   333  (fn major::prems=>
   334   [ (REPEAT (resolve_tac (prems @ [major RS specW]) 1)) ]);
   335 
   336 qed_goal "all_dupEW" Intensional.thy 
   337     "[| |- ! x. P x;  [| |- P x; |- ! x. P x |] ==> |- R |] ==> |- R"
   338  (fn prems =>
   339   [ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]);
   340 
   341 
   342 qed_goal "exIW" Intensional.thy "|- P x ==> |- ? x. P x"
   343   (fn [prem] => [rtac intI 1,
   344                  rewrite_goals_tac intensional_rews,
   345                  rtac exI 1,
   346                  rtac (prem RS intD) 1]);
   347 
   348 qed_goal "exEW" Intensional.thy 
   349   "[| w |= ? x. P x; !!x. |- P x --> Q |] ==> w |= Q"
   350   (fn [major,minor] => [rtac exE 1,
   351                         rtac (rewrite_rule intensional_rews major) 1,
   352                         etac rev_mpW 1,
   353                         rtac minor 1]);
   354 
   355 (** Classical quantifier reasoning **)
   356 
   357 qed_goal "exCIW" Intensional.thy 
   358   "!!P. w |= (! x. ~P x) --> P a ==> w |= ? x. P x"
   359   (fn prems => [rewrite_goals_tac intensional_rews,
   360                 Blast_tac 1]);
   361