Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Basic.thy Sprache: Isabelle

Original von: Isabelle^©

theory Basic imports Main begin

lemma conj_rule: "\ P; Q \ \ P \ (Q \ P)"
apply (rule conjI)
apply assumption
apply (rule conjI)
apply assumption
apply assumption
done


lemma disj_swap: "P | Q \ Q | P"
apply (erule disjE)
apply (rule disjI2)
apply assumption
apply (rule disjI1)
apply assumption
done

lemma conj_swap: "P \ Q \ Q \ P"
apply (rule conjI)
apply (drule conjunct2)
apply assumption
apply (drule conjunct1)
apply assumption
done

lemma imp_uncurry: "P \ Q \ R \ P \ Q \ R"
apply (rule impI)
apply (erule conjE)
apply (drule mp)
apply assumption
apply (drule mp)
  apply assumption
apply assumption
done

text \<open>
by eliminates uses of assumption and done
\<close>

lemma imp_uncurry': "P \ Q \ R \ P \ Q \ R"
apply (rule impI)
apply (erule conjE)
apply (drule mp)
apply assumption
by (drule mp)

text \<open>
substitution

@{thm[display] ssubst}
\rulename{ssubst}
\<close>

lemma "\ x = f x; P(f x) \ \ P x"
by (erule ssubst)

text \<open>
also provable by simp (re-orients)
\<close>

text \<open>
the subst method

@{thm[display] mult.commute}
\rulename{mult.commute}

this would fail:
apply (simp add: mult.commute)
\<close>

lemma "\P x y z; Suc x < y\ \ f z = x*y"
txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>
apply (subst mult.commute)
txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>
oops

(*exercise involving THEN*)
lemma "\P x y z; Suc x < y\ \ f z = x*y"
apply (rule mult.commute [THEN ssubst])
oops

lemma "\x = f x; triple (f x) (f x) x\ \ triple x x x"
apply (erule ssubst)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
back \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
back \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
back \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
back \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
done

lemma "\ x = f x; triple (f x) (f x) x \ \ triple x x x"
apply (erule ssubst, assumption)
done

text\<open>
or better still
\<close>

lemma "\ x = f x; triple (f x) (f x) x \ \ triple x x x"
by (erule ssubst)

lemma "\ x = f x; triple (f x) (f x) x \ \ triple x x x"
apply (erule_tac P="\u. triple u u x" in ssubst)
apply (assumption)
done

lemma "\ x = f x; triple (f x) (f x) x \ \ triple x x x"
by (erule_tac P="\u. triple u u x" in ssubst)

text \<open>
negation

@{thm[display] notI}
\rulename{notI}

@{thm[display] notE}
\rulename{notE}

@{thm[display] classical}
\rulename{classical}

@{thm[display] contrapos_pp}
\rulename{contrapos_pp}

@{thm[display] contrapos_pn}
\rulename{contrapos_pn}

@{thm[display] contrapos_np}
\rulename{contrapos_np}

@{thm[display] contrapos_nn}
\rulename{contrapos_nn}
\<close>

lemma "\\(P\Q); \(R\Q)\ \ R"
apply (erule_tac Q="R\Q" in contrapos_np)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (intro impI)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
by (erule notE)

text \<open>
@{thm[display] disjCI}
\rulename{disjCI}
\<close>

lemma "(P \ Q) \ R \ P \ Q \ R"
apply (intro disjCI conjI)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>

apply (elim conjE disjE)
apply assumption
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>

by (erule contrapos_np, rule conjI)
text\<open>
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{6}}\isanewline
\isanewline
goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
{\isacharparenleft}P\ {\isasymor}\ Q{\isacharparenright}\ {\isasymand}\ R\ {\isasymLongrightarrow}\ P\ {\isasymor}\ Q\ {\isasymand}\ R\isanewline
\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ Q\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}R{\isacharsemicolon}\ Q{\isacharsemicolon}\ {\isasymnot}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ R
\<close>

text\<open>rule_tac, etc.\<close>

lemma "P&Q"
apply (rule_tac P=P and Q=Q in conjI)
oops

text\<open>unification failure trace\<close>

declare [[unify_trace_failure = true]]

lemma "P(a, f(b, g(e,a), b), a) \ P(a, f(b, g(c,a), b), a)"
txt\<open>
@{subgoals[display,indent=0,margin=65]}
apply assumption
Clash: e =/= c

Clash: == =/= Trueprop
\<close>
oops

lemma "\x y. P(x,y) --> P(y,x)"
apply auto
txt\<open>
@{subgoals[display,indent=0,margin=65]}
apply assumption

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

Clash: == =/= Trueprop
Clash: == =/= Trueprop
\<close>
oops

declare [[unify_trace_failure = false]]

text\<open>Quantifiers\<close>

text \<open>
@{thm[display] allI}
\rulename{allI}

@{thm[display] allE}
\rulename{allE}

@{thm[display] spec}
\rulename{spec}
\<close>

lemma "\x. P x \ P x"
apply (rule allI)
by (rule impI)

