src/ZF/Induct/PropLog.thy
author nipkow
Sun, 04 Nov 2018 12:07:24 +0100
changeset 69232 2b913054a9cf
parent 65449 c82e63b11b8b
child 69587 53982d5ec0bb
permissions -rw-r--r--
Faster Braun tree functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
     1
(*  Title:      ZF/Induct/PropLog.thy
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     2
    Author:     Tobias Nipkow & Lawrence C Paulson
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
     4
*)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
     5
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
     6
section \<open>Meta-theory of propositional logic\<close>
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     7
65449
c82e63b11b8b clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents: 61798
diff changeset
     8
theory PropLog imports ZF begin
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
     9
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    10
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    11
  Datatype definition of propositional logic formulae and inductive
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    12
  definition of the propositional tautologies.
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    13
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    14
  Inductive definition of propositional logic.  Soundness and
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    15
  completeness w.r.t.\ truth-tables.
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    16
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    17
  Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in>
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    18
  Fin(H)\<close>
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    19
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    20
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    21
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    22
subsection \<open>The datatype of propositions\<close>
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    23
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    24
consts
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    25
  propn :: i
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    26
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    27
datatype propn =
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    28
    Fls
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    29
  | Var ("n \<in> nat")    ("#_" [100] 100)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    30
  | Imp ("p \<in> propn", "q \<in> propn")    (infixr "=>" 90)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    31
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    32
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    33
subsection \<open>The proof system\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    34
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    35
consts thms     :: "i => i"
35068
544867142ea4 modernized translations;
wenzelm
parents: 24893
diff changeset
    36
544867142ea4 modernized translations;
wenzelm
parents: 24893
diff changeset
    37
abbreviation
544867142ea4 modernized translations;
wenzelm
parents: 24893
diff changeset
    38
  thms_syntax :: "[i,i] => o"    (infixl "|-" 50)
544867142ea4 modernized translations;
wenzelm
parents: 24893
diff changeset
    39
  where "H |- p == p \<in> thms(H)"
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    40
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    41
inductive
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    42
  domains "thms(H)" \<subseteq> "propn"
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    43
  intros
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    44
    H:  "[| p \<in> H;  p \<in> propn |] ==> H |- p"
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    45
    K:  "[| p \<in> propn;  q \<in> propn |] ==> H |- p=>q=>p"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    46
    S:  "[| p \<in> propn;  q \<in> propn;  r \<in> propn |]
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    47
         ==> H |- (p=>q=>r) => (p=>q) => p=>r"
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    48
    DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p"
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    49
    MP: "[| H |- p=>q;  H |- p;  p \<in> propn;  q \<in> propn |] ==> H |- q"
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    50
  type_intros "propn.intros"
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
    51
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    52
declare propn.intros [simp]
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    53
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    54
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    55
subsection \<open>The semantics\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    56
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    57
subsubsection \<open>Semantics of propositional logic.\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    58
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    59
consts
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    60
  is_true_fun :: "[i,i] => i"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    61
primrec
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    62
  "is_true_fun(Fls, t) = 0"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    63
  "is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    64
  "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    65
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 20503
diff changeset
    66
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 20503
diff changeset
    67
  is_true :: "[i,i] => o"  where
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    68
  "is_true(p,t) == is_true_fun(p,t) = 1"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    69
  \<comment> \<open>this definition is required since predicates can't be recursive\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    70
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
    71
lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    72
  by (simp add: is_true_def)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    73
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
    74
lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    75
  by (simp add: is_true_def)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    76
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
    77
lemma is_true_Imp [simp]: "is_true(p=>q,t) \<longleftrightarrow> (is_true(p,t)\<longrightarrow>is_true(q,t))"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    78
  by (simp add: is_true_def)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    79
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    80
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    81
subsubsection \<open>Logical consequence\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    82
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    83
text \<open>
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    84
  For every valuation, if all elements of \<open>H\<close> are true then so
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    85
  is \<open>p\<close>.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    86
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    87
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 20503
diff changeset
    88
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 20503
diff changeset
    89
  logcon :: "[i,i] => o"    (infixl "|=" 50)  where
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
    90
  "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    91
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
    92
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    93
text \<open>
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    94
  A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
    95
  \<open>p\<close>.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
    96
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    97
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    98
consts
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
    99
  hyps :: "[i,i] => i"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   100
