src/HOL/Induct/PropLog.thy
author paulson
Tue, 02 Apr 2002 14:28:28 +0200
changeset 13075 d3e1d554cd6d
parent 10759 994877ee68cb
child 16417 9bc16273c2d4
permissions -rw-r--r--
conversion of some HOL/Induct proof scripts to Isar
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
     1
(*  Title:      HOL/Induct/PropLog.thy
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
     4
    Copyright   1994  TU Muenchen & University of Cambridge
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
     7
header {* Meta-theory of propositional logic *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
     8
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
     9
theory PropLog = Main:
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    10
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    11
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    12
  Datatype definition of propositional logic formulae and inductive
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    13
  definition of the propositional tautologies.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    14
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    15
  Inductive definition of propositional logic.  Soundness and
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    16
  completeness w.r.t.\ truth-tables.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    17
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    18
  Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    19
  Fin(H)"}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    20
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    21
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    22
subsection {* The datatype of propositions *}
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    23
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
datatype
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    25
    'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    26
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    27
subsection {* The proof system *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    28
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
consts
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    30
  thms  :: "'a pl set => 'a pl set"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    31
  "|-"  :: "['a pl set, 'a pl] => bool"   (infixl 50)
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
translations
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    34
  "H |- p" == "p \<in> thms(H)"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
inductive "thms(H)"
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    37
  intros
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    38
  H [intro]:  "p\<in>H ==> H |- p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    39
  K:          "H |- p->q->p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    40
  S:          "H |- (p->q->r) -> (p->q) -> p->r"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    41
  DN:         "H |- ((p->false) -> false) -> p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    42
  MP:         "[| H |- p->q; H |- p |] ==> H |- q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    43
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    44
subsection {* The semantics *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    45
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    46
subsubsection {* Semantics of propositional logic. *}
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    48
consts
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    49
  eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    50
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    51
primrec     "tt[[false]] = False"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    52
	    "tt[[#v]]    = (v \<in> tt)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    53
  eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    55
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    56
  A finite set of hypotheses from @{text t} and the @{text Var}s in
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    57
  @{text p}.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    58
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    59
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    60
consts
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    61
  hyps  :: "['a pl, 'a set] => 'a pl set"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3842
diff changeset
    63
primrec
10759
994877ee68cb *** empty log message ***
nipkow
parents: 9101
diff changeset
    64
  "hyps false  tt = {}"
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    65
  "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
10759
994877ee68cb *** empty log message ***
nipkow
parents: 9101
diff changeset
    66
  "hyps (p->q) tt = hyps p tt Un hyps q tt"
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    68
subsubsection {* Logical consequence *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    69
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    70
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    71
  For every valuation, if all elements of @{text H} are true then so
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    72
  is @{text p}.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    73
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    74
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    75
constdefs
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    76
  sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    77
    "H |= p  ==  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    78
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    79
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    80
subsection {* Proof theory of propositional logic *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    81
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    82
lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    83
apply (unfold thms.defs )
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    84
apply (rule lfp_mono)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    85
apply (assumption | rule basic_monos)+
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    86
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    87
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    88
lemma thms_I: "H |- p->p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    89
  -- {*Called @{text I} for Identity Combinator, not for Introduction. *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    90
by (best intro: thms.K thms.S thms.MP)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    91
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    92
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    93
subsubsection {* Weakening, left and right *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    94
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    95
lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    96
  -- {* Order of premises is convenient with @{text THEN} *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    97
  by (erule thms_mono [THEN subsetD])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    98
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
    99
lemmas weaken_left_insert = subset_insertI [THEN weaken_left]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   100
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   101
lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   102
lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   103
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   104
lemma weaken_right: "H |- q ==> H |- p->q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   105
by (fast intro: thms.K thms.MP)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   106
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   107
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   108
subsubsection {* The deduction theorem *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   109
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   110
theorem deduction: "insert p H |- q  ==>  H |- p->q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   111
apply (erule thms.induct)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   112
apply (fast intro: thms_I thms.H thms.K thms.S thms.DN 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   113
                   thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   114
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   115
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   116
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   117
subsubsection {* The cut rule *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   118
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   119
lemmas cut = deduction [THEN thms.MP]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   120
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   121
lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   122
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   123
lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   124
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   125
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   126
subsubsection {* Soundness of the rules wrt truth-table semantics *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   127
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   128
theorem soundness: "H |- p ==> H |= p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   129
apply (unfold sat_def)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   130
apply (erule thms.induct, auto) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   131
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   132
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   133
subsection {* Completeness *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   134
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   135
subsubsection {* Towards the completeness proof *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   136
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   137
lemma false_imp: "H |- p->false ==> H |- p->q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   138
apply (rule deduction)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   139
apply (erule weaken_left_insert [THEN thms_notE])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   140
apply blast
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   141
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   142
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   143
lemma imp_false:
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   144
    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   145
apply (rule deduction)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   146
apply (blast intro: weaken_left_insert thms.MP thms.H) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   147
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   148
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   149
lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   150
  -- {* Typical example of strengthening the induction statement. *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   151
apply simp 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   152
apply (induct_tac "p")
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   153
apply (simp_all add: thms_I thms.H)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   154
apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   155
                    imp_false false_imp)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   156
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   157
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   158
lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   159
  -- {* Key lemma for completeness; yields a set of assumptions 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   160
        satisfying @{text p} *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   161
apply (unfold sat_def) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   162
apply (drule spec, erule mp [THEN if_P, THEN subst], 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   163
       rule_tac [2] hyps_thms_if, simp)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   164
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   165
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   166
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   167
  For proving certain theorems in our new propositional logic.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   168
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   169
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   170
declare deduction [intro!]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   171
declare thms.H [THEN thms.MP, intro]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   172
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   173
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   174
  The excluded middle in the form of an elimination rule.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   175
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   176
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   177
lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   178
apply (rule deduction [THEN deduction])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   179
apply (rule thms.DN [THEN thms.MP], best) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   180
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   181
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   182
lemma thms_excluded_middle_rule:
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   183
    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   184
  -- {* Hard to prove directly because it requires cuts *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   185
by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   186
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   187
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   188
subsection{* Completeness -- lemmas for reducing the set of assumptions*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   189
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   190
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   191
  For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   192
  "hyps p t - {#v} \<subseteq> hyps p (t-{v})"}.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   193
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   194
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   195
lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   196
by (induct_tac "p", auto) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   197
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   198
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   199
  For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   200
  @{prop "hyps p t-{#v->Fls} \<subseteq> hyps p (insert v t)"}.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   201
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   202
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   203
lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   204
by (induct_tac "p", auto)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   205
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   206
text {* Two lemmas for use with @{text weaken_left} *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   207
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   208
lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   209
by fast
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   210
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   211
lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   212
by fast
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   213
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   214
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   215
  The set @{term "hyps p t"} is finite, and elements have the form
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   216
  @{term "#v"} or @{term "#v->Fls"}.
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   217
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   218
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   219
lemma hyps_finite: "finite(hyps p t)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   220
by (induct_tac "p", auto)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   221
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   222
lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   223
by (induct_tac "p", auto)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   224
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   225
lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   226
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   227
subsubsection {* Completeness theorem *}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   228
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   229
text {*
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   230
  Induction on the finite set of assumptions @{term "hyps p t0"}.  We
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   231
  may repeatedly subtract assumptions until none are left!
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   232
*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   233
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   234
lemma completeness_0_lemma:
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   235
    "{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p" 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   236
apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   237
 apply (simp add: sat_thms_p, safe)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   238
(*Case hyps p t-insert(#v,Y) |- p *)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   239
 apply (rule thms_excluded_middle_rule)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   240
  apply (rule insert_Diff_same [THEN weaken_left])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   241
  apply (erule spec)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   242
 apply (rule insert_Diff_subset2 [THEN weaken_left])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   243
 apply (rule hyps_Diff [THEN Diff_weaken_left])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   244
 apply (erule spec)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   245
(*Case hyps p t-insert(#v -> false,Y) |- p *)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   246
apply (rule thms_excluded_middle_rule)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   247
 apply (rule_tac [2] insert_Diff_same [THEN weaken_left])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   248
 apply (erule_tac [2] spec)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   249
apply (rule insert_Diff_subset2 [THEN weaken_left])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   250
apply (rule hyps_insert [THEN Diff_weaken_left])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   251
apply (erule spec)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   252
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   253
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   254
text{*The base case for completeness*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   255
lemma completeness_0:  "{} |= p ==> {} |- p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   256
apply (rule Diff_cancel [THEN subst])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   257
apply (erule completeness_0_lemma [THEN spec])
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   258
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   259
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   260
text{*A semantic analogue of the Deduction Theorem*}
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   261
lemma sat_imp: "insert p H |= q ==> H |= p->q"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   262
by (unfold sat_def, auto)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   263
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   264
theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   265
apply (erule finite_induct)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   266
apply (safe intro!: completeness_0)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   267
apply (drule sat_imp)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   268
apply (drule spec) 
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   269
apply (blast intro: weaken_left_insert [THEN thms.MP])  
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   270
done
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   271
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   272
theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   273
by (fast elim!: soundness completeness)
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 10759
diff changeset
   274
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   275
end
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   276