src/HOL/Induct/PropLog.thy

--- a/src/HOL/Induct/PropLog.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Induct/PropLog.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -26,20 +26,15 @@
 
 subsection {* The proof system *}
 
-consts
-  thms  :: "'a pl set => 'a pl set"
-
-abbreviation
-  thm_rel :: "['a pl set, 'a pl] => bool"   (infixl "|-" 50) where
-  "H |- p == p \<in> thms H"
-
-inductive "thms(H)"
-  intros
-  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"
+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"
 
 subsection {* The semantics *}
 
@@ -80,9 +75,9 @@
 subsection {* Proof theory of propositional logic *}
 
 lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
-apply (unfold thms.defs )
-apply (rule lfp_mono)
-apply (assumption | rule basic_monos)+
+apply (rule predicate1I)
+apply (erule thms.induct)
+apply (auto intro: thms.intros)
 done
 
 lemma thms_I: "H |- p->p"
@@ -94,7 +89,7 @@
 
 lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
   -- {* Order of premises is convenient with @{text THEN} *}
-  by (erule thms_mono [THEN subsetD])
+  by (erule thms_mono [THEN predicate1D])
 
 lemmas weaken_left_insert = subset_insertI [THEN weaken_left]