# HG changeset patch
# User wenzelm
# Date 1415702873 -3600
# Node ID 2a683fb686fd01107a6fa9c7deb22320f14a1d4a
# Parent  5b026cfc5f04649ff1463338f2552f842465ebeb
more Isar proof methods;

diff -r 5b026cfc5f04 -r 2a683fb686fd src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/LCF.thy	Tue Nov 11 11:47:53 2014 +0100
@@ -318,15 +318,15 @@
   adm_not_free adm_eq adm_less adm_not_less
   adm_not_eq_tr adm_conj adm_disj adm_imp adm_all
 
-
-ML {*
-  fun induct_tac ctxt v i =
-    res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
-    REPEAT (resolve_tac @{thms adm_lemmas} i)
+method_setup induct = {*
+  Scan.lift Args.name >> (fn v => fn ctxt =>
+    SIMPLE_METHOD' (fn i =>
+      res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN
+      REPEAT (resolve_tac @{thms adm_lemmas} i)))
 *}
 
 lemma least_FIX: "f(p) = p ==> FIX(f) << p"
-  apply (tactic {* induct_tac @{context} "f" 1 *})
+  apply (induct f)
   apply (rule minimal)
   apply (intro strip)
   apply (erule subst)
diff -r 5b026cfc5f04 -r 2a683fb686fd src/LCF/ex/Ex1.thy
--- a/src/LCF/ex/Ex1.thy	Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex1.thy	Tue Nov 11 11:47:53 2014 +0100
@@ -28,7 +28,7 @@
   done
 
 lemma H_idemp_lemma: "ALL x. H(FIX(K,x)) = FIX(K,x)"
-  apply (tactic {* induct_tac @{context} "K" 1 *})
+  apply (induct K)
   apply simp
   apply (simp split: COND_cases_iff)
   apply (intro strip)
diff -r 5b026cfc5f04 -r 2a683fb686fd src/LCF/ex/Ex2.thy
--- a/src/LCF/ex/Ex2.thy	Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex2.thy	Tue Nov 11 11:47:53 2014 +0100
@@ -19,7 +19,7 @@
 
 lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))"
   apply (simplesubst H)
-  apply (tactic {* induct_tac @{context} "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *})
+  apply (induct "K:: ('a=>'b=>'b) => ('a=>'b=>'b)")
   apply simp
   apply (simp split: COND_cases_iff)
   done
diff -r 5b026cfc5f04 -r 2a683fb686fd src/LCF/ex/Ex3.thy
--- a/src/LCF/ex/Ex3.thy	Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex3.thy	Tue Nov 11 11:47:53 2014 +0100
@@ -14,7 +14,7 @@
 declare p_strict [simp] p_s [simp]
 
 lemma example: "p(FIX(s),y) = FIX(s)"
-  apply (tactic {* induct_tac @{context} "s" 1 *})
+  apply (induct s)
   apply simp
   apply simp
   done
diff -r 5b026cfc5f04 -r 2a683fb686fd src/LCF/ex/Ex4.thy
--- a/src/LCF/ex/Ex4.thy	Tue Nov 11 11:41:58 2014 +0100
+++ b/src/LCF/ex/Ex4.thy	Tue Nov 11 11:47:53 2014 +0100
@@ -10,7 +10,7 @@
   shows "FIX(f)=p"
   apply (unfold eq_def)
   apply (rule conjI)
-  apply (tactic {* induct_tac @{context} "f" 1 *})
+  apply (induct f)
   apply (rule minimal)
   apply (intro strip)
   apply (rule less_trans)