# HG changeset patch # User nipkow # Date 976696375 -3600 # Node ID 55f33da63366013f520d12f4467c9f8eea46a86e # Parent e6a4bb832b46a876fc20812183b24757df365d7c small mods. diff -r e6a4bb832b46 -r 55f33da63366 src/HOL/BCV/Kildall.ML --- a/src/HOL/BCV/Kildall.ML Wed Dec 13 09:30:59 2000 +0100 +++ b/src/HOL/BCV/Kildall.ML Wed Dec 13 09:32:55 2000 +0100 @@ -152,10 +152,10 @@ val [iter_wf,iter_tc] = iter.tcs; goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf)); -by (REPEAT(rtac wf_same_fstI 1)); +by (REPEAT(rtac wf_same_fst 1)); by (split_all_tac 1); by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1); -by (REPEAT(rtac wf_same_fstI 1)); +by (REPEAT(rtac wf_same_fst 1)); by (rtac wf_lex_prod 1); by (rtac wf_finite_psubset 2); (* FIXME *) by (Clarify_tac 1); diff -r e6a4bb832b46 -r 55f33da63366 src/HOL/Lambda/ListBeta.thy --- a/src/HOL/Lambda/ListBeta.thy Wed Dec 13 09:30:59 2000 +0100 +++ b/src/HOL/Lambda/ListBeta.thy Wed Dec 13 09:32:55 2000 +0100 @@ -47,23 +47,23 @@ apply (case_tac r) apply simp apply (simp add: App_eq_foldl_conv) - apply (split (asm) split_if_asm) + apply (split split_if_asm) apply simp apply blast apply simp apply (simp add: App_eq_foldl_conv) - apply (split (asm) split_if_asm) + apply (split split_if_asm) apply simp apply simp apply (clarify del: disjCI) apply (drule App_eq_foldl_conv [THEN iffD1]) - apply (split (asm) split_if_asm) + apply (split split_if_asm) apply simp apply blast apply (force intro: disjI1 [THEN append_step1I]) apply (clarify del: disjCI) apply (drule App_eq_foldl_conv [THEN iffD1]) - apply (split (asm) split_if_asm) + apply (split split_if_asm) apply simp apply blast apply (auto 0 3 intro: disjI2 [THEN append_step1I]) diff -r e6a4bb832b46 -r 55f33da63366 src/HOL/Library/While_Combinator.thy --- a/src/HOL/Library/While_Combinator.thy Wed Dec 13 09:30:59 2000 +0100 +++ b/src/HOL/Library/While_Combinator.thy Wed Dec 13 09:32:55 2000 +0100 @@ -36,8 +36,8 @@ ML_setup {* goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux")))); - br wf_same_fstI 1; - br wf_same_fstI 1; + 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"; @@ -74,7 +74,7 @@ The proof rule for @{term while}, where @{term P} is the invariant. *} -theorem while_rule [rule_format]: +theorem while_rule_lemma[rule_format]: "(!!s. P s ==> b s ==> P (c s)) ==> (!!s. P s ==> \ b s ==> Q s) ==> wf {(t, s). P s \ b s \ t = c s} ==> @@ -91,31 +91,19 @@ done qed +theorem while_rule: + "\ P s; \s. \ P s; b s \ \ P(c s); + \s.\ P s; \ b s \ \ Q s; + wf r; \s. \ P s; b s \ \ (c s,s) \ r \ \ + Q (while b c s)" +apply (rule while_rule_lemma) +prefer 4 apply assumption +apply blast +apply blast +apply(erule wf_subset) +apply blast +done + hide const while_aux -text {* - \medskip An application: computation of the @{term lfp} on finite - sets via iteration. -*} - -theorem lfp_conv_while: - "mono f ==> finite U ==> f U = U ==> - lfp f = fst (while (\(A, fA). A \ fA) (\(A, fA). (fA, f fA)) ({}, f {}))" - apply (rule_tac P = - "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" in while_rule) - apply (subst lfp_unfold) - apply assumption - apply clarsimp - apply (blast dest: monoD) - apply (fastsimp intro!: lfp_lowerbound) - apply (rule_tac r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \ - inv_image finite_psubset (op - U o fst)" in wf_subset) - apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) - apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le) - apply (blast intro!: finite_Diff dest: monoD) - apply (subst lfp_unfold) - apply assumption - apply (simp add: monoD) - done - end diff -r e6a4bb832b46 -r 55f33da63366 src/HOL/Library/While_Combinator_Example.thy --- a/src/HOL/Library/While_Combinator_Example.thy Wed Dec 13 09:30:59 2000 +0100 +++ b/src/HOL/Library/While_Combinator_Example.thy Wed Dec 13 09:32:55 2000 +0100 @@ -1,9 +1,32 @@ - header {* \title{} *} theory While_Combinator_Example = While_Combinator: text {* + \medskip An application: computation of the @{term lfp} on finite + sets via iteration. +*} + +theorem lfp_conv_while: + "mono f ==> finite U ==> f U = U ==> + lfp f = fst (while (\(A, fA). A \ fA) (\(A, fA). (fA, f fA)) ({}, f {}))" +apply (rule_tac P = "\(A, B). (A \ U \ B = f A \ A \ B \ B \ lfp f)" and + r = "((Pow U <*> UNIV) <*> (Pow U <*> UNIV)) \ + inv_image finite_psubset (op - U o fst)" in while_rule) + apply (subst lfp_unfold) + apply assumption + apply (simp add: monoD) + apply (subst lfp_unfold) + apply assumption + apply clarsimp + apply (blast dest: monoD) + apply (fastsimp intro!: lfp_lowerbound) + apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) +apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le) +apply (blast intro!: finite_Diff dest: monoD) +done + +text {* An example of using the @{term while} combinator. *} diff -r e6a4bb832b46 -r 55f33da63366 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Wed Dec 13 09:30:59 2000 +0100 +++ b/src/HOL/Recdef.thy Wed Dec 13 09:32:55 2000 +0100 @@ -39,6 +39,7 @@ wf_inv_image wf_measure wf_pred_nat + wf_same_fst wf_empty end diff -r e6a4bb832b46 -r 55f33da63366 src/HOL/Wellfounded_Relations.ML --- a/src/HOL/Wellfounded_Relations.ML Wed Dec 13 09:30:59 2000 +0100 +++ b/src/HOL/Wellfounded_Relations.ML Wed Dec 13 09:32:55 2000 +0100 @@ -223,4 +223,4 @@ by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]); by(Blast_tac 1); by(blast_tac (claset() addIs prems) 1); -qed "wf_same_fstI"; +qed "wf_same_fst";