src/Doc/Logics_ZF/FOL_examples.thy
author wenzelm
Fri Jan 12 14:08:53 2018 +0100 (21 months ago)
changeset 67406 23307fd33906
parent 66453 cc19f7ca2ed6
child 67443 3abf6a722518
permissions -rw-r--r--
isabelle update_cartouches -c;
wenzelm@67406
     1
section\<open>Examples of Classical Reasoning\<close>
paulson@14152
     2
wenzelm@66453
     3
theory FOL_examples imports FOL begin
paulson@14152
     4
paulson@14152
     5
lemma "EX y. ALL x. P(y)-->P(x)"
wenzelm@67406
     6
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
     7
apply (rule exCI)
wenzelm@67406
     8
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
     9
apply (rule allI)
wenzelm@67406
    10
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
    11
apply (rule impI)
wenzelm@67406
    12
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
    13
apply (erule allE)
wenzelm@67406
    14
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
wenzelm@67406
    15
txt\<open>see below for @{text allI} combined with @{text swap}\<close>
paulson@14152
    16
apply (erule allI [THEN [2] swap])
wenzelm@67406
    17
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
    18
apply (rule impI)
wenzelm@67406
    19
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
    20
apply (erule notE)
wenzelm@67406
    21
  \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
paulson@14152
    22
apply assumption
paulson@14152
    23
done
paulson@14152
    24
wenzelm@67406
    25
text \<open>
paulson@14152
    26
@{thm[display] allI [THEN [2] swap]}
wenzelm@67406
    27
\<close>
paulson@14152
    28
paulson@14152
    29
lemma "EX y. ALL x. P(y)-->P(x)"
paulson@14152
    30
by blast
paulson@14152
    31
paulson@14152
    32
end
paulson@14152
    33
paulson@14152
    34