equal
deleted
inserted
replaced
341 qed auto |
341 qed auto |
342 qed |
342 qed |
343 ultimately show ?case |
343 ultimately show ?case |
344 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
344 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
345 apply (unfold IA_def, intro condI, assumption+) |
345 apply (unfold IA_def, intro condI, assumption+) |
346 apply (rule_tac x = "?ks_f sr ks" in pred_exI) |
346 apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI) |
347 apply (rule_tac x = "?idx_f sr ks ia" in pred_exI) |
347 apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI) |
348 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
348 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
349 apply (auto simp:sep_conj_ac fam_conj_simps) |
349 apply (auto simp:sep_conj_ac fam_conj_simps) |
350 (***************************************************************************) |
350 (***************************************************************************) |
351 (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *) |
351 (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *) |
352 (*-------------------------------------------------------------------------*) |
352 (*-------------------------------------------------------------------------*) |
525 qed auto |
525 qed auto |
526 qed |
526 qed |
527 ultimately show ?case |
527 ultimately show ?case |
528 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
528 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
529 apply (unfold IA_def, intro condI, assumption+) |
529 apply (unfold IA_def, intro condI, assumption+) |
530 apply (rule_tac x = "?ks_f sr ks" in pred_exI) |
530 apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI) |
531 apply (rule_tac x = "?idx_f sr ks ia" in pred_exI) |
531 apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI) |
532 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
532 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
533 apply (auto simp:sep_conj_ac fam_conj_simps) |
533 apply (auto simp:sep_conj_ac fam_conj_simps) |
534 (***************************************************************************) |
534 (***************************************************************************) |
535 (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *) |
535 (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *) |
536 (*-------------------------------------------------------------------------*) |
536 (*-------------------------------------------------------------------------*) |
710 qed auto |
710 qed auto |
711 qed |
711 qed |
712 ultimately show ?case |
712 ultimately show ?case |
713 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
713 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
714 apply (unfold IA_def, intro condI, assumption+) |
714 apply (unfold IA_def, intro condI, assumption+) |
715 apply (rule_tac x = "?ks_f sr ks" in pred_exI) |
715 apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI) |
716 apply (rule_tac x = "?idx_f sr ks ia" in pred_exI) |
716 apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI) |
717 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
717 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
718 apply (auto simp:sep_conj_ac fam_conj_simps) |
718 apply (auto simp:sep_conj_ac fam_conj_simps) |
719 (***************************************************************************) |
719 (***************************************************************************) |
720 (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *) |
720 (* apply (unfold fam_conj_insert_simp [OF h_fresh1[OF at_fresh_sr]], simp) *) |
721 (*-------------------------------------------------------------------------*) |
721 (*-------------------------------------------------------------------------*) |
910 by simp |
910 by simp |
911 qed |
911 qed |
912 ultimately show ?case |
912 ultimately show ?case |
913 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
913 apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI) |
914 apply (unfold IA_def, intro condI, assumption+) |
914 apply (unfold IA_def, intro condI, assumption+) |
915 apply (rule_tac x = "?ks_f sr ks" in pred_exI) |
915 apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI) |
916 apply (rule_tac x = "?idx_f sr ks ia" in pred_exI) |
916 apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI) |
917 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
917 apply (unfold fam_conj_disj_simp[OF fresh_atm]) |
918 by (auto simp:sep_conj_ac fam_conj_simps) |
918 by (auto simp:sep_conj_ac fam_conj_simps) |
919 qed |
919 qed |
920 |
920 |
921 lemma hoare_goto[step]: "IA. \<lbrace> pc i \<rbrace> |
921 lemma hoare_goto[step]: "IA. \<lbrace> pc i \<rbrace> |