lemma "(\x. P \ Q x) \ P \ (\x. Q x)"
apply (rule impI, rule allI)
apply (drule spec)
by (drule mp)

text\<open>rename_tac\<close>
lemma "x < y \ \x y. P x (f y)"
apply (intro allI)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rename_tac v w)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
oops

lemma "\\x. P x \ P (h x); P a\ \ P(h (h a))"
apply (frule spec)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (drule mp, assumption)
apply (drule spec)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
by (drule mp)

lemma "\\x. P x \ P (f x); P a\ \ P(f (f a))"
by blast

text\<open>
the existential quantifier\<close>

text \<open>
@{thm[display]"exI"}
\rulename{exI}

@{thm[display]"exE"}
\rulename{exE}
\<close>

text\<open>
instantiating quantifiers explicitly by rule_tac and erule_tac\<close>

lemma "\\x. P x \ P (h x); P a\ \ P(h (h a))"
apply (frule spec)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (drule mp, assumption)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (drule_tac x = "h a" in spec)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
by (drule mp)

text \<open>
@{thm[display]"dvd_def"}
\rulename{dvd_def}
\<close>

lemma mult_dvd_mono: "\i dvd m; j dvd n\ \ i*j dvd (m*n :: nat)"
apply (simp add: dvd_def)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule exE)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule exE)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rename_tac l)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule_tac x="k*l" in exI)
        \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply simp
done

text\<open>
Hilbert-epsilon theorems\<close>

text\<open>
@{thm[display] the_equality[no_vars]}
\rulename{the_equality}

@{thm[display] some_equality[no_vars]}
\rulename{some_equality}

@{thm[display] someI[no_vars]}
\rulename{someI}

@{thm[display] someI2[no_vars]}
\rulename{someI2}

@{thm[display] someI_ex[no_vars]}
\rulename{someI_ex}

needed for examples

@{thm[display] inv_def[no_vars]}
\rulename{inv_def}

@{thm[display] Least_def[no_vars]}
\rulename{Least_def}

@{thm[display] order_antisym[no_vars]}
\rulename{order_antisym}
\<close>

lemma "inv Suc (Suc n) = n"
by (simp add: inv_def)

text\<open>but we know nothing about inv Suc 0\<close>

theorem Least_equality:
     "\ P (k::nat); \x. P x \ k \ x \ \ (LEAST x. P(x)) = k"
apply (simp add: Least_def)

txt\<open>
@{subgoals[display,indent=0,margin=65]}
\<close>

apply (rule the_equality)

txt\<open>
@{subgoals[display,indent=0,margin=65]}

first subgoal is existence; second is uniqueness
\<close>
by (auto intro: order_antisym)

theorem axiom_of_choice:
     "(\x. \y. P x y) \ \f. \x. P x (f x)"
apply (rule exI, rule allI)

txt\<open>
@{subgoals[display,indent=0,margin=65]}

state after intro rules
\<close>
apply (drule spec, erule exE)

txt\<open>
@{subgoals[display,indent=0,margin=65]}

applying @text{someI} automatically instantiates
\<^term>\<open>f\<close> to \<^term>\<open>\<lambda>x. SOME y. P x y\<close>
\<close>

by (rule someI)

(*both can be done by blast, which however hasn't been introduced yet*)
lemma "[| P (k::nat); \x. P x \ k \ x |] ==> (LEAST x. P(x)) = k"
apply (simp add: Least_def)
by (blast intro: order_antisym)

theorem axiom_of_choice': "(\x. \y. P x y) \ \f. \x. P x (f x)"
apply (rule exI [of _  "\x. SOME y. P x y"])
by (blast intro: someI)

text\<open>end of Epsilon section\<close>

lemma "(\x. P x) \ (\x. Q x) \ \x. P x \ Q x"
apply (elim exE disjE)
apply (intro exI disjI1)
apply assumption
apply (intro exI disjI2)
apply assumption
done

lemma "(P\Q) \ (Q\P)"
apply (intro disjCI impI)
apply (elim notE)
apply (intro impI)
apply assumption
done

lemma "(P\Q)\(P\R) \ P \ (Q\R)"
apply (intro disjCI conjI)
apply (elim conjE disjE)
apply blast
apply blast
apply blast
apply blast
(*apply elim*)
done

lemma "(\x. P \ Q x) \ P \ (\x. Q x)"
apply (erule exE)
apply (erule conjE)
apply (rule conjI)
apply assumption
apply (rule exI)
apply assumption
done

lemma "(\x. P x) \ (\x. Q x) \ \x. P x \ Q x"
apply (erule conjE)
apply (erule exE)
apply (erule exE)
apply (rule exI)
apply (rule conjI)
apply assumption
oops

lemma "\y. R y y \ \x. \y. R x y"
apply (rule exI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule allI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (drule spec)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
oops

lemma "\x. \y. x=y"
apply (rule allI)
apply (rule exI)
apply (rule refl)
done

lemma "\x. \y. x=y"
apply (rule exI)
apply (rule allI)
oops

end

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.