author | haftmann |
Tue, 13 Jul 2010 16:00:56 +0200 | |
changeset 37804 | 0145e59c1f6c |
parent 36862 | 952b2b102a0a |
child 39246 | 9e58f0499f57 |
permissions | -rw-r--r-- |
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 |
Author: Tobias Nipkow |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
3 |
Copyright 1994 TU Muenchen & University of Cambridge |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
6 |
header {* Meta-theory of propositional logic *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
7 |
|
16417 | 8 |
theory PropLog imports Main begin |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
9 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
10 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
11 |
Datatype definition of propositional logic formulae and inductive |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
12 |
definition of the propositional tautologies. |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
13 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
14 |
Inductive definition of propositional logic. Soundness and |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
15 |
completeness w.r.t.\ truth-tables. |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
16 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
17 |
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
|
18 |
Fin(H)"} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
19 |
*} |
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 |
subsection {* The datatype of propositions *} |
5184 | 22 |
|
24824 | 23 |
datatype 'a pl = |
24 |
false | |
|
25 |
var 'a ("#_" [1000]) | |
|
26 |
imp "'a pl" "'a pl" (infixr "->" 90) |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
27 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
28 |
subsection {* The proof system *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
29 |
|
23746 | 30 |
inductive |
31 |
thms :: "['a pl set, 'a pl] => bool" (infixl "|-" 50) |
|
32 |
for H :: "'a pl set" |
|
33 |
where |
|
34 |
H [intro]: "p\<in>H ==> H |- p" |
|
35 |
| K: "H |- p->q->p" |
|
36 |
| S: "H |- (p->q->r) -> (p->q) -> p->r" |
|
37 |
| DN: "H |- ((p->false) -> false) -> p" |
|
38 |
| MP: "[| H |- p->q; H |- p |] ==> H |- q" |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
39 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
40 |
subsection {* The semantics *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
41 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
42 |
subsubsection {* Semantics of propositional logic. *} |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
43 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
44 |
consts |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
45 |
eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
46 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
47 |
primrec "tt[[false]] = False" |
18260 | 48 |
"tt[[#v]] = (v \<in> tt)" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
49 |
eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
50 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
51 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
52 |
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
|
53 |
@{text p}. |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
54 |
*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
55 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
56 |
consts |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
57 |
hyps :: "['a pl, 'a set] => 'a pl set" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
58 |
|
5184 | 59 |
primrec |
10759 | 60 |
"hyps false tt = {}" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
61 |
"hyps (#v) tt = {if v \<in> tt then #v else #v->false}" |
10759 | 62 |
"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
|
63 |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
64 |
subsubsection {* Logical consequence *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
65 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
66 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
67 |
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
|
68 |
is @{text p}. |
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 |
|
19736 | 71 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20503
diff
changeset
|
72 |
sat :: "['a pl set, 'a pl] => bool" (infixl "|=" 50) where |
19736 | 73 |
"H |= p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])" |
13075
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 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
76 |
subsection {* Proof theory of propositional logic *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
77 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
78 |
lemma thms_mono: "G<=H ==> thms(G) <= thms(H)" |
23746 | 79 |
apply (rule predicate1I) |
80 |
apply (erule thms.induct) |
|
81 |
apply (auto intro: thms.intros) |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
82 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
83 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
84 |
lemma thms_I: "H |- p->p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
85 |
-- {*Called @{text I} for Identity Combinator, not for Introduction. *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
86 |
by (best intro: thms.K thms.S thms.MP) |
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 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
89 |
subsubsection {* Weakening, left and right *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
90 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
91 |
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
|
92 |
-- {* Order of premises is convenient with @{text THEN} *} |
23746 | 93 |
by (erule thms_mono [THEN predicate1D]) |
13075
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 |
lemmas weaken_left_insert = subset_insertI [THEN weaken_left] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
96 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
97 |
lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
98 |
lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
99 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
100 |
lemma weaken_right: "H |- q ==> H |- p->q" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
101 |
by (fast intro: thms.K thms.MP) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
102 |
|
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 |
subsubsection {* The deduction theorem *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
105 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
106 |
theorem deduction: "insert p H |- q ==> H |- p->q" |
18260 | 107 |
apply (induct set: thms) |
108 |
apply (fast intro: thms_I thms.H thms.K thms.S thms.DN |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
109 |
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
|
110 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
111 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
112 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
113 |
subsubsection {* The cut rule *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
114 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
115 |
lemmas cut = deduction [THEN thms.MP] |
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 |
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
|
118 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
119 |
lemmas thms_notE = thms.MP [THEN thms_falseE, standard] |
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 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
122 |
subsubsection {* Soundness of the rules wrt truth-table semantics *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
123 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
124 |
theorem soundness: "H |- p ==> H |= p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
125 |
apply (unfold sat_def) |
18260 | 126 |
apply (induct set: thms) |
127 |
apply auto |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
128 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
129 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
130 |
subsection {* Completeness *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
131 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
132 |
subsubsection {* Towards the completeness proof *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
133 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
134 |
lemma false_imp: "H |- p->false ==> H |- p->q" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
135 |
apply (rule deduction) |
27034 | 136 |
apply (metis H insert_iff weaken_left_insert thms_notE) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
137 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
138 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
139 |
lemma imp_false: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
140 |
"[| H |- p; H |- q->false |] ==> H |- (p->q)->false" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
141 |
apply (rule deduction) |
27034 | 142 |
apply (metis H MP insert_iff weaken_left_insert) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
143 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
144 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
145 |
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
|
146 |
-- {* Typical example of strengthening the induction statement. *} |
18260 | 147 |
apply simp |
148 |
apply (induct p) |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
149 |
apply (simp_all add: thms_I thms.H) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
150 |
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
|
151 |
imp_false false_imp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
152 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
153 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
154 |
lemma sat_thms_p: "{} |= p ==> hyps p tt |- p" |
18260 | 155 |
-- {* Key lemma for completeness; yields a set of assumptions |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
156 |
satisfying @{text p} *} |
18260 | 157 |
apply (unfold sat_def) |
158 |
apply (drule spec, erule mp [THEN if_P, THEN subst], |
|
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
159 |
rule_tac [2] hyps_thms_if, simp) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
160 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
161 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
162 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
163 |
For proving certain theorems in our new propositional logic. |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
164 |
*} |
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 |
declare deduction [intro!] |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
167 |
declare thms.H [THEN thms.MP, intro] |
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 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
170 |
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
|
171 |
*} |
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 |
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
|
174 |
apply (rule deduction [THEN deduction]) |
18260 | 175 |
apply (rule thms.DN [THEN thms.MP], best) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
176 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
177 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
178 |
lemma thms_excluded_middle_rule: |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
179 |
"[| 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
|
180 |
-- {* Hard to prove directly because it requires cuts *} |
18260 | 181 |
by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
182 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
183 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
184 |
subsection{* Completeness -- lemmas for reducing the set of assumptions*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
185 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
186 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
187 |
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
|
188 |
"hyps p t - {#v} \<subseteq> hyps p (t-{v})"}. |
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 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
191 |
lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})" |
18260 | 192 |
by (induct p) auto |
13075
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 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
195 |
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
|
196 |
@{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
|
197 |
*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
198 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
199 |
lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})" |
18260 | 200 |
by (induct p) auto |
13075
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 |
text {* Two lemmas for use with @{text weaken_left} *} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
203 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
204 |
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
|
205 |
by fast |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
206 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
207 |
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
|
208 |
by fast |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
209 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
210 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
211 |
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
|
212 |
@{term "#v"} or @{term "#v->Fls"}. |
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 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
215 |
lemma hyps_finite: "finite(hyps p t)" |
18260 | 216 |
by (induct p) auto |
13075
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 |
lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})" |
18260 | 219 |
by (induct p) auto |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
220 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
221 |
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
|
222 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
223 |
subsubsection {* Completeness theorem *} |
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 |
text {* |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
226 |
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
|
227 |
may repeatedly subtract assumptions until none are left! |
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 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
230 |
lemma completeness_0_lemma: |
18260 | 231 |
"{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p" |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
232 |
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
|
233 |
apply (simp add: sat_thms_p, safe) |
16563 | 234 |
txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *} |
18260 | 235 |
apply (iprover intro: thms_excluded_middle_rule |
236 |
insert_Diff_same [THEN weaken_left] |
|
237 |
insert_Diff_subset2 [THEN weaken_left] |
|
16563 | 238 |
hyps_Diff [THEN Diff_weaken_left]) |
239 |
txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *} |
|
18260 | 240 |
apply (iprover intro: thms_excluded_middle_rule |
241 |
insert_Diff_same [THEN weaken_left] |
|
242 |
insert_Diff_subset2 [THEN weaken_left] |
|
16563 | 243 |
hyps_insert [THEN Diff_weaken_left]) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
244 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
245 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
246 |
text{*The base case for completeness*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
247 |
lemma completeness_0: "{} |= p ==> {} |- p" |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
248 |
apply (rule Diff_cancel [THEN subst]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
249 |
apply (erule completeness_0_lemma [THEN spec]) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
250 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
251 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
252 |
text{*A semantic analogue of the Deduction Theorem*} |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
253 |
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
|
254 |
by (unfold sat_def, auto) |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
255 |
|
18260 | 256 |
theorem completeness: "finite H ==> H |= p ==> H |- p" |
20503 | 257 |
apply (induct arbitrary: p rule: finite_induct) |
16563 | 258 |
apply (blast intro: completeness_0) |
17589 | 259 |
apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP]) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
260 |
done |
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
261 |
|
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
262 |
theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)" |
16563 | 263 |
by (blast intro: soundness completeness) |
13075
d3e1d554cd6d
conversion of some HOL/Induct proof scripts to Isar
paulson
parents:
10759
diff
changeset
|
264 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
265 |
end |