src/FOL/ex/Intuitionistic.thy
author haftmann
Thu, 24 Jul 2025 17:46:29 +0200
changeset 82902 99a720d3ed8f
parent 75400 970b9ab6c439
permissions -rw-r--r--
clarified code setup
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31974
e81979a703a4 removed obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
     1
(*  Title:      FOL/ex/Intuitionistic.thy
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
     4
*)
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     6
section \<open>Intuitionistic First-Order Logic\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
     7
31974
e81979a703a4 removed obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
     8
theory Intuitionistic
e81979a703a4 removed obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
     9
imports IFOL
e81979a703a4 removed obsolete CVS Ids;
wenzelm
parents: 16417
diff changeset
    10
begin
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    11
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    12
(*
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    13
Single-step ML commands:
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    14
by (IntPr.step_tac 1)
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    15
by (biresolve_tac safe_brls 1);
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    16
by (biresolve_tac haz_brls 1);
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    17
by (assume_tac 1);
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    18
by (IntPr.safe_tac 1);
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    19
by (IntPr.mp_tac 1);
51798
ad3a241def73 uniform Proof.context for hyp_subst_tac;
wenzelm
parents: 31974
diff changeset
    20
by (IntPr.fast_tac @{context} 1);
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    21
*)
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    22
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    23
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    24
text\<open>Metatheorem (for \emph{propositional} formulae):
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    25
  $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable.
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    26
  Therefore $\neg P$ is classically provable iff it is intuitionistically
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    27
  provable.
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    28
69591
cc6a21413f8a tuned spelling;
wenzelm
parents: 69590
diff changeset
    29
Proof: Let $Q$ be the conjunction of the propositions $A\vee\neg A$, one for
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    30
each atom $A$ in $P$.  Now $\neg\neg Q$ is intuitionistically provable because
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    31
$\neg\neg(A\vee\neg A)$ is and because double-negation distributes over
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    32
conjunction.  If $P$ is provable classically, then clearly $Q\rightarrow P$ is
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    33
provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    34
intuitionistically.  The latter is intuitionistically equivalent to $\neg\neg
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    35
Q\rightarrow\neg\neg P$, hence to $\neg\neg P$, since $\neg\neg Q$ is
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    36
intuitionistically provable.  Finally, if $P$ is a negation then $\neg\neg P$
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
    37
is intuitionstically equivalent to $P$.  [Andy Pitts]\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    38
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    39
lemma \<open>\<not> \<not> (P \<and> Q) \<longleftrightarrow> \<not> \<not> P \<and> \<not> \<not> Q\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    40
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    41
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    42
lemma \<open>\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longrightarrow> (\<not> P \<longrightarrow> \<not> Q) \<longrightarrow> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    43
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    44
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
    45
