# Theory Abstraction

theory Abstraction
imports LiveIOA
(*  Title:      HOL/HOLCF/IOA/Abstraction.thy
Author:     Olaf MÃ¼ller
*)

section ‹Abstraction Theory -- tailored for I/O automata›

theory Abstraction
imports LiveIOA
begin

default_sort type

definition cex_abs :: "('s1 ⇒ 's2) ⇒ ('a, 's1) execution ⇒ ('a, 's2) execution"
where "cex_abs f ex = (f (fst ex), Map (λ(a, t). (a, f t)) ⋅ (snd ex))"

text ‹equals cex_abs on Sequences -- after ex2seq application›
definition cex_absSeq ::
"('s1 ⇒ 's2) ⇒ ('a option, 's1) transition Seq ⇒ ('a option, 's2)transition Seq"
where "cex_absSeq f = (λs. Map (λ(s, a, t). (f s, a, f t)) ⋅ s)"

definition is_abstraction :: "('s1 ⇒ 's2) ⇒ ('a, 's1) ioa ⇒ ('a, 's2) ioa ⇒ bool"
where "is_abstraction f C A ⟷
((∀s ∈ starts_of C. f s ∈ starts_of A) ∧
(∀s t a. reachable C s ∧ s ─a─C→ t ⟶ f s ─a─A→ f t))"

definition weakeningIOA :: "('a, 's2) ioa ⇒ ('a, 's1) ioa ⇒ ('s1 ⇒ 's2) ⇒ bool"
where "weakeningIOA A C h ⟷ (∀ex. ex ∈ executions C ⟶ cex_abs h ex ∈ executions A)"

definition temp_strengthening :: "('a, 's2) ioa_temp ⇒ ('a, 's1) ioa_temp ⇒ ('s1 ⇒ 's2) ⇒ bool"
where "temp_strengthening Q P h ⟷ (∀ex. (cex_abs h ex ⊫ Q) ⟶ (ex ⊫ P))"

definition temp_weakening :: "('a, 's2) ioa_temp ⇒ ('a, 's1) ioa_temp ⇒ ('s1 ⇒ 's2) ⇒ bool"
where "temp_weakening Q P h ⟷ temp_strengthening (¬ Q) (¬ P) h"

definition state_strengthening :: "('a, 's2) step_pred ⇒ ('a, 's1) step_pred ⇒ ('s1 ⇒ 's2) ⇒ bool"
where "state_strengthening Q P h ⟷ (∀s t a. Q (h s, a, h t) ⟶ P (s, a, t))"

definition state_weakening :: "('a, 's2) step_pred ⇒ ('a, 's1) step_pred ⇒ ('s1 ⇒ 's2) ⇒ bool"
where "state_weakening Q P h ⟷ state_strengthening (¬ Q) (¬ P) h"

definition is_live_abstraction :: "('s1 ⇒ 's2) ⇒ ('a, 's1) live_ioa ⇒ ('a, 's2) live_ioa ⇒ bool"
where "is_live_abstraction h CL AM ⟷
is_abstraction h (fst CL) (fst AM) ∧ 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 ⟹ temp_weakening (□P) (□Q) h"

(* analog to the proved thm strength_Next - proof skipped as trivial *)
axiomatization where
weak_Next: "temp_weakening P Q h ⟹ temp_weakening (○P) (○Q) h"

subsection ‹‹cex_abs››

lemma cex_abs_UU [simp]: "cex_abs f (s, UU) = (f s, UU)"

lemma cex_abs_nil [simp]: "cex_abs f (s,nil) = (f s, nil)"

lemma cex_abs_cons [simp]:
"cex_abs f (s, (a, t) ↝ ex) = (f s, (a, f t) ↝ (snd (cex_abs f (t, ex))))"

subsection ‹Lemmas›

lemma temp_weakening_def2: "temp_weakening Q P h ⟷ (∀ex. (ex ⊫ P) ⟶ (cex_abs h ex ⊫ 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 ⟷ (∀s t a. P (s, a, t) ⟶ Q (h s, a, h t))"
apply (simp add: state_weakening_def state_strengthening_def NOT_def)
apply auto
done

subsection ‹Abstraction Rules for Properties›

lemma exec_frag_abstraction [rule_format]:
"is_abstraction h C A ⟹
∀s. reachable C s ∧ is_exec_frag C (s, xs) ⟶ is_exec_frag A (cex_abs h (s, xs))"
apply (pair_induct xs simp: is_exec_frag_def)
txt ‹main case›
apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
done

