(* Title: HOL/HOLCF/IOA/Abstraction.thy
Author: Olaf Müller
*)
section \<open>Abstraction Theory -- tailored for I/O automata\<close>
theory Abstraction
imports LiveIOA
begin
default_sort type
definition cex_abs :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) execution \<Rightarrow> ('a, 's2) execution"
where "cex_abs f ex = (f (fst ex), Map (\<lambda>(a, t). (a, f t)) \<cdot> (snd ex))"
text \<open>equals cex_abs on Sequences -- after ex2seq application\<close>
definition cex_absSeq ::
"('s1 \<Rightarrow> 's2) \<Rightarrow> ('a option, 's1) transition Seq \<Rightarrow> ('a option, 's2)transition Seq"
where "cex_absSeq f = (\<lambda>s. Map (\<lambda>(s, a, t). (f s, a, f t)) \<cdot> s)"
definition is_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
where "is_abstraction f C A \<longleftrightarrow>
((\<forall>s \<in> starts_of C. f s \<in> starts_of A) \<and>
(\<forall>s t a. reachable C s \<and> s \<midarrow>a\<midarrow>C\<rightarrow> t \<longrightarrow> f s \<midarrow>a\<midarrow>A\<rightarrow> f t))"
definition weakeningIOA :: "('a, 's2) ioa \<Rightarrow> ('a, 's1) ioa \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
where "weakeningIOA A C h \<longleftrightarrow> (\<forall>ex. ex \<in> executions C \<longrightarrow> cex_abs h ex \<in> executions A)"
definition temp_strengthening :: "('a, 's2) ioa_temp \<Rightarrow> ('a, 's1) ioa_temp \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
where "temp_strengthening Q P h \<longleftrightarrow> (\<forall>ex. (cex_abs h ex \<TTurnstile> Q) \<longrightarrow> (ex \<TTurnstile> P))"
definition temp_weakening :: "('a, 's2) ioa_temp \<Rightarrow> ('a, 's1) ioa_temp \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
where "temp_weakening Q P h \<longleftrightarrow> temp_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h"
definition state_strengthening :: "('a, 's2) step_pred \<Rightarrow> ('a, 's1) step_pred \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
where "state_strengthening Q P h \<longleftrightarrow> (\<forall>s t a. Q (h s, a, h t) \<longrightarrow> P (s, a, t))"
definition state_weakening :: "('a, 's2) step_pred \<Rightarrow> ('a, 's1) step_pred \<Rightarrow> ('s1 \<Rightarrow> 's2) \<Rightarrow> bool"
where "state_weakening Q P h \<longleftrightarrow> state_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h"
definition is_live_abstraction :: "('s1 \<Rightarrow> 's2) \<Rightarrow> ('a, 's1) live_ioa \<Rightarrow> ('a, 's2) live_ioa \<Rightarrow> bool"
where "is_live_abstraction h CL AM \<longleftrightarrow>
is_abstraction h (fst CL) (fst AM) \<and> temp_weakening (snd AM) (snd CL) h"
(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
axiomatization where
ex2seq_abs_cex: "ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
(* analog to the proved thm strength_Box - proof skipped as trivial *)
axiomatization where
weak_Box: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<box>P) (\<box>Q) h"
(* analog to the proved thm strength_Next - proof skipped as trivial *)
axiomatization where
weak_Next: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<circle>P) (\<circle>Q) h"
subsection \<open>\<open>cex_abs\<close>\<close>
lemma cex_abs_UU [simp]: "cex_abs f (s, UU) = (f s, UU)"
by (simp add: cex_abs_def)
lemma cex_abs_nil [simp]: "cex_abs f (s,nil) = (f s, nil)"
by (simp add: cex_abs_def)
lemma cex_abs_cons [simp]:
"cex_abs f (s, (a, t) \<leadsto> ex) = (f s, (a, f t) \<leadsto> (snd (cex_abs f (t, ex))))"
by (simp add: cex_abs_def)
subsection \<open>Lemmas\<close>
lemma temp_weakening_def2: "temp_weakening Q P h \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P) \<longrightarrow> (cex_abs h ex \<TTurnstile> Q))"
apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def)
apply auto
done
lemma state_weakening_def2: "state_weakening Q P h \<longleftrightarrow> (\<forall>s t a. P (s, a, t) \<longrightarrow> Q (h s, a, h t))"
apply (simp add: state_weakening_def state_strengthening_def NOT_def)
apply auto
done
subsection \<open>Abstraction Rules for Properties\<close>
lemma exec_frag_abstraction [rule_format]:
"is_abstraction h C A \<Longrightarrow>
\<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow> is_exec_frag A (cex_abs h (s, xs))"
apply (simp add: cex_abs_def)
apply (pair_induct xs simp: is_exec_frag_def)
txt \<open>main case\<close>
apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
done
lemma abs_is_weakening: "is_abstraction h C A \<Longrightarrow> weakeningIOA A C h"
apply (simp add: weakeningIOA_def)
apply auto
apply (simp add: executions_def)
txt \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_abstraction_def cex_abs_def)
txt \<open>is-execution-fragment\<close>
apply (erule exec_frag_abstraction)
apply (simp add: reachable.reachable_0)
done
lemma AbsRuleT1:
"is_abstraction h C A \<Longrightarrow> validIOA A Q \<Longrightarrow> temp_strengthening Q P h \<Longrightarrow> validIOA C P"
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
apply (auto simp add: split_paired_all)
done
lemma AbsRuleT2:
"is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A, M) Q \<Longrightarrow> temp_strengthening Q P h
\<Longrightarrow> validLIOA (C, L) P"
apply (unfold is_live_abstraction_def)
apply auto
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
apply (auto simp add: split_paired_all)
done
lemma AbsRuleTImprove:
"is_live_abstraction h (C, L) (A, M) \<Longrightarrow> validLIOA (A,M) (H1 \<^bold>\<longrightarrow> Q) \<Longrightarrow>
temp_strengthening Q P h \<Longrightarrow> temp_weakening H1 H2 h \<Longrightarrow> validLIOA (C, L) H2 \<Longrightarrow>
validLIOA (C, L) P"
apply (unfold is_live_abstraction_def)
apply auto
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def temp_weakening_def2 validLIOA_def validIOA_def temp_strengthening_def)
apply (auto simp add: split_paired_all)
done
subsection \<open>Correctness of safe abstraction\<close>
lemma abstraction_is_ref_map: "is_abstraction h C A \<Longrightarrow> is_ref_map h C A"
apply (auto simp: is_abstraction_def is_ref_map_def)
apply (rule_tac x = "(a,h t) \<leadsto>nil" in exI)
apply (simp add: move_def)
done
lemma abs_safety: "inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_abstraction h C A \<Longrightarrow> C =<| A"
apply (simp add: ioa_implements_def)
apply (rule trace_inclusion)
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (erule abstraction_is_ref_map)
done
subsection \<open>Correctness of life abstraction\<close>
text \<open>
Reduces to \<open>Filter (Map fst x) = Filter (Map fst (Map (\<lambda>(a, t). (a, x)) x)\<close>,
that is to special Map Lemma.
\<close>
lemma traces_coincide_abs:
"ext C = ext A \<Longrightarrow> mk_trace C \<cdot> xs = mk_trace A \<cdot> (snd (cex_abs f (s, xs)))"
apply (unfold cex_abs_def mk_trace_def filter_act_def)
apply simp
apply (pair_induct xs)
done
text \<open>
Does not work with \<open>abstraction_is_ref_map\<close> as proof of \<open>abs_safety\<close>, because
\<open>is_live_abstraction\<close> includes \<open>temp_strengthening\<close> which is necessarily based
on \<open>cex_abs\<close> and not on \<open>corresp_ex\<close>. Thus, the proof is redone in a more specific
way for \<open>cex_abs\<close>.
\<close>
lemma abs_liveness:
"inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> is_live_abstraction h (C, M) (A, L) \<Longrightarrow>
live_implements (C, M) (A, L)"
apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
apply auto
apply (rule_tac x = "cex_abs h ex" in exI)
apply auto
text \<open>Traces coincide\<close>
apply (pair ex)
apply (rule traces_coincide_abs)
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
text \<open>\<open>cex_abs\<close> is execution\<close>
apply (pair ex)
apply (simp add: executions_def)
text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_abstraction_def cex_abs_def)
text \<open>\<open>is_execution_fragment\<close>\<close>
apply (erule exec_frag_abstraction)
apply (simp add: reachable.reachable_0)
text \<open>Liveness\<close>
apply (simp add: temp_weakening_def2)
apply (pair ex)
done
subsection \<open>Abstraction Rules for Automata\<close>
lemma AbsRuleA1:
"inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> inp Q = inp P \<Longrightarrow> out Q = out P \<Longrightarrow>
is_abstraction h1 C A \<Longrightarrow> A =<| Q \<Longrightarrow> is_abstraction h2 Q P \<Longrightarrow> C =<| P"
apply (drule abs_safety)
apply assumption+
apply (drule abs_safety)
apply assumption+
apply (erule implements_trans)
apply (erule implements_trans)
apply assumption
done
lemma AbsRuleA2:
"inp C = inp A \<Longrightarrow> out C = out A \<Longrightarrow> inp Q = inp P \<Longrightarrow> out Q = out P \<Longrightarrow>
is_live_abstraction h1 (C, LC) (A, LA) \<Longrightarrow> live_implements (A, LA) (Q, LQ) \<Longrightarrow>
is_live_abstraction h2 (Q, LQ) (P, LP) \<Longrightarrow> live_implements (C, LC) (P, LP)"
apply (drule abs_liveness)
apply assumption+
apply (drule abs_liveness)
apply assumption+
apply (erule live_implements_trans)
apply (erule live_implements_trans)
apply assumption
done
declare split_paired_All [simp del]
subsection \<open>Localizing Temporal Strengthenings and Weakenings\<close>
lemma strength_AND:
"temp_strengthening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow>
temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
by (auto simp: temp_strengthening_def)
lemma strength_OR:
"temp_strengthening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow>
temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
by (auto simp: temp_strengthening_def)
lemma strength_NOT: "temp_weakening P Q h \<Longrightarrow> temp_strengthening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
by (auto simp: temp_weakening_def2 temp_strengthening_def)
lemma strength_IMPLIES:
"temp_weakening P1 Q1 h \<Longrightarrow> temp_strengthening P2 Q2 h \<Longrightarrow>
temp_strengthening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
by (simp add: temp_weakening_def2 temp_strengthening_def)
lemma weak_AND:
"temp_weakening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow>
temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
by (simp add: temp_weakening_def2)
lemma weak_OR:
"temp_weakening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow>
temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
by (simp add: temp_weakening_def2)
lemma weak_NOT:
"temp_strengthening P Q h \<Longrightarrow> temp_weakening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
by (auto simp add: temp_weakening_def2 temp_strengthening_def)
lemma weak_IMPLIES:
"temp_strengthening P1 Q1 h \<Longrightarrow> temp_weakening P2 Q2 h \<Longrightarrow>
temp_weakening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
by (simp add: temp_weakening_def2 temp_strengthening_def)
subsubsection \<open>Box\<close>
(* FIXME: should be same as nil_is_Conc2 when all nils are turned to right side! *)
lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x = nil \<and> y = UU))"
by (Seq_case_simp x)
lemma ex2seqConc [rule_format]:
"Finite s1 \<longrightarrow> (\<forall>ex. (s \<noteq> nil \<and> s \<noteq> UU \<and> ex2seq ex = s1 @@ s) \<longrightarrow> (\<exists>ex'. s = ex2seq ex'))"
apply (rule impI)
apply Seq_Finite_induct
apply blast
text \<open>main case\<close>
apply clarify
apply (pair ex)
apply (Seq_case_simp x2)
text \<open>\<open>UU\<close> case\<close>
apply (simp add: nil_is_Conc)
text \<open>\<open>nil\<close> case\<close>
apply (simp add: nil_is_Conc)
text \<open>cons case\<close>
apply (pair aa)
apply auto
done
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
lemma ex2seq_tsuffix: "tsuffix s (ex2seq ex) \<Longrightarrow> \<exists>ex'. s = (ex2seq ex')"
apply (unfold tsuffix_def suffix_def)
apply auto
apply (drule ex2seqConc)
apply auto
done
(*important property of cex_absSeq: As it is a 1to1 correspondence,
properties carry over *)
lemma cex_absSeq_tsuffix: "tsuffix s t \<Longrightarrow> tsuffix (cex_absSeq h s) (cex_absSeq h t)"
apply (unfold tsuffix_def suffix_def cex_absSeq_def)
apply auto
apply (simp add: Mapnil)
apply (simp add: MapUU)
apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))\<cdot>s1" in exI)
apply (simp add: Map2Finite MapConc)
done
lemma strength_Box: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<box>P) (\<box>Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
apply clarify
apply (frule ex2seq_tsuffix)
apply clarify
apply (drule_tac h = "h" in cex_absSeq_tsuffix)
apply (simp add: ex2seq_abs_cex)
done
subsubsection \<open>Init\<close>
lemma strength_Init:
"state_strengthening P Q h \<Longrightarrow> temp_strengthening (Init P) (Init Q) h"
apply (unfold temp_strengthening_def state_strengthening_def
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
done
subsubsection \<open>Next\<close>
lemma TL_ex2seq_UU: "TL \<cdot> (ex2seq (cex_abs h ex)) = UU \<longleftrightarrow> TL \<cdot> (ex2seq ex) = UU"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
done
lemma TL_ex2seq_nil: "TL \<cdot> (ex2seq (cex_abs h ex)) = nil \<longleftrightarrow> TL \<cdot> (ex2seq ex) = nil"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
done
(*important property of cex_absSeq: As it is a 1to1 correspondence,
properties carry over*)
lemma cex_absSeq_TL: "cex_absSeq h (TL \<cdot> s) = TL \<cdot> (cex_absSeq h s)"
by (simp add: MapTL cex_absSeq_def)
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
lemma TLex2seq: "snd ex \<noteq> UU \<Longrightarrow> snd ex \<noteq> nil \<Longrightarrow> \<exists>ex'. TL\<cdot>(ex2seq ex) = ex2seq ex'"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply auto
done
lemma ex2seqnilTL: "TL \<cdot> (ex2seq ex) \<noteq> nil \<longleftrightarrow> snd ex \<noteq> nil \<and> snd ex \<noteq> UU"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply (Seq_case_simp s)
apply (pair a)
done
lemma strength_Next: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<circle>P) (\<circle>Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
apply simp
apply auto
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU)
text \<open>cons case\<close>
apply (simp add: TL_ex2seq_nil TL_ex2seq_UU ex2seq_abs_cex cex_absSeq_TL [symmetric] ex2seqnilTL)
apply (erule conjE)
apply (drule TLex2seq)
apply assumption
apply auto
done
text \<open>Localizing Temporal Weakenings - 2\<close>
lemma weak_Init: "state_weakening P Q h \<Longrightarrow> temp_weakening (Init P) (Init Q) h"
apply (simp add: temp_weakening_def2 state_weakening_def2
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
done
text \<open>Localizing Temproal Strengthenings - 3\<close>
lemma strength_Diamond: "temp_strengthening P Q h \<Longrightarrow> temp_strengthening (\<diamond>P) (\<diamond>Q) h"
apply (unfold Diamond_def)
apply (rule strength_NOT)
apply (rule weak_Box)
apply (erule weak_NOT)
done
lemma strength_Leadsto:
"temp_weakening P1 P2 h \<Longrightarrow> temp_strengthening Q1 Q2 h \<Longrightarrow>
temp_strengthening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
apply (unfold Leadsto_def)
apply (rule strength_Box)
apply (erule strength_IMPLIES)
apply (erule strength_Diamond)
done
text \<open>Localizing Temporal Weakenings - 3\<close>
lemma weak_Diamond: "temp_weakening P Q h \<Longrightarrow> temp_weakening (\<diamond>P) (\<diamond>Q) h"
apply (unfold Diamond_def)
apply (rule weak_NOT)
apply (rule strength_Box)
apply (erule strength_NOT)
done
lemma weak_Leadsto:
"temp_strengthening P1 P2 h \<Longrightarrow> temp_weakening Q1 Q2 h \<Longrightarrow>
temp_weakening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
apply (unfold Leadsto_def)
apply (rule weak_Box)
apply (erule weak_IMPLIES)
apply (erule weak_Diamond)
done
lemma weak_WF:
"(\<And>s. Enabled A acts (h s) \<Longrightarrow> Enabled C acts s)
\<Longrightarrow> temp_weakening (WF A acts) (WF C acts) h"
apply (unfold WF_def)
apply (rule weak_IMPLIES)
apply (rule strength_Diamond)
apply (rule strength_Box)
apply (rule strength_Init)
apply (rule_tac [2] weak_Box)
apply (rule_tac [2] weak_Diamond)
apply (rule_tac [2] weak_Init)
apply (auto simp add: state_weakening_def state_strengthening_def
xt2_def plift_def option_lift_def NOT_def)
done
lemma weak_SF:
"(\<And>s. Enabled A acts (h s) \<Longrightarrow> Enabled C acts s)
\<Longrightarrow> temp_weakening (SF A acts) (SF C acts) h"
apply (unfold SF_def)
apply (rule weak_IMPLIES)
apply (rule strength_Box)
apply (rule strength_Diamond)
apply (rule strength_Init)
apply (rule_tac [2] weak_Box)
apply (rule_tac [2] weak_Diamond)
apply (rule_tac [2] weak_Init)
apply (auto simp add: state_weakening_def state_strengthening_def
xt2_def plift_def option_lift_def NOT_def)
done
lemmas weak_strength_lemmas =
weak_OR weak_AND weak_NOT weak_IMPLIES weak_Box weak_Next weak_Init
weak_Diamond weak_Leadsto strength_OR strength_AND strength_NOT
strength_IMPLIES strength_Box strength_Next strength_Init
strength_Diamond strength_Leadsto weak_WF weak_SF
ML \<open>
fun abstraction_tac ctxt =
SELECT_GOAL (auto_tac
(ctxt addSIs @{thms weak_strength_lemmas}
addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
\<close>
method_setup abstraction = \<open>Scan.succeed (SIMPLE_METHOD' o abstraction_tac)\<close>
end