recdef_tc;
authorwenzelm
Wed Jan 03 21:24:29 2001 +0100 (2001-01-03)
changeset 107744de3a0d3ae28
parent 10773 0deff0197496
child 10775 3a5e5657e41c
recdef_tc;
src/HOL/Library/While_Combinator.thy
src/HOL/MicroJava/BV/Kildall.thy
     1.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:23:50 2001 +0100
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Jan 03 21:24:29 2001 +0100
     1.3 @@ -29,20 +29,17 @@
     1.4        else if b s then while_aux (b, c, c s)
     1.5        else s)"
     1.6  
     1.7 +recdef_tc while_aux_tc: while_aux
     1.8 +  apply (rule wf_same_fst)
     1.9 +  apply (rule wf_same_fst)
    1.10 +  apply (simp add: wf_iff_no_infinite_down_chain)
    1.11 +  apply blast
    1.12 +  done
    1.13 +
    1.14  constdefs
    1.15    while :: "('a => bool) => ('a => 'a) => 'a => 'a"
    1.16    "while b c s == while_aux (b, c, s)"
    1.17  
    1.18 -ML_setup {*
    1.19 -  goalw_cterm [] (cterm_of (sign_of (the_context ()))
    1.20 -    (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
    1.21 -  br wf_same_fst 1;
    1.22 -  br wf_same_fst 1;
    1.23 -  by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
    1.24 -  by (Blast_tac 1);
    1.25 -  qed "while_aux_tc";
    1.26 -*} (* FIXME cannot access recdef tcs in Isar yet! *)
    1.27 -
    1.28  lemma while_aux_unfold:
    1.29    "while_aux (b, c, s) =
    1.30      (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))
     2.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Wed Jan 03 21:23:50 2001 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Wed Jan 03 21:24:29 2001 +0100
     2.3 @@ -59,7 +59,7 @@
     2.4  "merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
     2.5  
     2.6  
     2.7 -lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric];
     2.8 +lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric]
     2.9  
    2.10  
    2.11  lemma pres_typeD:
    2.12 @@ -206,26 +206,16 @@
    2.13  
    2.14  (** iter **)
    2.15  
    2.16 -ML_setup {*
    2.17 -let
    2.18 -val thy = the_context ()
    2.19 -val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
    2.20 -in
    2.21 -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
    2.22 -by (REPEAT(rtac wf_same_fst 1));
    2.23 -by (split_all_tac 1);
    2.24 -by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1);
    2.25 -by (REPEAT(rtac wf_same_fst 1));
    2.26 -by (rtac wf_lex_prod 1);
    2.27 - by (rtac wf_finite_psubset 2);
    2.28 -by (Clarify_tac 1);
    2.29 -by (dtac (thm "semilatDorderI" RS (thm "acc_le_listI")) 1);
    2.30 - by (assume_tac 1);
    2.31 -by (rewrite_goals_tac [thm "acc_def",thm "lesssub_def"]);
    2.32 -by (assume_tac 1);
    2.33 -qed "iter_wf"
    2.34 -end
    2.35 -*}
    2.36 +recdef_tc iter_wf: iter (1)
    2.37 +  apply (rule wf_same_fst)+
    2.38 +  apply (simp add: split_tupled_all lesssub_def)
    2.39 +  apply (rule wf_lex_prod)
    2.40 +   prefer 2
    2.41 +   apply (rule wf_finite_psubset)
    2.42 +  apply clarify
    2.43 +  apply (drule (1) semilatDorderI [THEN acc_le_listI])
    2.44 +  apply (simp only: acc_def lesssub_def)
    2.45 +  done
    2.46  
    2.47  lemma inter_tc_lemma:  
    2.48    "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> 
    2.49 @@ -243,27 +233,22 @@
    2.50    apply simp
    2.51    done
    2.52  
    2.53 -ML_setup {*
    2.54 -let
    2.55 -val thy = the_context ()
    2.56 -val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
    2.57 -in
    2.58 -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc)); 
    2.59 -by (asm_simp_tac (simpset() addsimps [same_fst_def,thm "pres_type_def"]) 1);
    2.60 -by (clarify_tac (claset() delrules [disjCI]) 1);
    2.61 -by (subgoal_tac "(@p. p:w) : w" 1);
    2.62 - by (fast_tac (claset() addIs [someI]) 2);
    2.63 -by (subgoal_tac "ss : list (size ss) A" 1);
    2.64 - by (blast_tac (claset() addSIs [thm "listI"]) 2);
    2.65 -by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
    2.66 - by (blast_tac (claset() addDs [thm "boundedD"]) 2);
    2.67 -by (rotate_tac 1 1);
    2.68 -by (asm_full_simp_tac (simpset() delsimps [thm "listE_length"]
    2.69 -      addsimps [thm "decomp_propa",finite_psubset_def,thm "inter_tc_lemma",
    2.70 -                bounded_nat_set_is_finite]) 1);
    2.71 -qed "iter_tc"
    2.72 -end
    2.73 -*}
    2.74 +recdef_tc iter_tc: iter (2)
    2.75 +  apply (simp add: same_fst_def pres_type_def)
    2.76 +  apply (clarify del: disjCI)
    2.77 +  apply (subgoal_tac "(@p. p:w) : w")
    2.78 +   prefer 2
    2.79 +   apply (fast intro: someI)
    2.80 +  apply (subgoal_tac "ss : list (size ss) A")
    2.81 +   prefer 2
    2.82 +   apply (blast intro!: listI)
    2.83 +  apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
    2.84 +   prefer 2
    2.85 +   apply (blast dest: boundedD)
    2.86 +  apply (rotate_tac 1)
    2.87 +  apply (simp del: listE_length
    2.88 +    add: decomp_propa finite_psubset_def inter_tc_lemma bounded_nat_set_is_finite)
    2.89 +  done
    2.90  
    2.91  lemma iter_induct:
    2.92    "(!!A r f step succs ss w.