lemma abs_is_weakening: "is_abstraction h C A ⟹ weakeningIOA A C h"
apply auto
txt ‹start state›
apply (rule conjI)
txt ‹is-execution-fragment›
apply (erule exec_frag_abstraction)
done

lemma AbsRuleT1:
"is_abstraction h C A ⟹ validIOA A Q ⟹ temp_strengthening Q P h ⟹ validIOA C P"
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
done

lemma AbsRuleT2:
"is_live_abstraction h (C, L) (A, M) ⟹ validLIOA (A, M) Q ⟹ temp_strengthening Q P h
⟹ 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)
done

lemma AbsRuleTImprove:
"is_live_abstraction h (C, L) (A, M) ⟹ validLIOA (A,M) (H1  Q) ⟹
temp_strengthening Q P h ⟹ temp_weakening H1 H2 h ⟹ validLIOA (C, L) H2 ⟹
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)
done

subsection ‹Correctness of safe abstraction›

lemma abstraction_is_ref_map: "is_abstraction h C A ⟹ is_ref_map h C A"
apply (auto simp: is_abstraction_def is_ref_map_def)
apply (rule_tac x = "(a,h t) ↝nil" in exI)
done

lemma abs_safety: "inp C = inp A ⟹ out C = out A ⟹ is_abstraction h C A ⟹ C =<| A"
apply (rule trace_inclusion)
apply (auto)[1]
apply (erule abstraction_is_ref_map)
done

subsection ‹Correctness of life abstraction›

text ‹
Reduces to ‹Filter (Map fst x) = Filter (Map fst (Map (λ(a, t). (a, x)) x)›,
that is to special Map Lemma.
›
lemma traces_coincide_abs:
"ext C = ext A ⟹ mk_trace C ⋅ xs = mk_trace A ⋅ (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 ‹
Does not work with ‹abstraction_is_ref_map› as proof of ‹abs_safety›, because
‹is_live_abstraction› includes ‹temp_strengthening› which is necessarily based
on ‹cex_abs› and not on ‹corresp_ex›. Thus, the proof is redone in a more specific
way for ‹cex_abs›.
›
lemma abs_liveness:
"inp C = inp A ⟹ out C = out A ⟹ is_live_abstraction h (C, M) (A, L) ⟹
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 ‹Traces coincide›
apply (pair ex)
apply (rule traces_coincide_abs)
apply (auto)[1]

text ‹‹cex_abs› is execution›
apply (pair ex)
text ‹start state›
apply (rule conjI)
text ‹‹is_execution_fragment››
apply (erule exec_frag_abstraction)

text ‹Liveness›
apply (pair ex)
done

subsection ‹Abstraction Rules for Automata›

lemma AbsRuleA1:
"inp C = inp A ⟹ out C = out A ⟹ inp Q = inp P ⟹ out Q = out P ⟹
is_abstraction h1 C A ⟹ A =<| Q ⟹ is_abstraction h2 Q P ⟹ 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 ⟹ out C = out A ⟹ inp Q = inp P ⟹ out Q = out P ⟹
is_live_abstraction h1 (C, LC) (A, LA) ⟹ live_implements (A, LA) (Q, LQ) ⟹
is_live_abstraction h2 (Q, LQ) (P, LP) ⟹ 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 ‹Localizing Temporal Strengthenings and Weakenings›

lemma strength_AND:
"temp_strengthening P1 Q1 h ⟹ temp_strengthening P2 Q2 h ⟹
temp_strengthening (P1  P2) (Q1  Q2) h"
by (auto simp: temp_strengthening_def)

lemma strength_OR:
"temp_strengthening P1 Q1 h ⟹ temp_strengthening P2 Q2 h ⟹
temp_strengthening (P1  P2) (Q1  Q2) h"
by (auto simp: temp_strengthening_def)

lemma strength_NOT: "temp_weakening P Q h ⟹ temp_strengthening (¬ P) (¬ Q) h"
by (auto simp: temp_weakening_def2 temp_strengthening_def)

lemma strength_IMPLIES:
"temp_weakening P1 Q1 h ⟹ temp_strengthening P2 Q2 h ⟹
temp_strengthening (P1  P2) (Q1  Q2) h"

lemma weak_AND:
"temp_weakening P1 Q1 h ⟹ temp_weakening P2 Q2 h ⟹
temp_weakening (P1  P2) (Q1  Q2) h"

lemma weak_OR:
"temp_weakening P1 Q1 h ⟹ temp_weakening P2 Q2 h ⟹
temp_weakening (P1  P2) (Q1  Q2) h"

lemma weak_NOT:
"temp_strengthening P Q h ⟹ temp_weakening (¬ P) (¬ Q) h"
by (auto simp add: temp_weakening_def2 temp_strengthening_def)

lemma weak_IMPLIES:
"temp_strengthening P1 Q1 h ⟹ temp_weakening P2 Q2 h ⟹
temp_weakening (P1  P2) (Q1  Q2) h"

subsubsection ‹Box›

(* 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 ∧ y = UU))"
by (Seq_case_simp x)

