Theory Fair_Otter_Loop_Def
section ‹Definition of Fair Otter Loop›
text ‹The fair Otter loop assumes that the passive queue is fair and ensures
(dynamic) refutational completeness under that assumption. This section contains
only the loop's definition.›
theory Fair_Otter_Loop_Def
imports
Otter_Loop
Prover_Queue
begin
subsection ‹Locale›
type_synonym ('p, 'f) OLf_state = "'f fset × 'f option × 'p × 'f option × 'f fset"
locale fair_otter_loop =
otter_loop Bot_F Inf_F Bot_G Q entails_q Inf_G_q Red_I_q Red_F_q 𝒢_F_q 𝒢_I_q Equiv_F Prec_F +
fair_prover_queue empty select add remove felems
for
Bot_F :: "'f set" and
Inf_F :: "'f inference set" and
Bot_G :: "'g set" and
Q :: "'q set" and
entails_q :: "'q ⇒ 'g set ⇒ 'g set ⇒ bool" and
Inf_G_q :: "'q ⇒ 'g inference set" and
Red_I_q :: "'q ⇒ 'g set ⇒ 'g inference set" and
Red_F_q :: "'q ⇒ 'g set ⇒ 'g set" and
𝒢_F_q :: "'q ⇒ 'f ⇒ 'g set" and
𝒢_I_q :: "'q ⇒ 'f inference ⇒ 'g inference set option" and
Equiv_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≐› 50) and
Prec_F :: "'f ⇒ 'f ⇒ bool" (infix ‹≺⋅› 50) and
empty :: "'p" and
select :: "'p ⇒ 'f" and
add :: "'f ⇒ 'p ⇒ 'p" and
remove :: "'f ⇒ 'p ⇒ 'p" and
felems :: "'p ⇒ 'f fset" +
fixes
Prec_S :: "'f ⇒ 'f ⇒ bool" (infix "≺S" 50)
assumes
wf_Prec_S: "minimal_element (≺S) UNIV" and
transp_Prec_S: "transp (≺S)" and
finite_Inf_between: "finite A ⟹ finite (no_labels.Inf_between A {C})"
begin
lemma trans_Prec_S: "trans {(x, y). x ≺S y}"
using transp_Prec_S transp_trans by blast
lemma irreflp_Prec_S: "irreflp (≺S)"
using minimal_element.wf wfP_imp_irreflp wf_Prec_S wfp_on_UNIV by blast
lemma irrefl_Prec_S: "irrefl {(x, y). x ≺S y}"
by (metis CollectD case_prod_conv irrefl_def irreflp_Prec_S irreflp_def)
subsection ‹Basic Definitions and Lemmas›
abbreviation new_of :: "('p, 'f) OLf_state ⇒ 'f fset" where
"new_of St ≡ fst St"
abbreviation xx_of :: "('p, 'f) OLf_state ⇒ 'f option" where
"xx_of St ≡ fst (snd St)"
abbreviation passive_of :: "('p, 'f) OLf_state ⇒ 'p" where
"passive_of St ≡ fst (snd (snd St))"
abbreviation yy_of :: "('p, 'f) OLf_state ⇒ 'f option" where
"yy_of St ≡ fst (snd (snd (snd St)))"
abbreviation active_of :: "('p, 'f) OLf_state ⇒ 'f fset" where
"active_of St ≡ snd (snd (snd (snd St)))"
abbreviation all_formulas_of :: "('p, 'f) OLf_state ⇒ 'f set" where
"all_formulas_of St ≡ fset (new_of St) ∪ set_option (xx_of St) ∪ elems (passive_of St) ∪
set_option (yy_of St) ∪ fset (active_of St)"
fun fstate :: "'f fset × 'f option × 'p × 'f option × 'f fset ⇒ ('f × OL_label) set" where
"fstate (N, X, P, Y, A) = state (fset N, set_option X, elems P, set_option Y, fset A)"
lemma fstate_alt_def:
"fstate St =
state (fset (fst St), set_option (fst (snd St)), elems (fst (snd (snd St))),
set_option (fst (snd (snd (snd St)))), fset (snd (snd (snd (snd St)))))"
by (cases St) auto
definition
Liminf_fstate :: "('p, 'f) OLf_state llist ⇒ 'f set × 'f set × 'f set × 'f set × 'f set"
where
"Liminf_fstate Sts =
(Liminf_llist (lmap (fset ∘ new_of) Sts),
Liminf_llist (lmap (set_option ∘ xx_of) Sts),
Liminf_llist (lmap (elems ∘ passive_of) Sts),
Liminf_llist (lmap (set_option ∘ yy_of) Sts),
Liminf_llist (lmap (fset ∘ active_of) Sts))"
lemma Liminf_fstate_commute: "Liminf_llist (lmap fstate Sts) = state (Liminf_fstate Sts)"
proof -
have "Liminf_llist (lmap fstate Sts) =
(λC. (C, New)) ` Liminf_llist (lmap (fset ∘ new_of) Sts) ∪
(λC. (C, XX)) ` Liminf_llist (lmap (set_option ∘ xx_of) Sts) ∪
(λC. (C, Passive)) ` Liminf_llist (lmap (elems ∘ passive_of) Sts) ∪
(λC. (C, YY)) ` Liminf_llist (lmap (set_option ∘ yy_of) Sts) ∪
(λC. (C, Active)) ` Liminf_llist (lmap (fset ∘ active_of) Sts)"
unfolding fstate_alt_def state_alt_def
apply (subst Liminf_llist_lmap_union, fast)+
apply (subst Liminf_llist_lmap_image, simp add: inj_on_convol_ident)+
by auto
thus ?thesis
unfolding Liminf_fstate_def by fastforce
qed
fun state_union :: "'f set × 'f set × 'f set × 'f set × 'f set ⇒ 'f set" where
"state_union (N, X, P, Y, A) = N ∪ X ∪ P ∪ Y ∪ A"
inductive fair_OL :: "('p, 'f) OLf_state ⇒ ('p, 'f) OLf_state ⇒ bool" (infix "↝OLf" 50) where
choose_n: "C |∉| N ⟹ (N |∪| {|C|}, None, P, None, A) ↝OLf (N, Some C, P, None, A)"
| delete_fwd: "C ∈ no_labels.Red_F (elems P ∪ fset A) ∨ (∃C' ∈ elems P ∪ fset A. C' ≼⋅ C) ⟹
(N, Some C, P, None, A) ↝OLf (N, None, P, None, A)"
| simplify_fwd: "C' ≺S C ⟹ C ∈ no_labels.Red_F (elems P ∪ fset A ∪ {C'}) ⟹
(N, Some C, P, None, A) ↝OLf (N, Some C', P, None, A)"
| delete_bwd_p: "C' ∈ elems P ⟹ C' ∈ no_labels.Red_F {C} ∨ C ≺⋅ C' ⟹
(N, Some C, P, None, A) ↝OLf (N, Some C, remove C' P, None, A)"
| simplify_bwd_p: "C'' ≺S C' ⟹ C' ∈ elems P ⟹ C' ∈ no_labels.Red_F {C, C''} ⟹
(N, Some C, P, None, A) ↝OLf (N |∪| {|C''|}, Some C, remove C' P, None, A)"
| delete_bwd_a: "C' |∉| A ⟹ C' ∈ no_labels.Red_F {C} ∨ C ≺⋅ C' ⟹
(N, Some C, P, None, A |∪| {|C'|}) ↝OLf (N, Some C, P, None, A)"
| simplify_bwd_a: "C'' ≺S C' ⟹ C' |∉| A ⟹ C' ∈ no_labels.Red_F {C, C''} ⟹
(N, Some C, P, None, A |∪| {|C'|}) ↝OLf (N |∪| {|C''|}, Some C, P, None, A)"
| transfer: "(N, Some C, P, None, A) ↝OLf (N, None, add C P, None, A)"
| choose_p: "P ≠ empty ⟹
({||}, None, P, None, A) ↝OLf ({||}, None, remove (select P) P, Some (select P), A)"
| infer: "no_labels.Inf_between (fset A) {C} ⊆ no_labels.Red_I (fset A ∪ {C} ∪ fset M) ⟹
({||}, None, P, Some C, A) ↝OLf (M, None, P, None, A |∪| {|C|})"
subsection ‹Initial State and Invariant›
inductive is_initial_OLf_state :: "('p, 'f) OLf_state ⇒ bool" where
"is_initial_OLf_state (N, None, empty, None, {||})"
inductive OLf_invariant :: "('p, 'f) OLf_state ⇒ bool" where
"(N = {||} ∧ X = None) ∨ Y = None ⟹ OLf_invariant (N, X, P, Y, A)"
lemma initial_OLf_invariant: "is_initial_OLf_state St ⟹ OLf_invariant St"
unfolding is_initial_OLf_state.simps OLf_invariant.simps by auto
lemma step_OLf_invariant:
assumes step: "St ↝OLf St'"
shows "OLf_invariant St'"
using step by cases (auto intro: OLf_invariant.intros)
lemma chain_OLf_invariant_lnth:
assumes
chain: "chain (↝OLf) Sts" and
fair_hd: "OLf_invariant (lhd Sts)" and
i_lt: "enat i < llength Sts"
shows "OLf_invariant (lnth Sts i)"
using i_lt
proof (induct i)
case 0
thus ?case
using fair_hd lhd_conv_lnth zero_enat_def by fastforce
next
case (Suc i)
thus ?case
using chain chain_lnth_rel step_OLf_invariant by blast
qed
lemma chain_OLf_invariant_llast:
assumes
chain: "chain (↝OLf) Sts" and
fair_hd: "OLf_invariant (lhd Sts)" and
fin: "lfinite Sts"
shows "OLf_invariant (llast Sts)"
proof -
obtain i :: nat where
i: "llength Sts = enat i"
using lfinite_llength_enat[OF fin] by blast
have im1_lt: "enat (i - 1) < llength Sts"
using i by (metis chain chain_length_pos diff_less enat_ord_simps(2) less_numeral_extra(1)
zero_enat_def)
show ?thesis
using chain_OLf_invariant_lnth[OF chain fair_hd im1_lt]
by (metis Suc_diff_1 chain chain_length_pos eSuc_enat enat_ord_simps(2) i llast_conv_lnth
zero_enat_def)
qed
subsection ‹Final State›
inductive is_final_OLf_state :: "('p, 'f) OLf_state ⇒ bool" where
"is_final_OLf_state ({||}, None, empty, None, A)"
lemma is_final_OLf_state_iff_no_OLf_step:
assumes inv: "OLf_invariant St"
shows "is_final_OLf_state St ⟷ (∀St'. ¬ St ↝OLf St')"
proof
assume "is_final_OLf_state St"
then obtain A :: "'f fset" where
st: "St = ({||}, None, empty, None, A)"
by (auto simp: is_final_OLf_state.simps)
show "∀St'. ¬ St ↝OLf St'"
unfolding st
proof (intro allI notI)
fix St'
assume "({||}, None, empty, None, A) ↝OLf St'"
thus False
by cases auto
qed
next
assume no_step: "∀St'. ¬ St ↝OLf St'"
show "is_final_OLf_state St"
proof (rule ccontr)
assume not_fin: "¬ is_final_OLf_state St"
obtain N A :: "'f fset" and X Y :: "'f option" and P :: 'p where
st: "St = (N, X, P, Y, A)"
by (cases St)
have inv': "(N = {||} ∧ X = None) ∨ Y = None"
using inv st OLf_invariant.simps by simp
have "N ≠ {||} ∨ X ≠ None ∨ P ≠ empty ∨ Y ≠ None"
using not_fin unfolding st is_final_OLf_state.simps by auto
moreover {
assume
n: "N ≠ {||}" and
x: "X = None"
obtain N' :: "'f fset" and C :: 'f where
n': "N = N' |∪| {|C|}" and
c_ni: "C |∉| N'"
using n finsert_is_funion by blast
have y: "Y = None"
using n x inv' by meson
have "∃St'. St ↝OLf St'"
using fair_OL.choose_n[OF c_ni] unfolding st n' x y by fast
} moreover {
assume "X ≠ None"
then obtain C :: 'f where
x: "X = Some C"
by blast
have y: "Y = None"
using x inv' by auto
have "∃St'. St ↝OLf St'"
using fair_OL.transfer unfolding st x y by fast
} moreover {
assume
p: "P ≠ empty" and
n: "N = {||}" and
x: "X = None" and
y: "Y = None"
have "∃St'. St ↝OLf St'"
using fair_OL.choose_p[OF p] unfolding st n x y by fast
} moreover {
assume "Y ≠ None"
then obtain C :: 'f where
y: "Y = Some C"
by blast
have n: "N = {||}" and
x: "X = None"
using y inv' by blast+
let ?M = "concl_of ` no_labels.Inf_between (fset A) {C}"
have fin: "finite ?M"
by (simp add: finite_Inf_between)
have fset_abs_m: "fset (Abs_fset ?M) = ?M"
by (rule Abs_fset_inverse[simplified, OF fin])
have inf_red: "no_labels.Inf_between (fset A) {C}
⊆ no_labels.Red_I_𝒢 (fset A ∪ {C} ∪ fset (Abs_fset ?M))"
by (simp add: fset_abs_m no_labels.Inf_if_Inf_between no_labels.empty_ord.Red_I_of_Inf_to_N
subsetI)
have "∃St'. St ↝OLf St'"
using fair_OL.infer[OF inf_red] unfolding st n x y by fast
} ultimately show False
using no_step by force
qed
qed
subsection ‹Refinement›
lemma fair_OL_step_imp_OL_step:
assumes olf: "(N, X, P, Y, A) ↝OLf (N', X', P', Y', A')"
shows "fstate (N, X, P, Y, A) ↝OL fstate (N', X', P', Y', A')"
using olf
proof cases
case (choose_n C)
note defs = this(1-7) and c_ni = this(8)
show ?thesis
unfolding defs fstate.simps option.set using OL.choose_n c_ni by simp
next
case (delete_fwd C)
note defs = this(1-7) and c_red = this(8)
show ?thesis
unfolding defs fstate.simps option.set by (rule OL.delete_fwd[OF c_red])
next
case (simplify_fwd C' C)
note defs = this(1-7) and c_red = this(9)
show ?thesis
unfolding defs fstate.simps option.set by (rule OL.simplify_fwd[OF c_red])
next
case (delete_bwd_p C' C)
note defs = this(1-7) and c'_in_p = this(8) and c'_red = this(9)
have p_rm_c'_uni_c': "elems (remove C' P) ∪ {C'} = elems P"
unfolding felems_remove by (auto intro: c'_in_p)
have p_mns_c': "elems P - {C'} = elems (remove C' P)"
unfolding felems_remove by auto
show ?thesis
unfolding defs fstate.simps option.set
by (rule OL.delete_bwd_p[OF c'_red, of _ "elems P - {C'}",
unfolded p_rm_c'_uni_c' p_mns_c'])
next
case (simplify_bwd_p C'' C' C)
note defs = this(1-7) and c'_in_p = this(9) and c'_red = this(10)
have p_rm_c'_uni_c': "elems (remove C' P) ∪ {C'} = elems P"
unfolding felems_remove by (auto intro: c'_in_p)
have p_mns_c': "elems P - {C'} = elems (remove C' P)"
unfolding felems_remove by auto
show ?thesis
unfolding defs fstate.simps option.set
using OL.simplify_bwd_p[OF c'_red, of "fset N" "elems P - {C'}",
unfolded p_rm_c'_uni_c' p_mns_c']
by simp
next
case (delete_bwd_a C' C)
note defs = this(1-7) and c'_red = this(9)
show ?thesis
unfolding defs fstate.simps option.set using OL.delete_bwd_a[OF c'_red] by simp
next
case (simplify_bwd_a C' C'' C)
note defs = this(1-7) and c'_red = this(10)
show ?thesis
unfolding defs fstate.simps option.set using OL.simplify_bwd_a[OF c'_red] by simp
next
case (transfer C)
note defs = this(1-7)
have p_uni_c: "elems P ∪ {C} = elems (add C P)"
using felems_add by auto
show ?thesis
unfolding defs fstate.simps option.set
by (rule OL.transfer[of _ C "elems P", unfolded p_uni_c])
next
case choose_p
note defs = this(1-8) and p_nemp = this(9)
have sel_ni_rm: "select P ∉ elems (remove (select P) P)"
unfolding felems_remove by auto
have rm_sel_uni_sel: "elems (remove (select P) P) ∪ {select P} = elems P"
unfolding felems_remove using p_nemp select_in_felems
by (metis Un_insert_right finsert.rep_eq finsert_fminus sup_bot_right)
show ?thesis
unfolding defs fstate.simps option.set
using OL.choose_p[of "select P" "elems (remove (select P) P)", OF sel_ni_rm,
unfolded rm_sel_uni_sel]
by simp
next
case (infer C)
note defs = this(1-7) and infers = this(8)
show ?thesis
unfolding defs fstate.simps option.set using OL.infer[OF infers] by simp
qed
lemma fair_OL_step_imp_GC_step:
"(N, X, P, Y, A) ↝OLf (N', X', P', Y', A') ⟹
fstate (N, X, P, Y, A) ↝GC fstate (N', X', P', Y', A')"
by (rule OL_step_imp_GC_step[OF fair_OL_step_imp_OL_step])
end
end