equal
deleted
inserted
replaced
106 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)" |
106 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)" |
107 apply (tactic "split_all_tac 1", rename_tac P e Q) |
107 apply (tactic "split_all_tac 1", rename_tac P e Q) |
108 apply (rule hoare_ehoare.induct) |
108 apply (rule hoare_ehoare.induct) |
109 (*18*) |
109 (*18*) |
110 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *}) |
110 apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *}) |
111 apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *}) |
111 apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *}) |
112 apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *}) |
112 apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *}) |
113 apply (simp_all only: cnvalid1_eq cenvalid_def2) |
113 apply (simp_all only: cnvalid1_eq cenvalid_def2) |
114 apply fast |
114 apply fast |
115 apply fast |
115 apply fast |
116 apply fast |
116 apply fast |
117 apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) |
117 apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+) |