wneuper/isa: doc-src/TutorialI/Rules/Basic.thy@20e3616b2d9c

     1 theory Basic imports Main begin

     3 lemma conj_rule: "\<lbrakk> P; Q \<rbrakk> \<Longrightarrow> P \<and> (Q \<and> P)"

     4 apply (rule conjI)

     5  apply assumption

     6 apply (rule conjI)

     7  apply assumption

     8 apply assumption

     9 done

    12 lemma disj_swap: "P | Q \<Longrightarrow> Q | P"

    13 apply (erule disjE)

    14  apply (rule disjI2)

    15  apply assumption

    16 apply (rule disjI1)

    17 apply assumption

    18 done

    20 lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P"

    21 apply (rule conjI)

    22  apply (drule conjunct2)

    23  apply assumption

    24 apply (drule conjunct1)

    25 apply assumption

    26 done

    28 lemma imp_uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"

    29 apply (rule impI)

    30 apply (erule conjE)

    31 apply (drule mp)

    32  apply assumption

    33 apply (drule mp)

    34   apply assumption

    35  apply assumption

    36 done

    38 text {*

    39 by eliminates uses of assumption and done

    40 *}

    42 lemma imp_uncurry': "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"

    43 apply (rule impI)

    44 apply (erule conjE)

    45 apply (drule mp)

    46  apply assumption

    47 by (drule mp)

    50 text {*

    51 substitution

    53 @{thm[display] ssubst}

    54 \rulename{ssubst}

    55 *};

    57 lemma "\<lbrakk> x = f x; P(f x) \<rbrakk> \<Longrightarrow> P x"

    58 by (erule ssubst)

    60 text {*

    61 also provable by simp (re-orients)

    62 *};

    64 text {*

    65 the subst method

    67 @{thm[display] mult_commute}

    68 \rulename{mult_commute}

    70 this would fail:

    71 apply (simp add: mult_commute)

    72 *};

    75 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y"

    76 txt{*

    77 @{subgoals[display,indent=0,margin=65]}

    78 *};

    79 apply (subst mult_commute)

    80 txt{*

    81 @{subgoals[display,indent=0,margin=65]}

    82 *};

    83 oops

    85 (*exercise involving THEN*)

    86 lemma "\<lbrakk>P x y z; Suc x < y\<rbrakk> \<Longrightarrow> f z = x*y"

    87 apply (rule mult_commute [THEN ssubst])

    88 oops

    91 lemma "\<lbrakk>x = f x; triple (f x) (f x) x\<rbrakk> \<Longrightarrow> triple x x x"

    92 apply (erule ssubst)

    93   --{* @{subgoals[display,indent=0,margin=65]} *}

    94 back --{* @{subgoals[display,indent=0,margin=65]} *}

    95 back --{* @{subgoals[display,indent=0,margin=65]} *}

    96 back --{* @{subgoals[display,indent=0,margin=65]} *}

    97 back --{* @{subgoals[display,indent=0,margin=65]} *}

    98 apply assumption

    99 done

   101 lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"

   102 apply (erule ssubst, assumption)

   103 done

   105 text{*

   106 or better still

   107 *}

   109 lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"

   110 by (erule ssubst)

   113 lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"

   114 apply (erule_tac P="\<lambda>u. triple u u x" in ssubst)

   115 apply (assumption)

   116 done

   119 lemma "\<lbrakk> x = f x; triple (f x) (f x) x \<rbrakk> \<Longrightarrow> triple x x x"

   120 by (erule_tac P="\<lambda>u. triple u u x" in ssubst)

   123 text {*

   124 negation

   126 @{thm[display] notI}

   127 \rulename{notI}

   129 @{thm[display] notE}

   130 \rulename{notE}

   132 @{thm[display] classical}

   133 \rulename{classical}

   135 @{thm[display] contrapos_pp}

   136 \rulename{contrapos_pp}

   138 @{thm[display] contrapos_pn}

   139 \rulename{contrapos_pn}

   141 @{thm[display] contrapos_np}

   142 \rulename{contrapos_np}

   144 @{thm[display] contrapos_nn}

   145 \rulename{contrapos_nn}

   146 *};

   149 lemma "\<lbrakk>\<not>(P\<longrightarrow>Q); \<not>(R\<longrightarrow>Q)\<rbrakk> \<Longrightarrow> R"

   150 apply (erule_tac Q="R\<longrightarrow>Q" in contrapos_np)

   151         --{* @{subgoals[display,indent=0,margin=65]} *}

   152 apply (intro impI)

   153         --{* @{subgoals[display,indent=0,margin=65]} *}

   154 by (erule notE)

   156 text {*

   157 @{thm[display] disjCI}

   158 \rulename{disjCI}

   159 *};

   161 lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R"

   162 apply (intro disjCI conjI)

   163         --{* @{subgoals[display,indent=0,margin=65]} *}

   165 apply (elim conjE disjE)

   166  apply assumption

   167         --{* @{subgoals[display,indent=0,margin=65]} *}

   169 by (erule contrapos_np, rule conjI)

   170 text{*

   171 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{6}}\isanewline

   172 \isanewline

   173 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline

   174 {\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R\ {\isasymLongrightarrow}\ P\ {\isasymor}\ Q\ {\isasymand}\ R\isanewline

   175 \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\isanewline

   176 \ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ R

   177 *}

   180 text{*rule_tac, etc.*}

   183 lemma "P&Q"

   184 apply (rule_tac P=P and Q=Q in conjI)

   185 oops

   188 text{*unification failure trace *}

   190 ML "Unsynchronized.set trace_unify_fail"

   192 lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"

   193 txt{*

   194 @{subgoals[display,indent=0,margin=65]}

   195 apply assumption

   196 Clash: e =/= c

   198 Clash: == =/= Trueprop

   199 *}

   200 oops

   202 lemma "\<forall>x y. P(x,y) --> P(y,x)"

   203 apply auto

   204 txt{*

   205 @{subgoals[display,indent=0,margin=65]}

   206 apply assumption

   208 Clash: bound variable x (depth 1) =/= bound variable y (depth 0)

   210 Clash: == =/= Trueprop

   211 Clash: == =/= Trueprop

   212 *}

   213 oops

   215 ML "Unsynchronized.reset trace_unify_fail"

   218 text{*Quantifiers*}

   220 text {*

   221 @{thm[display] allI}

   222 \rulename{allI}

   224 @{thm[display] allE}

   225 \rulename{allE}

   227 @{thm[display] spec}

   228 \rulename{spec}

   229 *};

   231 lemma "\<forall>x. P x \<longrightarrow> P x"

   232 apply (rule allI)

   233 by (rule impI)

   235 lemma "(\<forall>x. P \<longrightarrow> Q x) \<Longrightarrow> P \<longrightarrow> (\<forall>x. Q x)"

   236 apply (rule impI, rule allI)

   237 apply (drule spec)

   238 by (drule mp)

   240 text{*rename_tac*}

   241 lemma "x < y \<Longrightarrow> \<forall>x y. P x (f y)"

   242 apply (intro allI)

   243         --{* @{subgoals[display,indent=0,margin=65]} *}

   244 apply (rename_tac v w)

   245         --{* @{subgoals[display,indent=0,margin=65]} *}

   246 oops

   249 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))"

   250 apply (frule spec)

   251         --{* @{subgoals[display,indent=0,margin=65]} *}

   252 apply (drule mp, assumption)

   253 apply (drule spec)

   254         --{* @{subgoals[display,indent=0,margin=65]} *}

   255 by (drule mp)

   257 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (f x); P a\<rbrakk> \<Longrightarrow> P(f (f a))"

   258 by blast

   261 text{*

   262 the existential quantifier*}

   264 text {*

   265 @{thm[display]"exI"}

   266 \rulename{exI}

   268 @{thm[display]"exE"}

   269 \rulename{exE}

   270 *};

   273 text{*

   274 instantiating quantifiers explicitly by rule_tac and erule_tac*}

   276 lemma "\<lbrakk>\<forall>x. P x \<longrightarrow> P (h x); P a\<rbrakk> \<Longrightarrow> P(h (h a))"

   277 apply (frule spec)

   278         --{* @{subgoals[display,indent=0,margin=65]} *}

   279 apply (drule mp, assumption)

   280         --{* @{subgoals[display,indent=0,margin=65]} *}

   281 apply (drule_tac x = "h a" in spec)

   282         --{* @{subgoals[display,indent=0,margin=65]} *}

   283 by (drule mp)

   285 text {*

   286 @{thm[display]"dvd_def"}

   287 \rulename{dvd_def}

   288 *};

   290 lemma mult_dvd_mono: "\<lbrakk>i dvd m; j dvd n\<rbrakk> \<Longrightarrow> i*j dvd (m*n :: nat)"

   291 apply (simp add: dvd_def)

   292         --{* @{subgoals[display,indent=0,margin=65]} *}

   293 apply (erule exE)

   294         --{* @{subgoals[display,indent=0,margin=65]} *}

   295 apply (erule exE)

   296         --{* @{subgoals[display,indent=0,margin=65]} *}

   297 apply (rename_tac l)

   298         --{* @{subgoals[display,indent=0,margin=65]} *}

   299 apply (rule_tac x="k*l" in exI)

   300         --{* @{subgoals[display,indent=0,margin=65]} *}

   301 apply simp

   302 done

   304 text{*

   305 Hilbert-epsilon theorems*}

   307 text{*

   308 @{thm[display] the_equality[no_vars]}

   309 \rulename{the_equality}

   311 @{thm[display] some_equality[no_vars]}

   312 \rulename{some_equality}

   314 @{thm[display] someI[no_vars]}

   315 \rulename{someI}

   317 @{thm[display] someI2[no_vars]}

   318 \rulename{someI2}

   320 @{thm[display] someI_ex[no_vars]}

   321 \rulename{someI_ex}

   323 needed for examples

   325 @{thm[display] inv_def[no_vars]}

   326 \rulename{inv_def}

   328 @{thm[display] Least_def[no_vars]}

   329 \rulename{Least_def}

   331 @{thm[display] order_antisym[no_vars]}

   332 \rulename{order_antisym}

   333 *}

   336 lemma "inv Suc (Suc n) = n"

   337 by (simp add: inv_def)

   339 text{*but we know nothing about inv Suc 0*}

   341 theorem Least_equality:

   342      "\<lbrakk> P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"

   343 apply (simp add: Least_def)

   345 txt{*

   346 @{subgoals[display,indent=0,margin=65]}

   347 *};

   349 apply (rule the_equality)

   351 txt{*

   352 @{subgoals[display,indent=0,margin=65]}

   354 first subgoal is existence; second is uniqueness

   355 *};

   356 by (auto intro: order_antisym)

   359 theorem axiom_of_choice:

   360      "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"

   361 apply (rule exI, rule allI)

   363 txt{*

   364 @{subgoals[display,indent=0,margin=65]}

   366 state after intro rules

   367 *};

   368 apply (drule spec, erule exE)

   370 txt{*

   371 @{subgoals[display,indent=0,margin=65]}

   373 applying @text{someI} automatically instantiates

   374 @{term f} to @{term "\<lambda>x. SOME y. P x y"}

   375 *};

   377 by (rule someI)

   379 (*both can be done by blast, which however hasn't been introduced yet*)

   380 lemma "[| P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k";

   381 apply (simp add: Least_def LeastM_def)

   382 by (blast intro: some_equality order_antisym);

   384 theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"

   385 apply (rule exI [of _  "\<lambda>x. SOME y. P x y"])

   386 by (blast intro: someI);

   388 text{*end of Epsilon section*}

   391 lemma "(\<exists>x. P x) \<or> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<or> Q x"

   392 apply (elim exE disjE)

   393  apply (intro exI disjI1)

   394  apply assumption

   395 apply (intro exI disjI2)

   396 apply assumption

   397 done

   399 lemma "(P\<longrightarrow>Q) \<or> (Q\<longrightarrow>P)"

   400 apply (intro disjCI impI)

   401 apply (elim notE)

   402 apply (intro impI)

   403 apply assumption

   404 done

   406 lemma "(P\<or>Q)\<and>(P\<or>R) \<Longrightarrow> P \<or> (Q\<and>R)"

   407 apply (intro disjCI conjI)

   408 apply (elim conjE disjE)

   409 apply blast

   410 apply blast

   411 apply blast

   412 apply blast

   413 (*apply elim*)

   414 done

   416 lemma "(\<exists>x. P \<and> Q x) \<Longrightarrow> P \<and> (\<exists>x. Q x)"

   417 apply (erule exE)

   418 apply (erule conjE)

   419 apply (rule conjI)

   420  apply assumption

   421 apply (rule exI)

   422  apply assumption

   423 done

   425 lemma "(\<exists>x. P x) \<and> (\<exists>x. Q x) \<Longrightarrow> \<exists>x. P x \<and> Q x"

   426 apply (erule conjE)

   427 apply (erule exE)

   428 apply (erule exE)

   429 apply (rule exI)

   430 apply (rule conjI)

   431  apply assumption

   432 oops

   434 lemma "\<forall>y. R y y \<Longrightarrow> \<exists>x. \<forall>y. R x y"

   435 apply (rule exI)

   436   --{* @{subgoals[display,indent=0,margin=65]} *}

   437 apply (rule allI)

   438   --{* @{subgoals[display,indent=0,margin=65]} *}

   439 apply (drule spec)

   440   --{* @{subgoals[display,indent=0,margin=65]} *}

   441 oops

   443 lemma "\<forall>x. \<exists>y. x=y"

   444 apply (rule allI)

   445 apply (rule exI)

   446 apply (rule refl)

   447 done

   449 lemma "\<exists>x. \<forall>y. x=y"

   450 apply (rule exI)

   451 apply (rule allI)

   452 oops

   454 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 32962	69916a850301
child 39065	89f273ab1d42
permissions	-rw-r--r--