src/Doc/Tutorial/Rules/Force.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 64242 93c6f0da5c70
permissions -rw-r--r--
eliminated spurious semicolons;
     1 theory Force imports Main begin 
     2   (*Use Divides rather than Main to experiment with the first proof.
     3     Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
     4 
     5 declare div_mult_self_is_m [simp del]
     6 
     7 lemma div_mult_self_is_m: 
     8       "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
     9 apply (insert mod_div_equality [of "m*n" n])
    10 apply simp
    11 done
    12 
    13 
    14 lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)"
    15 apply clarify
    16 oops
    17 
    18 text {*
    19 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
    20 \isanewline
    21 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
    22 {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ Q\ x{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\isanewline
    23 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ xa{\isachardot}\ {\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x{\isacharsemicolon}\ Q\ xa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ {\isasymand}\ Q\ x
    24 *}
    25 
    26 text {*
    27 couldn't find a good example of clarsimp
    28 
    29 @{thm[display]"someI"}
    30 \rulename{someI}
    31 *}
    32 
    33 lemma "\<lbrakk>Q a; P a\<rbrakk> \<Longrightarrow> P (SOME x. P x \<and> Q x) \<and> Q (SOME x. P x \<and> Q x)"
    34 apply (rule someI)
    35 oops
    36 
    37 lemma "\<lbrakk>Q a; P a\<rbrakk> \<Longrightarrow> P (SOME x. P x \<and> Q x) \<and> Q (SOME x. P x \<and> Q x)"
    38 apply (fast intro!: someI)
    39 done
    40 
    41 text{*
    42 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ \isadigit{1}\isanewline
    43 \isanewline
    44 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
    45 {\isasymlbrakk}Q\ a{\isacharsemicolon}\ P\ a{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}SOME\ x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\ {\isasymand}\ Q\ {\isacharparenleft}SOME\ x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\isanewline
    46 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}Q\ a{\isacharsemicolon}\ P\ a{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharquery}x\ {\isasymand}\ Q\ {\isacharquery}x
    47 *}
    48 
    49 end
    50