doc-src/TutorialI/Overview/LNCS/Rules.thy
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 13489 79d117a158bd
child 21324 a5089fc012b5
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*<*)theory Rules = Main:(*>*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     2
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     3
section{*The Rules of the Game*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     4
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     5
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     6
subsection{*Introduction Rules*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     7
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     8
text{* Introduction rules for propositional logic:
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
     9
\begin{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    10
\begin{tabular}{ll}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    11
@{thm[source]impI} & @{thm impI[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    12
@{thm[source]conjI} & @{thm conjI[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    13
@{thm[source]disjI1} & @{thm disjI1[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    14
@{thm[source]disjI2} & @{thm disjI2[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    15
@{thm[source]iffI} & @{thm iffI[no_vars]}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    16
\end{tabular}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    17
\end{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    18
*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    19
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    20
(*<*)thm impI conjI disjI1 disjI2 iffI(*>*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    21
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    22
lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    23
apply(rule impI)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    24
apply(rule conjI)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    25
 apply assumption
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    26
apply(rule conjI)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    27
 apply assumption
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    28
apply assumption
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    29
done
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    30
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    31
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    32
subsection{*Elimination Rules*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    33
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    34
text{* Elimination rules for propositional logic:
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    35
\begin{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    36
\begin{tabular}{ll}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    37
@{thm[source]impE} & @{thm impE[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    38
@{thm[source]mp} & @{thm mp[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    39
@{thm[source]conjE} & @{thm conjE[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    40
@{thm[source]disjE} & @{thm disjE[no_vars]}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    41
\end{tabular}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    42
\end{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    43
*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    44
(*<*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    45
thm impE mp
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    46
thm conjE
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    47
thm disjE
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    48
(*>*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    49
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    50
apply (erule disjE)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    51
 apply (rule disjI2)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    52
 apply assumption
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    53
apply (rule disjI1)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    54
apply assumption
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    55
done
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    56
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    57
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    58
subsection{*Negation*}
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    59
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    60
text{*
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    61
\begin{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    62
\begin{tabular}{ll}
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    63
@{thm[source]notI} & @{thm notI[no_vars]} \\
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    64
@{thm[source]notE} & @{thm notE[no_vars]} \\
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    65
@{thm[source]ccontr} & @{thm ccontr[no_vars]}
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    66
\end{tabular}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    67
\end{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    68
*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    69
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    70
(*<*)thm notI notE ccontr(*>*)
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    71
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    72
lemma "\<not>\<not>P \<Longrightarrow> P"
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    73
apply (rule ccontr)
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    74
apply (erule notE)
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    75
apply assumption
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    76
done
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    77
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    78
text{*A simple exercise:*}
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    79
lemma "\<not>P \<or> \<not>Q \<Longrightarrow> \<not>(P \<and> Q)"
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    80
(*<*)oops(*>*)
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
    81
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    82
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    83
subsection{*Quantifiers*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    84
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    85
text{* Quantifier rules:
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    86
\begin{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    87
\begin{tabular}{ll}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    88
@{thm[source]allI} & @{thm allI[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    89
@{thm[source]exI} & @{thm exI[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    90
@{thm[source]allE} & @{thm allE[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    91
@{thm[source]exE} & @{thm exE[no_vars]} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    92
@{thm[source]spec} & @{thm spec[no_vars]}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    93
\end{tabular}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    94
\end{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    95
*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    96
(*<*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    97
thm allI exI
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    98
thm allE exE
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
    99
thm spec
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   100
(*>*)
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
   101
text{*Another classic exercise:*}
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   102
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   103
(*<*)oops(*>*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   104
13489
79d117a158bd *** empty log message ***
nipkow
parents: 13262
diff changeset
   105
13262
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   106
subsection{*Instantiation*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   107
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   108
lemma "\<exists>xs. xs @ xs = xs"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   109
apply(rule_tac x = "[]" in exI)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   110
by simp
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   111
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   112
lemma "\<forall>xs. f(xs @ xs) = xs \<Longrightarrow> f [] = []"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   113
apply(erule_tac x = "[]" in allE)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   114
by simp
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   115
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   116
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   117
subsection{*Automation*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   118
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   119
lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>  
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   120
       \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and> 
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   121
       (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and> 
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   122
       (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and> 
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   123
       (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))  
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   124
       \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   125
by blast
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   126
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   127
lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   128
       (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   129
by fast
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   130
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   131
lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   132
apply(clarify)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   133
by blast
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   134
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   135
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   136
subsection{*Forward Proof*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   137
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   138
text{*
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   139
Instantiation of unknowns (in left-to-right order):
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   140
\begin{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   141
\begin{tabular}{@ {}ll@ {}}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   142
@{thm[source]append_self_conv} & @{thm append_self_conv} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   143
@{thm[source]append_self_conv[of _ "[]"]} & @{thm append_self_conv[of _ "[]"]}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   144
\end{tabular}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   145
\end{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   146
Applying one theorem to another
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   147
by unifying the premise of one theorem with the conclusion of another:
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   148
\begin{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   149
\begin{tabular}{@ {}ll@ {}}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   150
@{thm[source]sym} & @{thm sym} \\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   151
@{thm[source]sym[OF append_self_conv]} & @{thm sym[OF append_self_conv]}\\
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   152
@{thm[source]append_self_conv[THEN sym]} & @{thm append_self_conv[THEN sym]}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   153
\end{tabular}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   154
\end{center}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   155
*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   156
(*<*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   157
thm append_self_conv
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   158
thm append_self_conv[of _ "[]"]
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   159
thm sym
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   160
thm sym[OF append_self_conv]
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   161
thm append_self_conv[THEN sym]
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   162
(*>*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   163
subsection{*Further Useful Methods*}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   164
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   165
lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   166
apply(subgoal_tac "n=1")
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   167
 apply simp
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   168
apply arith
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   169
done
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   170
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   171
text{* And a cute example: *}
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   172
lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q;
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   173
         \<forall>x y z. sqrt x * sqrt x = x \<and>
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   174
                  x ^ 2 = x * x \<and>
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   175
                 (x ^ y) ^ z = x ^ (y*z)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   176
       \<rbrakk> \<Longrightarrow> \<exists>a b. a \<notin> Q \<and> b \<notin> Q \<and> a ^ b \<in> Q"
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   177
(*
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   178
apply(case_tac "")
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   179
 apply blast
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   180
apply(rule_tac x = "" in exI)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   181
apply(rule_tac x = "" in exI)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   182
apply simp
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   183
done
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   184
*)
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   185
(*<*)oops
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   186
bbfc360db011 *** empty log message ***
nipkow
parents:
diff changeset
   187
end(*>*)