Isabelle2016-1: fix miscellaneous proofs
This commit is contained in:
Matthew Brecknell
parent
c7d2a8bb97
commit
bd94f7907e
|
|
@ -64,6 +64,7 @@ theorem spec_refine:
|
|||
THEN_ALL_NEW simp_tac @{simpset}
|
||||
THEN_ALL_NEW K no_tac)) *})
|
||||
*)
|
||||
apply (rule bij_id[simplified id_def])+
|
||||
done (* Woo! *)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -634,65 +634,63 @@ proof -
|
|||
apply (rename_tac s' d)
|
||||
apply (clarsimp simp: Let_def)
|
||||
apply (safe, simp_all add: invs_no_cicd'_max_CurDomain)
|
||||
(*12 subgoals *)
|
||||
apply (drule invs_no_cicd'_queues)
|
||||
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp signed_word_log2)
|
||||
apply (simp add: rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
|
||||
apply (case_tac queue, simp)
|
||||
apply (clarsimp simp: tcb_queue_relation'_def cready_queues_index_to_C_def
|
||||
numPriorities_def l1IndexToPrio_def)
|
||||
apply (erule trans[rotated])
|
||||
apply (subst unat_of_nat_shiftl_or_8_32)
|
||||
apply (clarsimp simp: wordRadix_def)
|
||||
apply (fastforce dest: ksReadyQueuesL1Bitmap_word_log2_max
|
||||
simp: numPriorities_def wordBits_def word_size)
|
||||
apply (drule_tac s=s in ksReadyQueuesL1Bitmap_word_log2_max, assumption)
|
||||
apply (rule order_less_le_trans[OF word_log2_max_word32] ; simp)
|
||||
(*10 subgoals *)
|
||||
apply (drule invs_no_cicd'_queues)
|
||||
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp signed_word_log2)
|
||||
apply (simp add: rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
|
||||
apply (case_tac queue, simp)
|
||||
apply (clarsimp simp: tcb_queue_relation'_def cready_queues_index_to_C_def
|
||||
numPriorities_def l1IndexToPrio_def)
|
||||
apply (erule trans[rotated])
|
||||
apply (subst unat_of_nat_shiftl_or_8_32)
|
||||
apply (clarsimp simp: wordRadix_def)
|
||||
apply (fastforce dest: ksReadyQueuesL1Bitmap_word_log2_max
|
||||
simp: numPriorities_def wordBits_def word_size)
|
||||
apply (drule_tac s=s in ksReadyQueuesL1Bitmap_word_log2_max, assumption)
|
||||
apply (rule order_less_le_trans[OF word_log2_max_word32] ; simp)
|
||||
|
||||
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
|
||||
apply (frule (1) lookupBitmapPriority_le_maxPriority)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
apply (simp add: unat_lookupBitmapPriority_32)
|
||||
apply (subst unat_add_lem')
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
|
||||
apply (rename_tac \<sigma>)
|
||||
apply (drule invs_no_cicd'_queues)
|
||||
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
|
||||
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
|
||||
apply (frule (1) lookupBitmapPriority_le_maxPriority)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt unat_lookupBitmapPriority_32)
|
||||
apply (subst unat_add_lem')
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
|
||||
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
|
||||
apply (frule (1) lookupBitmapPriority_le_maxPriority)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
apply (simp add: unat_lookupBitmapPriority_32)
|
||||
apply (subst unat_add_lem')
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
|
||||
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (rule order_le_less_trans)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
|
||||
apply (simp add: field_simps)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
|
||||
apply (fastforce dest!: invs_no_cicd'_queues
|
||||
simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp
|
||||
signed_word_log2)
|
||||
apply (rename_tac \<sigma>)
|
||||
apply (drule invs_no_cicd'_queues)
|
||||
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
|
||||
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
|
||||
apply (frule (1) lookupBitmapPriority_le_maxPriority)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt unat_lookupBitmapPriority_32)
|
||||
apply (subst unat_add_lem')
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
|
||||
apply (simp add: word_less_nat_alt word_le_nat_alt)
|
||||
|
||||
apply (rename_tac \<sigma>)
|
||||
apply (drule invs_no_cicd'_queues)
|
||||
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
|
||||
apply (drule word_log2_nth_same)
|
||||
apply (drule bitmapQ_no_L1_orphansD[rotated])
|
||||
apply (simp add: valid_queues_def)
|
||||
apply (fastforce intro!: cguard_UNIV word_of_nat_less
|
||||
simp: numPriorities_def wordBits_def word_size)
|
||||
apply (fastforce simp: field_simps)
|
||||
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (rule order_le_less_trans)
|
||||
apply (simp add: word_le_nat_alt)
|
||||
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
|
||||
|
||||
apply (fastforce dest!: invs_no_cicd'_queues
|
||||
simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp
|
||||
signed_word_log2)
|
||||
|
||||
apply (rename_tac \<sigma>)
|
||||
apply (drule invs_no_cicd'_queues)
|
||||
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
|
||||
apply (drule word_log2_nth_same)
|
||||
apply (drule bitmapQ_no_L1_orphansD[rotated])
|
||||
apply (simp add: valid_queues_def)
|
||||
apply (fastforce intro!: cguard_UNIV word_of_nat_less
|
||||
simp: numPriorities_def wordBits_def word_size)
|
||||
apply (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD[rotated] invs_no_cicd'_queues
|
||||
simp: valid_queues_def)
|
||||
apply (clarsimp dest!: invs_no_cicd'_queues simp add: valid_queues_def)
|
||||
|
|
|
|||
|
|
@ -901,7 +901,6 @@ shows "evalMonad (f) (machine_state sa) =
|
|||
apply (clarsimp simp:image_def)
|
||||
apply (rule iffI)
|
||||
apply clarsimp
|
||||
apply (rule_tac x = "(a,b)" in bexI)
|
||||
using assms
|
||||
apply (clarsimp simp:empty_when_fail_def weak_det_spec_def no_fail_def)
|
||||
apply (drule_tac x = "machine_state sa" in spec)
|
||||
|
|
|
|||
|
|
@ -40,8 +40,7 @@ lemma exec_transformed_valid_def:
|
|||
apply (erule allE, erule (1) impE)
|
||||
apply (case_tac "M s")
|
||||
apply (erule_tac allE, erule impE)
|
||||
apply (auto intro!: exI)
|
||||
done
|
||||
by (auto intro!: exI) fastforce
|
||||
|
||||
lemma exec_transformed_wp [wp]:
|
||||
"\<lbrace> \<lambda>s. \<exists>s'. (s', s) \<in> sr \<and> P s' \<rbrace> M \<lbrace> \<lambda>r s. \<forall>s'. (s', s) \<in> sr \<longrightarrow> Q r s' \<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> exec_transformed sr M \<lbrace> Q \<rbrace>"
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ lemma factorial'_correct_old: "m > unat n \<longrightarrow> factorial' m n s = S
|
|||
apply (clarsimp split: option.splits)
|
||||
apply (intro conjI impI)
|
||||
apply unat_arith
|
||||
apply (metis (hide_lams, no_types) Nat.add_0_right Nat.le_iff_add Suc_eq_plus1_left Suc_pred factorial.factorial'_terminates_old less_nat_zero_code nat_add_left_cancel_less nat_less_le unatSuc)
|
||||
apply (metis (hide_lams, no_types) Nat.add_0_right le_iff_add Suc_eq_plus1_left Suc_pred factorial.factorial'_terminates_old less_nat_zero_code nat_add_left_cancel_less nat_less_le)
|
||||
apply (unat_arith, force)
|
||||
done
|
||||
|
||||
|
|
|
|||
|
|
@ -43,12 +43,9 @@ lemma gcd_wp [wp]:
|
|||
and M="\<lambda>((a', b'), s). a'"])
|
||||
|
||||
(* Solve using weakest-precondition. *)
|
||||
apply wp
|
||||
apply clarsimp
|
||||
apply (metis gcd_commute_nat gcd_red_nat)
|
||||
apply clarsimp
|
||||
apply clarsimp
|
||||
done
|
||||
apply (wp; clarsimp)
|
||||
apply (metis gcd.commute gcd_red_nat)
|
||||
using gt_or_eq_0 by fastforce
|
||||
|
||||
lemma monad_to_gets:
|
||||
"\<lbrakk> \<And>P. \<lbrace> P \<rbrace> f \<lbrace> \<lambda>r s. P s \<and> r = v s \<rbrace>!; empty_fail f \<rbrakk> \<Longrightarrow> f = gets v"
|
||||
|
|
|
|||
Loading…
Reference in New Issue