small mods.
authornipkow
Wed Dec 13 09:32:55 2000 +0100 (2000-12-13)
changeset 1065355f33da63366
parent 10652 e6a4bb832b46
child 10654 458068404143
small mods.
src/HOL/BCV/Kildall.ML
src/HOL/Lambda/ListBeta.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Library/While_Combinator_Example.thy
src/HOL/Recdef.thy
src/HOL/Wellfounded_Relations.ML
     1.1 --- a/src/HOL/BCV/Kildall.ML	Wed Dec 13 09:30:59 2000 +0100
     1.2 +++ b/src/HOL/BCV/Kildall.ML	Wed Dec 13 09:32:55 2000 +0100
     1.3 @@ -152,10 +152,10 @@
     1.4  val [iter_wf,iter_tc] = iter.tcs;
     1.5  
     1.6  goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
     1.7 -by (REPEAT(rtac wf_same_fstI 1));
     1.8 +by (REPEAT(rtac wf_same_fst 1));
     1.9  by (split_all_tac 1);
    1.10  by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
    1.11 -by (REPEAT(rtac wf_same_fstI 1));
    1.12 +by (REPEAT(rtac wf_same_fst 1));
    1.13  by (rtac wf_lex_prod 1);
    1.14   by (rtac wf_finite_psubset 2); (* FIXME *)
    1.15  by (Clarify_tac 1);
     2.1 --- a/src/HOL/Lambda/ListBeta.thy	Wed Dec 13 09:30:59 2000 +0100
     2.2 +++ b/src/HOL/Lambda/ListBeta.thy	Wed Dec 13 09:32:55 2000 +0100
     2.3 @@ -47,23 +47,23 @@
     2.4       apply (case_tac r)
     2.5         apply simp
     2.6        apply (simp add: App_eq_foldl_conv)
     2.7 -      apply (split (asm) split_if_asm)
     2.8 +      apply (split split_if_asm)
     2.9         apply simp
    2.10         apply blast
    2.11        apply simp
    2.12       apply (simp add: App_eq_foldl_conv)
    2.13 -     apply (split (asm) split_if_asm)
    2.14 +     apply (split split_if_asm)
    2.15        apply simp
    2.16       apply simp
    2.17      apply (clarify del: disjCI)
    2.18      apply (drule App_eq_foldl_conv [THEN iffD1])
    2.19 -    apply (split (asm) split_if_asm)
    2.20 +    apply (split split_if_asm)
    2.21       apply simp
    2.22       apply blast
    2.23      apply (force intro: disjI1 [THEN append_step1I])
    2.24     apply (clarify del: disjCI)
    2.25     apply (drule App_eq_foldl_conv [THEN iffD1])
    2.26 -   apply (split (asm) split_if_asm)
    2.27 +   apply (split split_if_asm)
    2.28      apply simp
    2.29      apply blast
    2.30     apply (auto 0 3 intro: disjI2 [THEN append_step1I])
     3.1 --- a/src/HOL/Library/While_Combinator.thy	Wed Dec 13 09:30:59 2000 +0100
     3.2 +++ b/src/HOL/Library/While_Combinator.thy	Wed Dec 13 09:32:55 2000 +0100
     3.3 @@ -36,8 +36,8 @@
     3.4  ML_setup {*
     3.5    goalw_cterm [] (cterm_of (sign_of (the_context ()))
     3.6      (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));
     3.7 -  br wf_same_fstI 1;
     3.8 -  br wf_same_fstI 1;
     3.9 +  br wf_same_fst 1;
    3.10 +  br wf_same_fst 1;
    3.11    by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);
    3.12    by (Blast_tac 1);
    3.13    qed "while_aux_tc";
    3.14 @@ -74,7 +74,7 @@
    3.15   The proof rule for @{term while}, where @{term P} is the invariant.
    3.16  *}
    3.17  
    3.18 -theorem while_rule [rule_format]:
    3.19 +theorem while_rule_lemma[rule_format]:
    3.20    "(!!s. P s ==> b s ==> P (c s)) ==>
    3.21      (!!s. P s ==> \<not> b s ==> Q s) ==>
    3.22      wf {(t, s). P s \<and> b s \<and> t = c s} ==>
    3.23 @@ -91,31 +91,19 @@
    3.24      done
    3.25  qed
    3.26  
    3.27 +theorem while_rule:
    3.28 +  "\<lbrakk> P s; \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> P(c s);
    3.29 +    \<And>s.\<lbrakk> P s; \<not> b s \<rbrakk> \<Longrightarrow> Q s;
    3.30 +    wf r;  \<And>s. \<lbrakk> P s; b s \<rbrakk> \<Longrightarrow> (c s,s) \<in> r \<rbrakk> \<Longrightarrow>
    3.31 +    Q (while b c s)"
    3.32 +apply (rule while_rule_lemma)
    3.33 +prefer 4 apply assumption
    3.34 +apply blast
    3.35 +apply blast
    3.36 +apply(erule wf_subset)
    3.37 +apply blast
    3.38 +done
    3.39 +
    3.40  hide const while_aux
    3.41  
    3.42 -text {*
    3.43 - \medskip An application: computation of the @{term lfp} on finite
    3.44 - sets via iteration.
    3.45 -*}
    3.46 -
    3.47 -theorem lfp_conv_while:
    3.48 -  "mono f ==> finite U ==> f U = U ==>
    3.49 -    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
    3.50 -  apply (rule_tac P =
    3.51 -      "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" in while_rule)
    3.52 -     apply (subst lfp_unfold)
    3.53 -      apply assumption
    3.54 -     apply clarsimp
    3.55 -     apply (blast dest: monoD)
    3.56 -    apply (fastsimp intro!: lfp_lowerbound)
    3.57 -   apply (rule_tac r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
    3.58 -       inv_image finite_psubset (op - U o fst)" in wf_subset)
    3.59 -    apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
    3.60 -   apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
    3.61 -   apply (blast intro!: finite_Diff dest: monoD)
    3.62 -  apply (subst lfp_unfold)
    3.63 -   apply assumption
    3.64 -  apply (simp add: monoD)
    3.65 -  done
    3.66 -
    3.67  end
     4.1 --- a/src/HOL/Library/While_Combinator_Example.thy	Wed Dec 13 09:30:59 2000 +0100
     4.2 +++ b/src/HOL/Library/While_Combinator_Example.thy	Wed Dec 13 09:32:55 2000 +0100
     4.3 @@ -1,9 +1,32 @@
     4.4 -
     4.5  header {* \title{} *}
     4.6  
     4.7  theory While_Combinator_Example = While_Combinator:
     4.8  
     4.9  text {*
    4.10 + \medskip An application: computation of the @{term lfp} on finite
    4.11 + sets via iteration.
    4.12 +*}
    4.13 +
    4.14 +theorem lfp_conv_while:
    4.15 +  "mono f ==> finite U ==> f U = U ==>
    4.16 +    lfp f = fst (while (\<lambda>(A, fA). A \<noteq> fA) (\<lambda>(A, fA). (fA, f fA)) ({}, f {}))"
    4.17 +apply (rule_tac P = "\<lambda>(A, B). (A \<subseteq> U \<and> B = f A \<and> A \<subseteq> B \<and> B \<subseteq> lfp f)" and
    4.18 +                r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \<inter>
    4.19 +                     inv_image finite_psubset (op - U o fst)" in while_rule)
    4.20 +   apply (subst lfp_unfold)
    4.21 +    apply assumption
    4.22 +   apply (simp add: monoD)
    4.23 +  apply (subst lfp_unfold)
    4.24 +   apply assumption
    4.25 +  apply clarsimp
    4.26 +  apply (blast dest: monoD)
    4.27 + apply (fastsimp intro!: lfp_lowerbound)
    4.28 + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
    4.29 +apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le)
    4.30 +apply (blast intro!: finite_Diff dest: monoD)
    4.31 +done
    4.32 +
    4.33 +text {*
    4.34   An example of using the @{term while} combinator.
    4.35  *}
    4.36  
     5.1 --- a/src/HOL/Recdef.thy	Wed Dec 13 09:30:59 2000 +0100
     5.2 +++ b/src/HOL/Recdef.thy	Wed Dec 13 09:32:55 2000 +0100
     5.3 @@ -39,6 +39,7 @@
     5.4    wf_inv_image
     5.5    wf_measure
     5.6    wf_pred_nat
     5.7 +  wf_same_fst
     5.8    wf_empty
     5.9  
    5.10  end
     6.1 --- a/src/HOL/Wellfounded_Relations.ML	Wed Dec 13 09:30:59 2000 +0100
     6.2 +++ b/src/HOL/Wellfounded_Relations.ML	Wed Dec 13 09:32:55 2000 +0100
     6.3 @@ -223,4 +223,4 @@
     6.4   by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
     6.5   by(Blast_tac 1);
     6.6  by(blast_tac (claset() addIs prems) 1);
     6.7 -qed "wf_same_fstI";
     6.8 +qed "wf_same_fst";