primrec
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   101
  "hyps(Fls, t) = 0"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   102
  "hyps(Var(v), t) = (if v \<in> t then {#v} else {#v=>Fls})"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   103
  "hyps(p=>q, t) = hyps(p,t) \<union> hyps(q,t)"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   104
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   105
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   106
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   107
subsection \<open>Proof theory of propositional logic\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   108
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   109
lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   110
  apply (unfold thms.defs)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   111
  apply (rule lfp_mono)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   112
    apply (rule thms.bnd_mono)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   113
  apply (assumption | rule univ_mono basic_monos)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   114
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   115
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   116
lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   117
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   118
inductive_cases ImpE: "p=>q \<in> propn"
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   119
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   120
lemma thms_MP: "[| H |- p=>q;  H |- p |] ==> H |- q"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   121
  \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   122
  apply (rule thms.MP)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   123
     apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   124
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   125
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   126
lemma thms_I: "p \<in> propn ==> H |- p=>p"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   127
  \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   128
  apply (rule thms.S [THEN thms_MP, THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   129
      apply (rule_tac [5] thms.K)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   130
       apply (rule_tac [4] thms.K)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   131
         apply simp_all
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   132
  done
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   133
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   134
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   135
subsubsection \<open>Weakening, left and right\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   136
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   137
lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   138
  \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   139
  by (erule thms_mono [THEN subsetD])
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   140
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   141
lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   142
  by (erule subset_consI [THEN weaken_left])
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   143
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   144
lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   145
lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   146
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   147
lemma weaken_right: "[| H |- q;  p \<in> propn |] ==> H |- p=>q"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   148
  by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   149
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   150
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   151
subsubsection \<open>The deduction theorem\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   152
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   153
theorem deduction: "[| cons(p,H) |- q;  p \<in> propn |] ==>  H |- p=>q"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   154
  apply (erule thms.induct)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   155
      apply (blast intro: thms_I thms.H [THEN weaken_right])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   156
     apply (blast intro: thms.K [THEN weaken_right])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   157
    apply (blast intro: thms.S [THEN weaken_right])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   158
   apply (blast intro: thms.DN [THEN weaken_right])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   159
  apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   160
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   161
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   162
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   163
subsubsection \<open>The cut rule\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   164
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   165
lemma cut: "[| H|-p;  cons(p,H) |- q |] ==>  H |- q"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   166
  apply (rule deduction [THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   167
    apply (simp_all add: thms_in_pl)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   168
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   169
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   170
lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   171
  apply (rule thms.DN [THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   172
   apply (rule_tac [2] weaken_right)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   173
    apply (simp_all add: propn.intros)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   174
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   175
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   176
lemma thms_notE: "[| H |- p=>Fls;  H |- p;  q \<in> propn |] ==> H |- q"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   177
  by (erule thms_MP [THEN thms_FlsE])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   178
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   179
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   180
subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   181
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   182
theorem soundness: "H |- p ==> H |= p"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   183
  apply (unfold logcon_def)
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16417
diff changeset
   184
  apply (induct set: thms)
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   185
      apply auto
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   186
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   187
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   188
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   189
subsection \<open>Completeness\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   190
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   191
subsubsection \<open>Towards the completeness proof\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   192
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   193
lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   194
  apply (frule thms_in_pl)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   195
  apply (rule deduction)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   196
   apply (rule weaken_left_cons [THEN thms_notE])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   197
     apply (blast intro: thms.H elim: ImpE)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   198
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   199
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   200
lemma Imp_Fls: "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   201
  apply (frule thms_in_pl)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   202
  apply (frule thms_in_pl [of concl: "q=>Fls"])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   203
  apply (rule deduction)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   204
   apply (erule weaken_left_cons [THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   205
   apply (rule consI1 [THEN thms.H, THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   206
    apply (blast intro: weaken_left_cons elim: ImpE)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   207
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   208
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   209
lemma hyps_thms_if:
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   210
    "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   211
  \<comment> \<open>Typical example of strengthening the induction statement.\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   212
  apply simp
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   213
  apply (induct_tac p)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   214
    apply (simp_all add: thms_I thms.H)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   215
  apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   216
  apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   217
  done
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   218
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   219
lemma logcon_thms_p: "[| p \<in> propn;  0 |= p |] ==> hyps(p,t) |- p"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   220
  \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   221
  apply (drule hyps_thms_if)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   222
  apply (simp add: logcon_def)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   223
  done
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   224
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   225
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   226
  For proving certain theorems in our new propositional logic.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   227
\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   228
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   229
lemmas propn_SIs = propn.intros deduction
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   230
  and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   231
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   232
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   233
  The excluded middle in the form of an elimination rule.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   234
\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   235
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   236
lemma thms_excluded_middle:
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   237
    "[| p \<in> propn;  q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   238
  apply (rule deduction [THEN deduction])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   239
    apply (rule thms.DN [THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   240
     apply (best intro!: propn_SIs intro: propn_Is)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   241
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   242
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   243
lemma thms_excluded_middle_rule:
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   244
  "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \<in> propn |] ==> H |- q"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   245
  \<comment> \<open>Hard to prove directly because it requires cuts\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   246
  apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   247
     apply (blast intro!: propn_SIs intro: propn_Is)+
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   248
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   249
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   250
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   251
subsubsection \<open>Completeness -- lemmas for reducing the set of assumptions\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   252
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   253
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   254
  For the case @{prop "hyps(p,t)-cons(#v,Y) |- p"} we also have @{prop
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   255
  "hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v})"}.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   256
\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   257
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   258
lemma hyps_Diff:
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   259
    "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16417
diff changeset
   260
  by (induct set: propn) auto
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   261
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   262
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   263
  For the case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} we also have
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   264
  @{prop "hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t))"}.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   265
\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   266
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   267
lemma hyps_cons:
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   268
    "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16417
diff changeset
   269
  by (induct set: propn) auto
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   270
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   271
text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   272
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   273
lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   274
  by blast
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   275
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   276
lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   277
  by blast
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   278
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   279
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   280
  The set @{term "hyps(p,t)"} is finite, and elements have the form
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   281
  @{term "#v"} or @{term "#v=>Fls"}; could probably prove the stronger
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   282
  @{prop "hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))"}.
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   283
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   284
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   285
lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16417
diff changeset
   286
  by (induct set: propn) auto
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   287
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   288
lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   289
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   290
text \<open>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   291
  Induction on the finite set of assumptions @{term "hyps(p,t0)"}.  We
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   292
  may repeatedly subtract assumptions until none are left!
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   293
\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   294
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   295
lemma completeness_0_lemma [rule_format]:
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   296
    "[| p \<in> propn;  0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   297
  apply (frule hyps_finite)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   298
  apply (erule Fin_induct)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   299
   apply (simp add: logcon_thms_p Diff_0)
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   300
  txt \<open>inductive step\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   301
  apply safe
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   302
   txt \<open>Case @{prop "hyps(p,t)-cons(#v,Y) |- p"}\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   303
   apply (rule thms_excluded_middle_rule)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   304
     apply (erule_tac [3] propn.intros)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   305
    apply (blast intro: cons_Diff_same [THEN weaken_left])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   306
   apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   307
     hyps_Diff [THEN Diff_weaken_left])
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   308
  txt \<open>Case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"}\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   309
  apply (rule thms_excluded_middle_rule)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   310
    apply (erule_tac [3] propn.intros)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   311
   apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   312
     hyps_cons [THEN Diff_weaken_left])
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   313
  apply (blast intro: cons_Diff_same [THEN weaken_left])
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   314
  done
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   315
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   316
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 58871
diff changeset
   317
subsubsection \<open>Completeness theorem\<close>
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   318
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   319
lemma completeness_0: "[| p \<in> propn;  0 |= p |] ==> 0 |- p"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   320
  \<comment> \<open>The base case for completeness\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   321
  apply (rule Diff_cancel [THEN subst])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   322
  apply (blast intro: completeness_0_lemma)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   323
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   324
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   325
lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
61798
27f3c10b0b50 isabelle update_cartouches -c -t;
wenzelm
parents: 60770
diff changeset
   326
  \<comment> \<open>A semantic analogue of the Deduction Theorem\<close>
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   327
  by (simp add: logcon_def)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   328
18415
eb68dc98bda2 improved proofs;
wenzelm
parents: 16417
diff changeset
   329
lemma completeness:
eb68dc98bda2 improved proofs;
wenzelm
parents: 16417
diff changeset
   330
     "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 18415
diff changeset
   331
  apply (induct arbitrary: p set: Fin)
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   332
   apply (safe intro!: completeness_0)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   333
  apply (rule weaken_left_cons [THEN thms_MP])
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   334
   apply (blast intro!: logcon_Imp propn.intros)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   335
  apply (blast intro: propn_Is)
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   336
  done
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   337
46822
95f1e700b712 mathematical symbols for Isabelle/ZF example theories
paulson
parents: 35762
diff changeset
   338
theorem thms_iff: "H \<in> Fin(propn) ==> H |- p \<longleftrightarrow> H |= p \<and> p \<in> propn"
12610
8b9845807f77 tuned document sources;
wenzelm
parents: 12560
diff changeset
   339
  by (blast intro: soundness completeness thms_in_pl)
12560
5820841f21fd converted some ZF/Induct examples to Isar
paulson
parents: 12088
diff changeset
   340
12088
6f463d16cbd0 reorganization of the ZF examples
paulson
parents:
diff changeset
   341
end