# HG changeset patch # User paulson # Date 1046959718 -3600 # Node ID f6923453953a293ec8d0f5cba37ddfa80874420c # Parent 6d1bb3059818ec1f67c182f99ca8434a4cfb4322 new UNITY examples theory diff -r 6d1bb3059818 -r f6923453953a src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Mar 06 15:03:16 2003 +0100 +++ b/src/HOL/IsaMakefile Thu Mar 06 15:08:38 2003 +0100 @@ -398,7 +398,7 @@ UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \ UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \ UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \ - UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy \ + UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ UNITY/Comp/TimerArray.thy @$(ISATOOL) usedir $(OUT)/HOL UNITY diff -r 6d1bb3059818 -r f6923453953a src/HOL/UNITY/Comp/Progress.thy --- a/src/HOL/UNITY/Comp/Progress.thy Thu Mar 06 15:03:16 2003 +0100 +++ b/src/HOL/UNITY/Comp/Progress.thy Thu Mar 06 15:08:38 2003 +0100 @@ -10,15 +10,6 @@ theory Progress = UNITY_Main: - - -(*????????????????Int*) -lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" -by simp - - - - subsection {*The Composition of Two Single-Assignment Programs*} text{*Thesis Section 4.4.2*} diff -r 6d1bb3059818 -r f6923453953a src/HOL/UNITY/Transformers.thy --- a/src/HOL/UNITY/Transformers.thy Thu Mar 06 15:03:16 2003 +0100 +++ b/src/HOL/UNITY/Transformers.thy Thu Mar 06 15:08:38 2003 +0100 @@ -44,6 +44,10 @@ lemma wp_Id [simp]: "wp Id B = B" by (simp add: wp_def) +lemma wp_totalize_act: + "wp (totalize_act act) B = (wp act B \ Domain act) \ (B - Domain act)" +by (simp add: wp_def totalize_act_def, blast) + lemma awp_Int_eq: "awp F (A\B) = awp F A \ awp F B" by (simp add: awp_def wp_def, blast) @@ -164,8 +168,7 @@ lemma leadsTo_imp_wens_set: "F \ A leadsTo B ==> \C \ wens_set F B. A \ C" apply (erule leadsTo_induct_pre) - apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) - apply clarify + apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens, clarify) apply (drule ensures_weaken_R, assumption) apply (blast dest!: ensures_imp_wens intro: wens_set.Wens) apply (case_tac "S={}") @@ -236,8 +239,7 @@ apply (rule_tac B = "wens (F\G) act (T\X)" in subset_trans) prefer 2 apply (blast intro!: wens_mono) apply (subst wens_Int_eq, assumption+) -apply (rule subset_wens_Join [of _ T]) - apply simp +apply (rule subset_wens_Join [of _ T], simp) apply blast apply (subgoal_tac "T \ wens F act (T\X) \ T\X = T \ wens F act X") prefer 2 @@ -274,8 +276,7 @@ apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) apply (rule wens_Union [THEN bexE]) apply (rule awpF) - apply (erule awpG) - apply assumption + apply (erule awpG, assumption) apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L]) done @@ -334,10 +335,13 @@ lemma atMost_nat_nonempty: "atMost (k::nat) \ {}" by force +lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B" +by (simp add: wens_single_finite_def) + lemma wens_single_finite_Suc: "single_valued act ==> wens_single_finite act B (Suc k) = - wens_single_finite act B k \ wp act (wens_single_finite act B k) " + wens_single_finite act B k \ wp act (wens_single_finite act B k)" apply (simp add: wens_single_finite_def image_def wp_UN_eq [OF _ atMost_nat_nonempty]) apply (force elim!: le_SucE) @@ -350,6 +354,12 @@ (wens_single_finite act B k)" by (simp add: wens_single_finite_Suc wens_single_eq) +lemma def_wens_single_finite_Suc_eq_wens: + "[|F = mk_program (init, {act}, allowed); single_valued act|] + ==> wens_single_finite act B (Suc k) = + wens F act (wens_single_finite act B k)" +by (simp add: wens_single_finite_Suc_eq_wens) + lemma wens_single_finite_Un_eq: "single_valued act ==> wens_single_finite act B k \ wp act (wens_single_finite act B k) @@ -377,8 +387,9 @@ lemma subset_wens_single_finite: "[|W \ wens_single_finite act B ` (atMost k); single_valued act; W\{}|] ==> \m. \W = wens_single_finite act B m" -apply (induct k) - apply (simp, blast) +apply (induct k) + apply (rule_tac x=0 in exI, simp) + apply blast apply (auto simp add: atMost_Suc) apply (case_tac "wens_single_finite act B (Suc n) \ W") prefer 2 apply blast @@ -398,11 +409,10 @@ apply (case_tac "wens_single act B \ W") apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) apply (simp add: wens_single_eq_Union) -apply (rule equalityI) - apply blast +apply (rule equalityI, blast) apply (simp add: UN_subset_iff, clarify) apply (subgoal_tac "\y\W. \n. y = wens_single_finite act B n & i\n") - apply (blast intro: wens_single_finite_mono [THEN subsetD] ) + apply (blast intro: wens_single_finite_mono [THEN subsetD]) apply (drule_tac x=i in spec) apply (force simp add: atMost_def) done @@ -447,12 +457,12 @@ text{*Theorem (4.29)*} theorem wens_set_single_eq: - "single_valued act - ==> wens_set (mk_program (init, {act}, allowed)) B = - insert (wens_single act B) (range (wens_single_finite act B))" + "[|F = mk_program (init, {act}, allowed); single_valued act|] + ==> wens_set F B = + insert (wens_single act B) (range (wens_single_finite act B))" apply (rule equalityI) -apply (erule wens_set_subset_single) -apply (erule single_subset_wens_set) + apply (simp add: wens_set_subset_single) +apply (erule ssubst, erule single_subset_wens_set) done end diff -r 6d1bb3059818 -r f6923453953a src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Thu Mar 06 15:03:16 2003 +0100 +++ b/src/HOL/UNITY/UNITY_Main.thy Thu Mar 06 15:08:38 2003 +0100 @@ -6,7 +6,7 @@ header{*Comprehensive UNITY Theory*} -theory UNITY_Main = Detects + PPROD + Follows +theory UNITY_Main = Detects + PPROD + Follows + Transformers files "UNITY_tactics.ML": method_setup constrains = {*