89 lemma cnvalid1_eq: |
89 lemma cnvalid1_eq: |
90 "A |\<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)" |
90 "A |\<Turnstile> {(P,c,Q)} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)" |
91 by(simp add: cnvalids_def nvalids_def nvalid_def2) |
91 by(simp add: cnvalids_def nvalids_def nvalid_def2) |
92 |
92 |
93 lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>\<^sub>e t \<longrightarrow> A |\<Turnstile>\<^sub>e t)" |
93 lemma hoare_sound_main:"\<And>t. (A |\<turnstile> C \<longrightarrow> A |\<Turnstile> C) \<and> (A |\<turnstile>\<^sub>e t \<longrightarrow> A |\<Turnstile>\<^sub>e t)" |
94 apply (tactic "split_all_tac @{context} 1", rename_tac P e Q) |
94 apply (tactic "split_all_tac \<^context> 1", rename_tac P e Q) |
95 apply (rule hoare_ehoare.induct) |
95 apply (rule hoare_ehoare.induct) |
96 (*18*) |
96 (*18*) |
97 apply (tactic \<open>ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}])\<close>) |
97 apply (tactic \<open>ALLGOALS (REPEAT o dresolve_tac \<^context> [@{thm all_conjunct2}, @{thm all3_conjunct2}])\<close>) |
98 apply (tactic \<open>ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare _ _" [])\<close>) |
98 apply (tactic \<open>ALLGOALS (REPEAT o Rule_Insts.thin_tac \<^context> "hoare _ _" [])\<close>) |
99 apply (tactic \<open>ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare _ _" [])\<close>) |
99 apply (tactic \<open>ALLGOALS (REPEAT o Rule_Insts.thin_tac \<^context> "ehoare _ _" [])\<close>) |
100 apply (simp_all only: cnvalid1_eq cenvalid_def2) |
100 apply (simp_all only: cnvalid1_eq cenvalid_def2) |
101 apply fast |
101 apply fast |
102 apply fast |
102 apply fast |
103 apply fast |
103 apply fast |
104 apply (clarify,tactic "smp_tac @{context} 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) |
104 apply (clarify,tactic "smp_tac \<^context> 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) |
105 apply fast |
105 apply fast |
106 apply fast |
106 apply fast |
107 apply fast |
107 apply fast |
108 apply fast |
108 apply fast |
109 apply fast |
109 apply fast |