doc-src/TutorialI/Rules/Blast.thy
author huffman
Fri, 04 Nov 2011 07:04:34 +0100
changeset 45333 04b21922ed68
parent 42637 381fdcab0f36
permissions -rw-r--r--
ex/Tree23.thy: simpler definition of ordered-ness predicate
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 10844
diff changeset
     1
theory Blast imports Main begin
10295
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     2
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     3
lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y))))   =    
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     4
       ((\<exists>x. \<forall>y. q(x)=q(y)) = ((\<exists>x. p(x))=(\<forall>y. q(y))))"
10844
0c0e7de7e9c5 now using "by" for one-line proofs
paulson
parents: 10341
diff changeset
     5
by blast
10295
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     6
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     7
text{*\noindent Until now, we have proved everything using only induction and
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     8
simplification.  Substantial proofs require more elaborate types of
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
     9
inference.*}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    10
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    11
lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    12
       \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and> 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    13
       (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and> 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    14
       (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and> 
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    15
       (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))  
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    16
       \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
10844
0c0e7de7e9c5 now using "by" for one-line proofs
paulson
parents: 10341
diff changeset
    17
by blast
10295
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    18
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    19
lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    20
        (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
10844
0c0e7de7e9c5 now using "by" for one-line proofs
paulson
parents: 10341
diff changeset
    21
by blast
10295
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    22
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    23
text {*
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    24
@{thm[display] mult_is_0}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    25
 \rulename{mult_is_0}}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    26
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    27
@{thm[display] finite_Un}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    28
 \rulename{finite_Un}}
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    29
*};
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    30
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    31
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    32
lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])"
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    33
  apply (induct_tac xs)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    34
  by (simp_all);
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    35
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    36
(*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*)
8eb12693cead the Rules chapter and theories
paulson
parents:
diff changeset
    37
end