# HG changeset patch
# User wenzelm
# Date 978553469 -3600
# Node ID 4de3a0d3ae281f086193b6c4ec20a8daa385f250
# Parent  0deff01974963e48093252fb4b9f9e7029133497
recdef_tc;

diff -r 0deff0197496 -r 4de3a0d3ae28 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:23:50 2001 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:24:29 2001 +0100
@@ -29,20 +29,17 @@
       else if b s then while_aux (b, c, c s)
       else s)"
 
+recdef_tc while_aux_tc: while_aux
+  apply (rule wf_same_fst)
+  apply (rule wf_same_fst)
+  apply (simp add: wf_iff_no_infinite_down_chain)
+  apply blast
+  done
+
 constdefs
   while :: "('a => bool) => ('a => 'a) => 'a => 'a"
   "while b c s == while_aux (b, c, s)"
 
-ML_setup {*
-  goalw_cterm [] (cterm_of (sign_of (the_context ()))
-    (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
-  br wf_same_fst 1;
-  br wf_same_fst 1;
-  by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
-  by (Blast_tac 1);
-  qed "while_aux_tc";
-*} (* FIXME cannot access recdef tcs in Isar yet! *)
-
 lemma while_aux_unfold:
   "while_aux (b, c, s) =
     (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
diff -r 0deff0197496 -r 4de3a0d3ae28 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Jan 03 21:23:50 2001 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed Jan 03 21:24:29 2001 +0100
@@ -59,7 +59,7 @@
 "merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
 
 
-lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric];
+lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
 
 
 lemma pres_typeD:
@@ -206,26 +206,16 @@
 
 (** iter **)
 
-ML_setup {*
-let
-val thy = the_context ()
-val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
-in
-goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
-by (REPEAT(rtac wf_same_fst 1));
-by (split_all_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1);
-by (REPEAT(rtac wf_same_fst 1));
-by (rtac wf_lex_prod 1);
- by (rtac wf_finite_psubset 2);
-by (Clarify_tac 1);
-by (dtac (thm "semilatDorderI" RS (thm "acc_le_listI")) 1);
- by (assume_tac 1);
-by (rewrite_goals_tac [thm "acc_def",thm "lesssub_def"]);
-by (assume_tac 1);
-qed "iter_wf"
-end
-*}
+recdef_tc iter_wf: iter (1)
+  apply (rule wf_same_fst)+
+  apply (simp add: split_tupled_all lesssub_def)
+  apply (rule wf_lex_prod)
+   prefer 2
+   apply (rule wf_finite_psubset)
+  apply clarify
+  apply (drule (1) semilatDorderI [THEN acc_le_listI])
+  apply (simp only: acc_def lesssub_def)
+  done
 
 lemma inter_tc_lemma:  
   "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> 
@@ -243,27 +233,22 @@
   apply simp
   done
 
-ML_setup {*
-let
-val thy = the_context ()
-val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
-in
-goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc)); 
-by (asm_simp_tac (simpset() addsimps [same_fst_def,thm "pres_type_def"]) 1);
-by (clarify_tac (claset() delrules [disjCI]) 1);
-by (subgoal_tac "(@p. p:w) : w" 1);
- by (fast_tac (claset() addIs [someI]) 2);
-by (subgoal_tac "ss : list (size ss) A" 1);
- by (blast_tac (claset() addSIs [thm "listI"]) 2);
-by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
- by (blast_tac (claset() addDs [thm "boundedD"]) 2);
-by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() delsimps [thm "listE_length"]
-      addsimps [thm "decomp_propa",finite_psubset_def,thm "inter_tc_lemma",
-                bounded_nat_set_is_finite]) 1);
-qed "iter_tc"
-end
-*}
+recdef_tc iter_tc: iter (2)
+  apply (simp add: same_fst_def pres_type_def)
+  apply (clarify del: disjCI)
+  apply (subgoal_tac "(@p. p:w) : w")
+   prefer 2
+   apply (fast intro: someI)
+  apply (subgoal_tac "ss : list (size ss) A")
+   prefer 2
+   apply (blast intro!: listI)
+  apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
+   prefer 2
+   apply (blast dest: boundedD)
+  apply (rotate_tac 1)
+  apply (simp del: listE_length
+    add: decomp_propa finite_psubset_def inter_tc_lemma bounded_nat_set_is_finite)
+  done
 
 lemma iter_induct:
   "(!!A r f step succs ss w.