text \<open>Double-negation does NOT distribute over disjunction.\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    46
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    47
lemma \<open>\<not> \<not> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> \<not> P \<longrightarrow> \<not> \<not> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    48
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    49
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    50
lemma \<open>\<not> \<not> \<not> P \<longleftrightarrow> \<not> P\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    51
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    52
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    53
lemma \<open>\<not> \<not> ((P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    54
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    55
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    56
lemma \<open>(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    57
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    58
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    59
lemma \<open>((P \<longrightarrow> (Q \<or> (Q \<longrightarrow> R))) \<longrightarrow> R) \<longrightarrow> R\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    60
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    61
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
    62
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    63
  \<open>(((G \<longrightarrow> A) \<longrightarrow> J) \<longrightarrow> D \<longrightarrow> E) \<longrightarrow> (((H \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> C \<longrightarrow> J)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
    64
    \<longrightarrow> (A \<longrightarrow> H) \<longrightarrow> F \<longrightarrow> G \<longrightarrow> (((C \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> D) \<longrightarrow> (A \<longrightarrow> C)
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    65
    \<longrightarrow> (((F \<longrightarrow> A) \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> E\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    66
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    67
75400
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    68
text \<open>Admissibility of the excluded middle for negated formulae\<close>
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    69
lemma \<open>(P \<or> \<not>P \<longrightarrow> \<not>Q) \<longrightarrow> \<not>Q\<close>
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    70
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    71
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    72
text \<open>The same in a more general form, no ex falso quodlibet\<close>
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    73
lemma \<open>(P \<or> (P\<longrightarrow>R) \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> Q \<longrightarrow> R\<close>
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    74
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
970b9ab6c439 two new examples
paulson <lp15@cam.ac.uk>
parents: 69593
diff changeset
    75
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    76
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
    77
subsection \<open>Lemmas for the propositional double-negation translation\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    78
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    79
lemma \<open>P \<longrightarrow> \<not> \<not> P\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    80
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    81
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    82
lemma \<open>\<not> \<not> (\<not> \<not> P \<longrightarrow> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    83
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    84
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    85
lemma \<open>\<not> \<not> P \<and> \<not> \<not> (P \<longrightarrow> Q) \<longrightarrow> \<not> \<not> Q\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    86
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    87
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    88
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
    89
text \<open>The following are classically but not constructively valid.
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
    90
  The attempt to prove them terminates quickly!\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    91
lemma \<open>((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    92
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
    93
apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    94
oops
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    95
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
    96
lemma \<open>(P \<and> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> R) \<or> (Q \<longrightarrow> R)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
    97
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
    98
apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
    99
oops
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   100
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   101
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   102
subsection \<open>de Bruijn formulae\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   103
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   104
text \<open>de Bruijn formula with three predicates\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   105
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   106
  \<open>((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   107
    ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R) \<and>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   108
    ((R \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R) \<longrightarrow> P \<and> Q \<and> R\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   109
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   110
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   111
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   112
text \<open>de Bruijn formula with five predicates\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   113
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   114
  \<open>((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   115
    ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   116
    ((R \<longleftrightarrow> S) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   117
    ((S \<longleftrightarrow> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   118
    ((T \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   119
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   120
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   121
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   122
text \<open>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   123
  Problems from of Sahlin, Franzen and Haridi,
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   124
  An Intuitionistic Predicate Logic Theorem Prover.
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   125
  J. Logic and Comp. 2 (5), October 1992, 619-656.
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   126
\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   127
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   128
text\<open>Problem 1.1\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   129
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   130
  \<open>(\<forall>x. \<exists>y. \<forall>z. p(x) \<and> q(y) \<and> r(z)) \<longleftrightarrow>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   131
    (\<forall>z. \<exists>y. \<forall>x. p(x) \<and> q(y) \<and> r(z))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   132
  by (tactic \<open>IntPr.best_dup_tac \<^context> 1\<close>)  \<comment> \<open>SLOW\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   133
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   134
text\<open>Problem 3.1\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   135
lemma \<open>\<not> (\<exists>x. \<forall>y. mem(y,x) \<longleftrightarrow> \<not> mem(x,x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   136
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   137
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   138
text\<open>Problem 4.1: hopeless!\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   139
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   140
  \<open>(\<forall>x. p(x) \<longrightarrow> p(h(x)) \<or> p(g(x))) \<and> (\<exists>x. p(x)) \<and> (\<forall>x. \<not> p(h(x)))
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   141
    \<longrightarrow> (\<exists>x. p(g(g(g(g(g(x)))))))\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   142
  oops
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   143
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   144
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   145
subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   146
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   147
text\<open>\<open>\<not>\<not>\<close>1\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   148
lemma \<open>\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   149
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   150
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   151
text\<open>\<open>\<not>\<not>\<close>2\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   152
lemma \<open>\<not> \<not> (\<not> \<not> P \<longleftrightarrow> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   153
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   154
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   155
text\<open>3\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   156
lemma \<open>\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   157
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   158
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   159
text\<open>\<open>\<not>\<not>\<close>4\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   160
lemma \<open>\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   161
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   162
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   163
text\<open>\<open>\<not>\<not>\<close>5\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   164
lemma \<open>\<not> \<not> ((P \<or> Q \<longrightarrow> P \<or> R) \<longrightarrow> P \<or> (Q \<longrightarrow> R))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   165
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   166
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   167
text\<open>\<open>\<not>\<not>\<close>6\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   168
lemma \<open>\<not> \<not> (P \<or> \<not> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   169
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   170
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   171
text\<open>\<open>\<not>\<not>\<close>7\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   172
lemma \<open>\<not> \<not> (P \<or> \<not> \<not> \<not> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   173
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   174
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   175
text\<open>\<open>\<not>\<not>\<close>8. Peirce's law\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   176
lemma \<open>\<not> \<not> (((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   177
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   178
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   179
text\<open>9\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   180
lemma \<open>((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   181
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   182
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   183
text\<open>10\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   184
lemma \<open>(Q \<longrightarrow> R) \<longrightarrow> (R \<longrightarrow> P \<and> Q) \<longrightarrow> (P \<longrightarrow> (Q \<or> R)) \<longrightarrow> (P \<longleftrightarrow> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   185
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   186
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   187
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   188
subsection\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   189
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   190
lemma \<open>P \<longleftrightarrow> P\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   191
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   192
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   193
text\<open>\<open>\<not>\<not>\<close>12. Dijkstra's law\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   194
lemma \<open>\<not> \<not> (((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   195
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   196
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   197
lemma \<open>((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longrightarrow> \<not> \<not> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   198
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   199
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   200
text\<open>13. Distributive law\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   201
lemma \<open>P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   202
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   203
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   204
text\<open>\<open>\<not>\<not>\<close>14\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   205
lemma \<open>\<not> \<not> ((P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   206
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   207
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   208
text\<open>\<open>\<not>\<not>\<close>15\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   209
lemma \<open>\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   210
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   211
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   212
text\<open>\<open>\<not>\<not>\<close>16\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   213
lemma \<open>\<not> \<not> ((P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   214
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   215
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   216
text\<open>\<open>\<not>\<not>\<close>17\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   217
lemma \<open>\<not> \<not> (((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   218
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   219
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   220
text \<open>Dijkstra's ``Golden Rule''\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   221
lemma \<open>(P \<and> Q) \<longleftrightarrow> P \<longleftrightarrow> Q \<longleftrightarrow> (P \<or> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   222
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   223
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   224
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   225
section \<open>Examples with quantifiers\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   226
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   227
subsection \<open>The converse is classical in the following implications \dots\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   228
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   229
lemma \<open>(\<exists>x. P(x) \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   230
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   231
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   232
lemma \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. P(x) \<and> \<not> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   233
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   234
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   235
lemma \<open>((\<forall>x. \<not> P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. \<not> (P(x) \<or> Q))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   236
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   237
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   238
lemma \<open>(\<forall>x. P(x)) \<or> Q \<longrightarrow> (\<forall>x. P(x) \<or> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   239
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   240
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   241
lemma \<open>(\<exists>x. P \<longrightarrow> Q(x)) \<longrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   242
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   243
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   244
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   245
subsection \<open>The following are not constructively valid!\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   246
text \<open>The attempt to prove them terminates quickly!\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   247
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   248
lemma \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   249
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   250
  apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   251
  oops
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   252
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   253
lemma \<open>(P \<longrightarrow> (\<exists>x. Q(x))) \<longrightarrow> (\<exists>x. P \<longrightarrow> Q(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   254
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   255
  apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   256
  oops
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   257
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   258
lemma \<open>(\<forall>x. P(x) \<or> Q) \<longrightarrow> ((\<forall>x. P(x)) \<or> Q)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   259
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   260
  apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   261
  oops
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   262
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   263
lemma \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   264
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   265
  apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   266
  oops
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   267
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   268
text \<open>Classically but not intuitionistically valid.  Proved by a bug in 1986!\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   269
lemma \<open>\<exists>x. Q(x) \<longrightarrow> (\<forall>x. Q(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   270
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)?
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   271
  apply (rule asm_rl) \<comment> \<open>Checks that subgoals remain: proof failed.\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   272
  oops
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   273
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   274
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   275
subsection \<open>Hard examples with quantifiers\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   276
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   277
text \<open>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   278
  The ones that have not been proved are not known to be valid! Some will
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   279
  require quantifier duplication -- not currently available.
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   280
\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   281
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   282
text\<open>\<open>\<not>\<not>\<close>18\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   283
lemma \<open>\<not> \<not> (\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x))\<close>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   284
  oops  \<comment> \<open>NOT PROVED\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   285
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   286
text\<open>\<open>\<not>\<not>\<close>19\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   287
lemma \<open>\<not> \<not> (\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x)))\<close>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   288
  oops  \<comment> \<open>NOT PROVED\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   289
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   290
text\<open>20\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   291
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   292
  \<open>(\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y) \<longrightarrow> R(z) \<and> S(w)))
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   293
    \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   294
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   295
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   296
text\<open>21\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   297
lemma \<open>(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> \<not> \<not> (\<exists>x. P \<longleftrightarrow> Q(x))\<close>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   298
  oops \<comment> \<open>NOT PROVED; needs quantifier duplication\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   299
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   300
text\<open>22\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   301
lemma \<open>(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   302
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   303
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   304
text\<open>\<open>\<not>\<not>\<close>23\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   305
lemma \<open>\<not> \<not> ((\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x))))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   306
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   307
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   308
text\<open>24\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   309
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   310
  \<open>\<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   311
    (\<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   312
    \<longrightarrow> \<not> \<not> (\<exists>x. P(x) \<and> R(x))\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   313
text \<open>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   314
  Not clear why \<open>fast_tac\<close>, \<open>best_tac\<close>, \<open>ASTAR\<close> and
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   315
  \<open>ITER_DEEPEN\<close> all take forever.
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   316
\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   317
  apply (tactic \<open>IntPr.safe_tac \<^context>\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   318
  apply (erule impE)
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   319
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   320
  apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   321
  done
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   322
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   323
text\<open>25\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   324
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   325
  \<open>(\<exists>x. P(x)) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   326
      (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   327
      (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   328
      ((\<forall>x. P(x) \<longrightarrow> Q(x)) \<or> (\<exists>x. P(x) \<and> R(x)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   329
    \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   330
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   331
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   332
text\<open>\<open>\<not>\<not>\<close>26\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   333
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   334
  \<open>(\<not> \<not> (\<exists>x. p(x)) \<longleftrightarrow> \<not> \<not> (\<exists>x. q(x))) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   335
    (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   336
  \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))\<close>
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   337
  oops  \<comment> \<open>NOT PROVED\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   338
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   339
text\<open>27\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   340
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   341
  \<open>(\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   342
    (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   343
    (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   344
    ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   345
  \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   346
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   347
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   348
text\<open>\<open>\<not>\<not>\<close>28. AMENDED\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   349
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   350
  \<open>(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   351
      (\<not> \<not> (\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   352
      (\<not> \<not> (\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   353
    \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   354
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   355
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   356
text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   357
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   358
  \<open>(\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   359
    \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   360
      (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   361
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   362
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   363
text\<open>\<open>\<not>\<not>\<close>30\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   364
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   365
  \<open>(\<forall>x. (P(x) \<or> Q(x)) \<longrightarrow> \<not> R(x)) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   366
      (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   367
    \<longrightarrow> (\<forall>x. \<not> \<not> S(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   368
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   369
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   370
text\<open>31\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   371
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   372
  \<open>\<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   373
      (\<exists>x. L(x) \<and> P(x)) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   374
      (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   375
  \<longrightarrow> (\<exists>x. L(x) \<and> M(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   376
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   377
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   378
text\<open>32\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   379
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   380
  \<open>(\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   381
    (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   382
    (\<forall>x. M(x) \<longrightarrow> R(x))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   383
  \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   384
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   385
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61490
diff changeset
   386
text\<open>\<open>\<not>\<not>\<close>33\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   387
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   388
  \<open>(\<forall>x. \<not> \<not> (P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c))) \<longleftrightarrow>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   389
    (\<forall>x. \<not> \<not> ((\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c))))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   390
  apply (tactic \<open>IntPr.best_tac \<^context> 1\<close>)
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   391
  done
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   392
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   393
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   394
text\<open>36\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   395
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   396
  \<open>(\<forall>x. \<exists>y. J(x,y)) \<and>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   397
    (\<forall>x. \<exists>y. G(x,y)) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   398
    (\<forall>x y. J(x,y) \<or> G(x,y) \<longrightarrow> (\<forall>z. J(y,z) \<or> G(y,z) \<longrightarrow> H(x,z)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   399
  \<longrightarrow> (\<forall>x. \<exists>y. H(x,y))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   400
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   401
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   402
text\<open>37\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   403
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   404
  \<open>(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   405
      \<not> \<not> (P(x,z) \<longrightarrow> P(y,w)) \<and> P(y,z) \<and> (P(y,w) \<longrightarrow> (\<exists>u. Q(u,w)))) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   406
        (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   407
        (\<not> \<not> (\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   408
    \<longrightarrow> \<not> \<not> (\<forall>x. \<exists>y. R(x,y))\<close>
67443
3abf6a722518 standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents: 62020
diff changeset
   409
  oops  \<comment> \<open>NOT PROVED\<close>
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   410
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   411
text\<open>39\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   412
lemma \<open>\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   413
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   414
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   415
text\<open>40. AMENDED\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   416
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   417
  \<open>(\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   418
    \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   419
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   420
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   421
text\<open>44\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   422
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   423
  \<open>(\<forall>x. f(x) \<longrightarrow>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   424
    (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   425
    (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h(x,y)))
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   426
    \<longrightarrow> (\<exists>x. j(x) \<and> \<not> f(x))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   427
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   428
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   429
text\<open>48\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   430
lemma \<open>(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   431
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   432
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   433
text\<open>51\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   434
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   435
  \<open>(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   436
    (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   437
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   438
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   439
text\<open>52\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   440
text \<open>Almost the same as 51.\<close>
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   441
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   442
  \<open>(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   443
    (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   444
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   445
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   446
text\<open>56\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   447
lemma \<open>(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   448
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   449
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   450
text\<open>57\<close>
61489
b8d375aee0df more symbols;
wenzelm
parents: 60770
diff changeset
   451
lemma
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   452
  \<open>P(f(a,b), f(b,c)) \<and> P(f(b,c), f(a,c)) \<and>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   453
    (\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   454
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   455
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
   456
text\<open>60\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 67443
diff changeset
   457
lemma \<open>\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69591
diff changeset
   458
  by (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)
14239
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   459
af2a9e68bea9 partial conversion to Isar scripts
paulson
parents:
diff changeset
   460
end