src/HOL/Induct/PropLog.thy

 datatype 'a pl =
   false |
   var 'a ("#_" [1000]) |
   imp "'a pl" "'a pl" (infixr "->" 90)
 
+
 subsection {* The proof system *}
 
-inductive
-  thms :: "['a pl set, 'a pl] => bool"  (infixl "|-" 50)
+inductive thms :: "['a pl set, 'a pl] => bool"  (infixl "|-" 50)
   for H :: "'a pl set"
-  where
-    H [intro]:  "p\<in>H ==> H |- p"
-  | K:          "H |- p->q->p"
-  | S:          "H |- (p->q->r) -> (p->q) -> p->r"
-  | DN:         "H |- ((p->false) -> false) -> p"
-  | MP:         "[| H |- p->q; H |- p |] ==> H |- q"
+where
+  H: "p\<in>H ==> H |- p"
+| K: "H |- p->q->p"
+| S: "H |- (p->q->r) -> (p->q) -> p->r"
+| DN: "H |- ((p->false) -> false) -> p"
+| MP: "[| H |- p->q; H |- p |] ==> H |- q"
+
 
 subsection {* The semantics *}
 
 subsubsection {* Semantics of propositional logic. *}
 
-primrec eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100) where
-            "tt[[false]] = False"
-|            "tt[[#v]]    = (v \<in> tt)"
-| eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
+primrec eval :: "['a set, 'a pl] => bool"  ("_[[_]]" [100,0] 100)
+where
+  "tt[[false]] = False"
+| "tt[[#v]] = (v \<in> tt)"
+| eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
 
 text {*
   A finite set of hypotheses from @{text t} and the @{text Var}s in
   @{text p}.
 *}
 
-primrec hyps  :: "['a pl, 'a set] => 'a pl set" where
+primrec hyps :: "['a pl, 'a set] => 'a pl set"
+where
   "hyps false  tt = {}"
 | "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
 | "hyps (p->q) tt = hyps p tt Un hyps q tt"
 
+
 subsubsection {* Logical consequence *}
 
 text {*
   For every valuation, if all elements of @{text H} are true then so
   is @{text p}.
 *}
 
-definition
-  sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50) where
-    "H |= p  =  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
+definition sat :: "['a pl set, 'a pl] => bool"  (infixl "|=" 50)
+  where "H |= p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
 
 
 subsection {* Proof theory of propositional logic *}
 
 lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"

 
 lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
   -- {* Order of premises is convenient with @{text THEN} *}
   by (erule thms_mono [THEN predicate1D])
 
-lemmas weaken_left_insert = subset_insertI [THEN weaken_left]
-
-lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
-lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
+lemma weaken_left_insert: "G |- p \<Longrightarrow> insert a G |- p"
+by (rule weaken_left) (rule subset_insertI)
+
+lemma weaken_left_Un1: "G |- p \<Longrightarrow> G \<union> B |- p"
+by (rule weaken_left) (rule Un_upper1)
+
+lemma weaken_left_Un2: "G |- p \<Longrightarrow> A \<union> G |- p"
+by (rule weaken_left) (rule Un_upper2)
 
 lemma weaken_right: "H |- q ==> H |- p->q"
 by (fast intro: thms.K thms.MP)
 
 

 done
 
 
 subsubsection {* The cut rule *}
 
-lemmas cut = deduction [THEN thms.MP]
-
-lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
-
-lemmas thms_notE = thms.MP [THEN thms_falseE]
+lemma cut: "insert p H |- q \<Longrightarrow> H |- p \<Longrightarrow> H |- q"
+by (rule thms.MP) (rule deduction)
+
+lemma thms_falseE: "H |- false \<Longrightarrow> H |- q"
+by (rule thms.MP, rule thms.DN) (rule weaken_right)
+
+lemma thms_notE: "H |- p -> false \<Longrightarrow> H |- p \<Longrightarrow> H |- q"
+by (rule thms_falseE) (rule thms.MP)
 
 
 subsubsection {* Soundness of the rules wrt truth-table semantics *}
 
 theorem soundness: "H |- p ==> H |= p"
-apply (unfold sat_def)
-apply (induct set: thms)
-apply auto
-done
+by (induct set: thms) (auto simp: sat_def)
+
 
 subsection {* Completeness *}
 
 subsubsection {* Towards the completeness proof *}
 

   The excluded middle in the form of an elimination rule.
 *}
 
 lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
 apply (rule deduction [THEN deduction])
-apply (rule thms.DN [THEN thms.MP], best)
+apply (rule thms.DN [THEN thms.MP], best intro: H)
 done
 
 lemma thms_excluded_middle_rule:
     "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q"
   -- {* Hard to prove directly because it requires cuts *}

 by (induct p) auto
 
 lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
 by (induct p) auto
 
-lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
+lemma Diff_weaken_left: "A \<subseteq> C \<Longrightarrow> A - B |- p \<Longrightarrow> C - B |- p"
+  by (rule Diff_mono [OF _ subset_refl, THEN weaken_left])
+
 
 subsubsection {* Completeness theorem *}
 
 text {*
   Induction on the finite set of assumptions @{term "hyps p t0"}.  We

 apply (erule completeness_0_lemma [THEN spec])
 done
 
 text{*A semantic analogue of the Deduction Theorem*}
 lemma sat_imp: "insert p H |= q ==> H |= p->q"
-by (unfold sat_def, auto)
+by (auto simp: sat_def)
 
 theorem completeness: "finite H ==> H |= p ==> H |- p"
 apply (induct arbitrary: p rule: finite_induct)
  apply (blast intro: completeness_0)
 apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])