--- a/src/HOL/HoareParallel/OG_Tactics.thy Mon Sep 21 11:15:21 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,496 +0,0 @@
-header {* \section{Generation of Verification Conditions} *}
-
-theory OG_Tactics
-imports OG_Hoare
-begin
-
-lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq
-lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq
-
-lemma ParallelConseqRule:
- "\<lbrakk> p \<subseteq> (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i))));
- \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i))))
- (Parallel Ts)
- (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i));
- (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i)) \<subseteq> q \<rbrakk>
- \<Longrightarrow> \<parallel>- p (Parallel Ts) q"
-apply (rule Conseq)
-prefer 2
- apply fast
-apply assumption+
-done
-
-lemma SkipRule: "p \<subseteq> q \<Longrightarrow> \<parallel>- p (Basic id) q"
-apply(rule oghoare_intros)
- prefer 2 apply(rule Basic)
- prefer 2 apply(rule subset_refl)
-apply(simp add:Id_def)
-done
-
-lemma BasicRule: "p \<subseteq> {s. (f s)\<in>q} \<Longrightarrow> \<parallel>- p (Basic f) q"
-apply(rule oghoare_intros)
- prefer 2 apply(rule oghoare_intros)
- prefer 2 apply(rule subset_refl)
-apply assumption
-done
-
-lemma SeqRule: "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q"
-apply(rule Seq)
-apply fast+
-done
-
-lemma CondRule:
- "\<lbrakk> p \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>w) \<and> (s\<notin>b \<longrightarrow> s\<in>w')}; \<parallel>- w c1 q; \<parallel>- w' c2 q \<rbrakk>
- \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q"
-apply(rule Cond)
- apply(rule Conseq)
- prefer 4 apply(rule Conseq)
-apply simp_all
-apply force+
-done
-
-lemma WhileRule: "\<lbrakk> p \<subseteq> i; \<parallel>- (i \<inter> b) c i ; (i \<inter> (-b)) \<subseteq> q \<rbrakk>
- \<Longrightarrow> \<parallel>- p (While b i c) q"
-apply(rule Conseq)
- prefer 2 apply(rule While)
-apply assumption+
-done
-
-text {* Three new proof rules for special instances of the @{text
-AnnBasic} and the @{text AnnAwait} commands when the transformation
-performed on the state is the identity, and for an @{text AnnAwait}
-command where the boolean condition is @{text "{s. True}"}: *}
-
-lemma AnnatomRule:
- "\<lbrakk> atom_com(c); \<parallel>- r c q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r {s. True} c) q"
-apply(rule AnnAwait)
-apply simp_all
-done
-
-lemma AnnskipRule:
- "r \<subseteq> q \<Longrightarrow> \<turnstile> (AnnBasic r id) q"
-apply(rule AnnBasic)
-apply simp
-done
-
-lemma AnnwaitRule:
- "\<lbrakk> (r \<inter> b) \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b (Basic id)) q"
-apply(rule AnnAwait)
- apply simp
-apply(rule BasicRule)
-apply simp
-done
-
-text {* Lemmata to avoid using the definition of @{text
-map_ann_hoare}, @{text interfree_aux}, @{text interfree_swap} and
-@{text interfree} by splitting it into different cases: *}
-
-lemma interfree_aux_rule1: "interfree_aux(co, q, None)"
-by(simp add:interfree_aux_def)
-
-lemma interfree_aux_rule2:
- "\<forall>(R,r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<Longrightarrow> interfree_aux(None, q, Some a)"
-apply(simp add:interfree_aux_def)
-apply(force elim:oghoare_sound)
-done
-
-lemma interfree_aux_rule3:
- "(\<forall>(R, r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<and> (\<forall>p\<in>(assertions c). \<parallel>- (p \<inter> R) r p))
- \<Longrightarrow> interfree_aux(Some c, q, Some a)"
-apply(simp add:interfree_aux_def)
-apply(force elim:oghoare_sound)
-done
-
-lemma AnnBasic_assertions:
- "\<lbrakk>interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk> \<Longrightarrow>
- interfree_aux(Some (AnnBasic r f), q, Some a)"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnSeq_assertions:
- "\<lbrakk> interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow>
- interfree_aux(Some (AnnSeq c1 c2), q, Some a)"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnCond1_assertions:
- "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a);
- interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow>
- interfree_aux(Some(AnnCond1 r b c1 c2), q, Some a)"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnCond2_assertions:
- "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow>
- interfree_aux(Some (AnnCond2 r b c), q, Some a)"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnWhile_assertions:
- "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, i, Some a);
- interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow>
- interfree_aux(Some (AnnWhile r b i c), q, Some a)"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnAwait_assertions:
- "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk>\<Longrightarrow>
- interfree_aux(Some (AnnAwait r b c), q, Some a)"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnBasic_atomics:
- "\<parallel>- (q \<inter> r) (Basic f) q \<Longrightarrow> interfree_aux(None, q, Some (AnnBasic r f))"
-by(simp add: interfree_aux_def oghoare_sound)
-
-lemma AnnSeq_atomics:
- "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow>
- interfree_aux(Any, q, Some (AnnSeq a1 a2))"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnCond1_atomics:
- "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow>
- interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))"
-apply(simp add: interfree_aux_def)
-by force
-
-lemma AnnCond2_atomics:
- "interfree_aux (Any, q, Some a)\<Longrightarrow> interfree_aux(Any, q, Some (AnnCond2 r b a))"
-by(simp add: interfree_aux_def)
-
-lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a)
- \<Longrightarrow> interfree_aux(Any, q, Some (AnnWhile r b i a))"
-by(simp add: interfree_aux_def)
-
-lemma Annatom_atomics:
- "\<parallel>- (q \<inter> r) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r {x. True} a))"
-by(simp add: interfree_aux_def oghoare_sound)
-
-lemma AnnAwait_atomics:
- "\<parallel>- (q \<inter> (r \<inter> b)) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r b a))"
-by(simp add: interfree_aux_def oghoare_sound)
-
-constdefs
- interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) \<Rightarrow> bool"
- "interfree_swap == \<lambda>(x, xs). \<forall>y\<in>set xs. interfree_aux (com x, post x, com y)
- \<and> interfree_aux(com y, post y, com x)"
-
-lemma interfree_swap_Empty: "interfree_swap (x, [])"
-by(simp add:interfree_swap_def)
-
-lemma interfree_swap_List:
- "\<lbrakk> interfree_aux (com x, post x, com y);
- interfree_aux (com y, post y ,com x); interfree_swap (x, xs) \<rbrakk>
- \<Longrightarrow> interfree_swap (x, y#xs)"
-by(simp add:interfree_swap_def)
-
-lemma interfree_swap_Map: "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> interfree_aux (com x, post x, c k)
- \<and> interfree_aux (c k, Q k, com x)
- \<Longrightarrow> interfree_swap (x, map (\<lambda>k. (c k, Q k)) [i..<j])"
-by(force simp add: interfree_swap_def less_diff_conv)
-
-lemma interfree_Empty: "interfree []"
-by(simp add:interfree_def)
-
-lemma interfree_List:
- "\<lbrakk> interfree_swap(x, xs); interfree xs \<rbrakk> \<Longrightarrow> interfree (x#xs)"
-apply(simp add:interfree_def interfree_swap_def)
-apply clarify
-apply(case_tac i)
- apply(case_tac j)
- apply simp_all
-apply(case_tac j,simp+)
-done
-
-lemma interfree_Map:
- "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j))
- \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..<b])"
-by(force simp add: interfree_def less_diff_conv)
-
-constdefs map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45)
- "[\<turnstile>] Ts == (\<forall>i<length Ts. \<exists>c q. Ts!i=(Some c, q) \<and> \<turnstile> c q)"
-
-lemma MapAnnEmpty: "[\<turnstile>] []"
-by(simp add:map_ann_hoare_def)
-
-lemma MapAnnList: "\<lbrakk> \<turnstile> c q ; [\<turnstile>] xs \<rbrakk> \<Longrightarrow> [\<turnstile>] (Some c,q)#xs"
-apply(simp add:map_ann_hoare_def)
-apply clarify
-apply(case_tac i,simp+)
-done
-
-lemma MapAnnMap:
- "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> \<turnstile> (c k) (Q k) \<Longrightarrow> [\<turnstile>] map (\<lambda>k. (Some (c k), Q k)) [i..<j]"
-apply(simp add: map_ann_hoare_def less_diff_conv)
-done
-
-lemma ParallelRule:"\<lbrakk> [\<turnstile>] Ts ; interfree Ts \<rbrakk>
- \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i))))
- Parallel Ts
- (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))"
-apply(rule Parallel)
- apply(simp add:map_ann_hoare_def)
-apply simp
-done
-(*
-lemma ParamParallelRule:
- "\<lbrakk> \<forall>k<n. \<turnstile> (c k) (Q k);
- \<forall>k l. k<n \<and> l<n \<and> k\<noteq>l \<longrightarrow> interfree_aux (Some(c k), Q k, Some(c l)) \<rbrakk>
- \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<n} . pre(c i)) COBEGIN SCHEME [0\<le>i<n] (c i) (Q i) COEND (\<Inter>i\<in>{i. i<n} . Q i )"
-apply(rule ParallelConseqRule)
- apply simp
- apply clarify
- apply force
- apply(rule ParallelRule)
- apply(rule MapAnnMap)
- apply simp
- apply(rule interfree_Map)
- apply simp
-apply simp
-apply clarify
-apply force
-done
-*)
-
-text {* The following are some useful lemmas and simplification
-tactics to control which theorems are used to simplify at each moment,
-so that the original input does not suffer any unexpected
-transformation. *}
-
-lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}"
-by fast
-lemma list_length: "length []=0 \<and> length (x#xs) = Suc(length xs)"
-by simp
-lemma list_lemmas: "length []=0 \<and> length (x#xs) = Suc(length xs)
-\<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
-by simp
-lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
-by auto
-lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
-lemmas my_simp_list = list_lemmas fst_conv snd_conv
-not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
-Collect_mem_eq ball_simps option.simps primrecdef_list
-lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length
-
-ML {*
-val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))
-
-val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
-
-val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
-*}
-
-text {* The following tactic applies @{text tac} to each conjunct in a
-subgoal of the form @{text "A \<Longrightarrow> a1 \<and> a2 \<and> .. \<and> an"} returning
-@{text n} subgoals, one for each conjunct: *}
-
-ML {*
-fun conjI_Tac tac i st = st |>
- ( (EVERY [rtac conjI i,
- conjI_Tac tac (i+1),
- tac i]) ORELSE (tac i) )
-*}
-
-
-subsubsection {* Tactic for the generation of the verification conditions *}
-
-text {* The tactic basically uses two subtactics:
-
-\begin{description}
-
-\item[HoareRuleTac] is called at the level of parallel programs, it
- uses the ParallelTac to solve parallel composition of programs.
- This verification has two parts, namely, (1) all component programs are
- correct and (2) they are interference free. @{text HoareRuleTac} is
- also called at the level of atomic regions, i.e. @{text "\<langle> \<rangle>"} and
- @{text "AWAIT b THEN _ END"}, and at each interference freedom test.
-
-\item[AnnHoareRuleTac] is for component programs which
- are annotated programs and so, there are not unknown assertions
- (no need to use the parameter precond, see NOTE).
-
- NOTE: precond(::bool) informs if the subgoal has the form @{text "\<parallel>- ?p c q"},
- in this case we have precond=False and the generated verification
- condition would have the form @{text "?p \<subseteq> \<dots>"} which can be solved by
- @{text "rtac subset_refl"}, if True we proceed to simplify it using
- the simplification tactics above.
-
-\end{description}
-*}
-
-ML {*
-
- fun WlpTac i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac false (i+1))
-and HoareRuleTac precond i st = st |>
- ( (WlpTac i THEN HoareRuleTac precond i)
- ORELSE
- (FIRST[rtac (@{thm SkipRule}) i,
- rtac (@{thm BasicRule}) i,
- EVERY[rtac (@{thm ParallelConseqRule}) i,
- ParallelConseq (i+2),
- ParallelTac (i+1),
- ParallelConseq i],
- EVERY[rtac (@{thm CondRule}) i,
- HoareRuleTac false (i+2),
- HoareRuleTac false (i+1)],
- EVERY[rtac (@{thm WhileRule}) i,
- HoareRuleTac true (i+1)],
- K all_tac i ]
- THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i))))
-
-and AnnWlpTac i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac (i+1))
-and AnnHoareRuleTac i st = st |>
- ( (AnnWlpTac i THEN AnnHoareRuleTac i )
- ORELSE
- (FIRST[(rtac (@{thm AnnskipRule}) i),
- EVERY[rtac (@{thm AnnatomRule}) i,
- HoareRuleTac true (i+1)],
- (rtac (@{thm AnnwaitRule}) i),
- rtac (@{thm AnnBasic}) i,
- EVERY[rtac (@{thm AnnCond1}) i,
- AnnHoareRuleTac (i+3),
- AnnHoareRuleTac (i+1)],
- EVERY[rtac (@{thm AnnCond2}) i,
- AnnHoareRuleTac (i+1)],
- EVERY[rtac (@{thm AnnWhile}) i,
- AnnHoareRuleTac (i+2)],
- EVERY[rtac (@{thm AnnAwait}) i,
- HoareRuleTac true (i+1)],
- K all_tac i]))
-
-and ParallelTac i = EVERY[rtac (@{thm ParallelRule}) i,
- interfree_Tac (i+1),
- MapAnn_Tac i]
-
-and MapAnn_Tac i st = st |>
- (FIRST[rtac (@{thm MapAnnEmpty}) i,
- EVERY[rtac (@{thm MapAnnList}) i,
- MapAnn_Tac (i+1),
- AnnHoareRuleTac i],
- EVERY[rtac (@{thm MapAnnMap}) i,
- rtac (@{thm allI}) i,rtac (@{thm impI}) i,
- AnnHoareRuleTac i]])
-
-and interfree_swap_Tac i st = st |>
- (FIRST[rtac (@{thm interfree_swap_Empty}) i,
- EVERY[rtac (@{thm interfree_swap_List}) i,
- interfree_swap_Tac (i+2),
- interfree_aux_Tac (i+1),
- interfree_aux_Tac i ],
- EVERY[rtac (@{thm interfree_swap_Map}) i,
- rtac (@{thm allI}) i,rtac (@{thm impI}) i,
- conjI_Tac (interfree_aux_Tac) i]])
-
-and interfree_Tac i st = st |>
- (FIRST[rtac (@{thm interfree_Empty}) i,
- EVERY[rtac (@{thm interfree_List}) i,
- interfree_Tac (i+1),
- interfree_swap_Tac i],
- EVERY[rtac (@{thm interfree_Map}) i,
- rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i,
- interfree_aux_Tac i ]])
-
-and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN
- (FIRST[rtac (@{thm interfree_aux_rule1}) i,
- dest_assertions_Tac i])
-
-and dest_assertions_Tac i st = st |>
- (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i,
- dest_atomics_Tac (i+1),
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnSeq_assertions}) i,
- dest_assertions_Tac (i+1),
- dest_assertions_Tac i],
- EVERY[rtac (@{thm AnnCond1_assertions}) i,
- dest_assertions_Tac (i+2),
- dest_assertions_Tac (i+1),
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnCond2_assertions}) i,
- dest_assertions_Tac (i+1),
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnWhile_assertions}) i,
- dest_assertions_Tac (i+2),
- dest_atomics_Tac (i+1),
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnAwait_assertions}) i,
- dest_atomics_Tac (i+1),
- dest_atomics_Tac i],
- dest_atomics_Tac i])
-
-and dest_atomics_Tac i st = st |>
- (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i,
- HoareRuleTac true i],
- EVERY[rtac (@{thm AnnSeq_atomics}) i,
- dest_atomics_Tac (i+1),
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnCond1_atomics}) i,
- dest_atomics_Tac (i+1),
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnCond2_atomics}) i,
- dest_atomics_Tac i],
- EVERY[rtac (@{thm AnnWhile_atomics}) i,
- dest_atomics_Tac i],
- EVERY[rtac (@{thm Annatom_atomics}) i,
- HoareRuleTac true i],
- EVERY[rtac (@{thm AnnAwait_atomics}) i,
- HoareRuleTac true i],
- K all_tac i])
-*}
-
-
-text {* The final tactic is given the name @{text oghoare}: *}
-
-ML {*
-val oghoare_tac = SUBGOAL (fn (_, i) =>
- (HoareRuleTac true i))
-*}
-
-text {* Notice that the tactic for parallel programs @{text
-"oghoare_tac"} is initially invoked with the value @{text true} for
-the parameter @{text precond}.
-
-Parts of the tactic can be also individually used to generate the
-verification conditions for annotated sequential programs and to
-generate verification conditions out of interference freedom tests: *}
-
-ML {* val annhoare_tac = SUBGOAL (fn (_, i) =>
- (AnnHoareRuleTac i))
-
-val interfree_aux_tac = SUBGOAL (fn (_, i) =>
- (interfree_aux_Tac i))
-*}
-
-text {* The so defined ML tactics are then ``exported'' to be used in
-Isabelle proofs. *}
-
-method_setup oghoare = {*
- Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
- "verification condition generator for the oghoare logic"
-
-method_setup annhoare = {*
- Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
- "verification condition generator for the ann_hoare logic"
-
-method_setup interfree_aux = {*
- Scan.succeed (K (SIMPLE_METHOD' interfree_aux_tac)) *}
- "verification condition generator for interference freedom tests"
-
-text {* Tactics useful for dealing with the generated verification conditions: *}
-
-method_setup conjI_tac = {*
- Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac)))) *}
- "verification condition generator for interference freedom tests"
-
-ML {*
-fun disjE_Tac tac i st = st |>
- ( (EVERY [etac disjE i,
- disjE_Tac tac (i+1),
- tac i]) ORELSE (tac i) )
-*}
-
-method_setup disjE_tac = {*
- Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *}
- "verification condition generator for interference freedom tests"
-
-end