lemma ex2seqConc [rule_format]:
"Finite s1 ⟶ (∀ex. (s ≠ nil ∧ s ≠ UU ∧ ex2seq ex = s1 @@ s) ⟶ (∃ex'. s = ex2seq ex'))"
apply (rule impI)
apply Seq_Finite_induct
apply blast
text ‹main case›
apply clarify
apply (pair ex)
apply (Seq_case_simp x2)
text ‹‹UU› case›
text ‹‹nil› case›
text ‹cons case›
apply (pair aa)
apply auto
done

(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
lemma ex2seq_tsuffix: "tsuffix s (ex2seq ex) ⟹ ∃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 ⟹ tsuffix (cex_absSeq h s) (cex_absSeq h t)"
apply (unfold tsuffix_def suffix_def cex_absSeq_def)
apply auto
apply (rule_tac x = "Map (% (s,a,t) . (h s,a, h t))⋅s1" in exI)
done

lemma strength_Box: "temp_strengthening P Q h ⟹ temp_strengthening (□P) (□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)
done

subsubsection ‹Init›

lemma strength_Init:
"state_strengthening P Q h ⟹ 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 ‹Next›

lemma TL_ex2seq_UU: "TL ⋅ (ex2seq (cex_abs h ex)) = UU ⟷ TL ⋅ (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 ⋅ (ex2seq (cex_abs h ex)) = nil ⟷ TL ⋅ (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 ⋅ s) = TL ⋅ (cex_absSeq h s)"

(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
lemma TLex2seq: "snd ex ≠ UU ⟹ snd ex ≠ nil ⟹ ∃ex'. TL⋅(ex2seq ex) = ex2seq ex'"
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
apply auto
done

lemma ex2seqnilTL: "TL ⋅ (ex2seq ex) ≠ nil ⟷ snd ex ≠ nil ∧ snd ex ≠ 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 ⟹ temp_strengthening (○P) (○Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
apply simp
apply auto
text ‹cons case›
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 ‹Localizing Temporal Weakenings - 2›

lemma weak_Init: "state_weakening P Q h ⟹ temp_weakening (Init P) (Init Q) h"
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
apply (pair ex)
apply (Seq_case_simp x2)
apply (pair a)
done

text ‹Localizing Temproal Strengthenings - 3›

lemma strength_Diamond: "temp_strengthening P Q h ⟹ temp_strengthening (◇P) (◇Q) h"
apply (unfold Diamond_def)
apply (rule strength_NOT)
apply (rule weak_Box)
apply (erule weak_NOT)
done

"temp_weakening P1 P2 h ⟹ temp_strengthening Q1 Q2 h ⟹
temp_strengthening (P1 ↝ Q1) (P2 ↝ Q2) h"
apply (rule strength_Box)
apply (erule strength_IMPLIES)
apply (erule strength_Diamond)
done

text ‹Localizing Temporal Weakenings - 3›

lemma weak_Diamond: "temp_weakening P Q h ⟹ temp_weakening (◇P) (◇Q) h"
apply (unfold Diamond_def)
apply (rule weak_NOT)
apply (rule strength_Box)
apply (erule strength_NOT)
done

"temp_strengthening P1 P2 h ⟹ temp_weakening Q1 Q2 h ⟹
temp_weakening (P1 ↝ Q1) (P2 ↝ Q2) h"
apply (rule weak_Box)
apply (erule weak_IMPLIES)
apply (erule weak_Diamond)
done

lemma weak_WF:
"(⋀s. Enabled A acts (h s) ⟹ Enabled C acts s)
⟹ 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:
"(⋀s. Enabled A acts (h s) ⟹ Enabled C acts s)
⟹ 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