Theory FOR_Check
theory FOR_Check
imports
FOR_Semantics
FOL_Extra
GTT_RRn
First_Order_Terms.Option_Monad
LV_to_GTT
NF
Regular_Tree_Relations.GTT_Transitive_Closure
Regular_Tree_Relations.AGTT
Regular_Tree_Relations.RR2_Infinite_Q_infinity
Regular_Tree_Relations.RRn_Automata
begin
section ‹Check inference steps›
type_synonym ('f, 'v) fin_trs = "('f, 'v) rule fset"
lemma tl_drop_conv:
"tl xs = drop 1 xs"
by (induct xs) auto
definition rrn_drop_fst where
"rrn_drop_fst 𝒜 = relabel_reg (trim_reg (collapse_automaton_reg (fmap_funs_reg (drop_none_rule 1) (trim_reg 𝒜))))"
lemma rrn_drop_fst_lang:
assumes "RRn_spec n A T" "1 < n"
shows "RRn_spec (n - 1) (rrn_drop_fst A) (drop 1 ` T)"
using drop_automaton_reg[OF _ assms(2), of "trim_reg A" T] assms(1)
unfolding rrn_drop_fst_def
by (auto simp: trim_ta_reach)
definition liftO1 :: "('a ⇒ 'b) ⇒ 'a option ⇒ 'b option" where
"liftO1 = map_option"
definition liftO2 :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a option ⇒ 'b option ⇒ 'c option" where
"liftO2 f a b = case_option None (λa'. liftO1 (f a') b) a"
lemma liftO1_Some [simp]:
"liftO1 f x = Some y ⟷ (∃x'. x = Some x') ∧ y = f (the x)"
by (cases x) (auto simp: liftO1_def)
lemma liftO2_Some [simp]:
"liftO2 f x y = Some z ⟷ (∃x' y'. x = Some x' ∧ y = Some y') ∧ z = f (the x) (the y)"
by (cases x; cases y) (auto simp: liftO2_def)
subsection ‹Computing TRSs›
lemma is_to_trs_props:
assumes "∀ R ∈ set Rs. finite R ∧ lv_trs R ∧ funas_trs R ⊆ ℱ" "∀i ∈ set is. case_ftrs id id i < length Rs"
shows "funas_trs (is_to_trs Rs is) ⊆ ℱ" "lv_trs (is_to_trs Rs is)" "finite (is_to_trs Rs is)"
proof (goal_cases ℱ lv fin)
case ℱ show ?case using assms nth_mem
apply (auto simp: is_to_trs_def funas_trs_def case_prod_beta split: ftrs.splits)
apply fastforce
apply (metis (no_types, lifting) assms(1) in_mono rhs_wf)
apply (metis (no_types, lifting) assms(1) in_mono rhs_wf)
by (smt (z3) UN_subset_iff fst_conv in_mono le_sup_iff)
qed (insert assms, (fastforce simp: is_to_trs_def funas_trs_def lv_trs_def split: ftrs.splits)+)
definition is_to_fin_trs :: "('f, 'v) fin_trs list ⇒ ftrs list ⇒ ('f, 'v) fin_trs" where
"is_to_fin_trs Rs is = |⋃| (fset_of_list (map (case_ftrs ((!) Rs) ((|`|) prod.swap ∘ (!) Rs)) is))"
lemma is_to_fin_trs_conv:
assumes "∀i ∈ set is. case_ftrs id id i < length Rs"
shows "is_to_trs (map fset Rs) is = fset (is_to_fin_trs Rs is)"
using assms unfolding is_to_trs_def is_to_fin_trs_def
by (auto simp: ffUnion.rep_eq fset_of_list.rep_eq split: ftrs.splits)
definition is_to_trs' :: "('f, 'v) fin_trs list ⇒ ftrs list ⇒ ('f, 'v) fin_trs option" where
"is_to_trs' Rs is = do {
guard (∀i ∈ set is. case_ftrs id id i < length Rs);
Some (is_to_fin_trs Rs is)
}"
lemma is_to_trs_conv:
"is_to_trs' Rs is = Some S ⟹ is_to_trs (map fset Rs) is = fset S"
using is_to_fin_trs_conv unfolding is_to_trs'_def
by (auto simp add: guard_simps split: bind_splits)
lemma is_to_trs'_props:
assumes "∀ R ∈ set Rs. lv_trs (fset R) ∧ ffunas_trs R |⊆| ℱ" and "is_to_trs' Rs is = Some S"
shows "ffunas_trs S |⊆| ℱ" "lv_trs (fset S)"
proof -
from assms(2) have well: "∀i ∈ set is. case_ftrs id id i < length Rs" "is_to_fin_trs Rs is = S"
unfolding is_to_trs'_def
by (auto simp add: guard_simps split: bind_splits)
have "∀ R ∈ set Rs. finite (fset R) ∧ lv_trs (fset R) ∧ funas_trs (fset R) ⊆ (fset ℱ)"
using assms(1) by (auto simp: ffunas_trs.rep_eq less_eq_fset.rep_eq)
from is_to_trs_props[of "map fset Rs" "fset ℱ" "is"] this well(1)
have "lv_trs (is_to_trs (map fset Rs) is)" "funas_trs (is_to_trs (map fset Rs) is) ⊆ fset ℱ"
by auto
then show "lv_trs (fset S)" "ffunas_trs S |⊆| ℱ"
using is_to_fin_trs_conv[OF well(1)] unfolding well(2)
by (auto simp: ffunas_trs.rep_eq less_eq_fset.rep_eq)
qed
subsection ‹Computing GTTs›
fun gtt_of_gtt_rel :: "('f × nat) fset ⇒ ('f :: linorder, 'v) fin_trs list ⇒ ftrs gtt_rel ⇒ (nat, 'f) gtt option" where
"gtt_of_gtt_rel ℱ Rs (ARoot is) = liftO1 (λR. relabel_gtt (agtt_grrstep R ℱ)) (is_to_trs' Rs is)"
| "gtt_of_gtt_rel ℱ Rs (GInv g) = liftO1 prod.swap (gtt_of_gtt_rel ℱ Rs g)"
| "gtt_of_gtt_rel ℱ Rs (AUnion g1 g2) = liftO2 (λg1 g2. relabel_gtt (AGTT_union' g1 g2)) (gtt_of_gtt_rel ℱ Rs g1) (gtt_of_gtt_rel ℱ Rs g2)"
| "gtt_of_gtt_rel ℱ Rs (ATrancl g) = liftO1 (relabel_gtt ∘ AGTT_trancl) (gtt_of_gtt_rel ℱ Rs g)"
| "gtt_of_gtt_rel ℱ Rs (GTrancl g) = liftO1 GTT_trancl (gtt_of_gtt_rel ℱ Rs g)"
| "gtt_of_gtt_rel ℱ Rs (AComp g1 g2) = liftO2 (λg1 g2. relabel_gtt (AGTT_comp' g1 g2)) (gtt_of_gtt_rel ℱ Rs g1) (gtt_of_gtt_rel ℱ Rs g2)"
| "gtt_of_gtt_rel ℱ Rs (GComp g1 g2) = liftO2 (λg1 g2. relabel_gtt (GTT_comp' g1 g2)) (gtt_of_gtt_rel ℱ Rs g1) (gtt_of_gtt_rel ℱ Rs g2)"
lemma gtt_of_gtt_rel_correct:
assumes "∀R ∈ set Rs. lv_trs (fset R) ∧ ffunas_trs R |⊆| ℱ"
shows "gtt_of_gtt_rel ℱ Rs g = Some g' ⟹ agtt_lang g' = eval_gtt_rel (fset ℱ) (map fset Rs) g"
proof (induct g arbitrary: g')
note [simp] = bind_eq_Some_conv guard_simps
have proj_sq: "fst ` (X × X) = X" "snd ` (X × X) = X" for X by auto
{
case (ARoot "is")
then obtain w where w:"is_to_trs' Rs is = Some w" by auto
then show ?case using ARoot is_to_trs'_props[OF assms w] is_to_trs_conv[OF w]
using agtt_grrstep
by auto
next
case (GInv g) then show ?case by (simp add: agtt_lang_swap gtt_states_def)
next
case (AUnion g1 g2)
from AUnion(3)[simplified, THEN conjunct1] AUnion(3)[simplified, THEN conjunct2, THEN conjunct1]
obtain w1 w2 where
[simp]: "gtt_of_gtt_rel ℱ Rs g1 = Some w1" "gtt_of_gtt_rel ℱ Rs g2 = Some w2"
by blast
then show ?case using AUnion(3)
by (simp add: AGTT_union'_sound AUnion)
next
case (ATrancl g)
from ATrancl[simplified] obtain w1 where
[simp]: "gtt_of_gtt_rel ℱ Rs g = Some w1" "g' = relabel_gtt (AGTT_trancl w1)" by auto
then have fin_lang: "eval_gtt_rel (fset ℱ) (map fset Rs) g = agtt_lang w1"
using ATrancl by auto
from fin_lang show ?case using AGTT_trancl_sound[of w1]
by auto
next
case (GTrancl g) note * = GTrancl(2)[simplified, THEN conjunct2]
show ?case unfolding gtt_of_gtt_rel.simps GTT_trancl_alang * gtrancl_rel_def eval_gtt_rel.simps gmctxt_cl_gmctxtex_onp_conv
proof ((intro conjI equalityI subrelI; (elim relcompE)?), goal_cases LR RL)
case (LR _ _ s _ z s' t' t)
show ?case using lift_root_steps_sig_transfer'[OF LR(2)[folded lift_root_step.simps], of "fset ℱ"]
lift_root_steps_sig_transfer[OF LR(5)[folded lift_root_step.simps], of "fset ℱ"]
image_mono[OF eval_gtt_rel_sig[of "fset ℱ" "map fset Rs" g], of fst, unfolded proj_sq]
image_mono[OF eval_gtt_rel_sig[of "fset ℱ" "map fset Rs" g], of snd, unfolded proj_sq]
subsetD[OF eval_gtt_rel_sig[of "fset ℱ" "map fset Rs" g]] LR(1, 3, 4) GTrancl
by (intro relcompI[OF _ relcompI, of _ s' _ t' _])
(auto simp: 𝒯⇩G_funas_gterm_conv lift_root_step.simps)
next
case (RL _ _ s _ z s' t' t)
then show ?case using GTrancl
lift_root_step_mono[of "fset ℱ" UNIV PAny ESingle "eval_gtt_rel (fset ℱ) (map fset Rs) g", THEN rtrancl_mono]
unfolding lift_root_step.simps[symmetric]
by (intro relcompI[OF _ relcompI, of _ s' _ t' _])
(auto simp: 𝒯⇩G_funas_gterm_conv lift_root_step_mono trancl_mono)
qed
next
case (AComp g1 g2)
from AComp[simplified] obtain w1 w2 where
[simp]: "gtt_of_gtt_rel ℱ Rs g1 = Some w1" "gtt_of_gtt_rel ℱ Rs g2 = Some w2"
"g' = relabel_gtt (AGTT_comp' w1 w2)" by auto
then have fin_lang: "eval_gtt_rel (fset ℱ) (map fset Rs) g1 = agtt_lang w1"
"eval_gtt_rel (fset ℱ) (map fset Rs) g2 = agtt_lang w2"
using AComp by auto
from fin_lang AGTT_comp'_sound[of w1 w2]
show ?case by simp
next
case (GComp g1 g2)
let ?r = "λ g. eval_gtt_rel (fset ℱ) (map fset Rs) g"
have *: "gmctxtex_onp (λC. True) (?r g1) = lift_root_step UNIV PAny EParallel (?r g1)"
"gmctxtex_onp (λC. True) (?r g2) = lift_root_step UNIV PAny EParallel (?r g2)"
by (auto simp: lift_root_step.simps)
show ?case using GComp(3)
apply (intro conjI equalityI subrelI; simp add: gmctxt_cl_gmctxtex_onp_conv GComp(1,2) gtt_comp'_alang gcomp_rel_def * flip: lift_root_step.simps; elim conjE disjE exE relcompE)
subgoal for s t _ _ _ _ _ u
using image_mono[OF eval_gtt_rel_sig, of snd "fset ℱ" "map fset Rs", unfolded proj_sq]
apply (subst relcompI[of _ u "eval_gtt_rel _ _ g1", OF _ lift_root_step_sig_transfer[of _ UNIV PAny EParallel "_ g2" "fset ℱ"]])
apply (force simp add: subsetI 𝒯⇩G_equivalent_def)+
done
subgoal for s t _ _ _ _ _ u
using image_mono[OF eval_gtt_rel_sig, of fst "fset ℱ" "map fset Rs", unfolded proj_sq]
apply (subst relcompI[of _ u _ _ "eval_gtt_rel _ _ g2", OF lift_root_step_sig_transfer'[of _ UNIV PAny EParallel "_ g1" "fset ℱ"]])
apply (force simp add: subsetI 𝒯⇩G_equivalent_def)+
done
by (auto intro: subsetD[OF lift_root_step_mono[of "fset ℱ" UNIV]])
}
qed
subsection ‹Computing RR1 and RR2 relations›
definition "simplify_reg 𝒜 = (relabel_reg (trim_reg 𝒜))"
lemma ℒ_simplify_reg [simp]: "ℒ (simplify_reg 𝒜) = ℒ 𝒜"
by (simp add: simplify_reg_def ℒ_trim)
lemma RR1_spec_simplify_reg[simp]:
"RR1_spec (simplify_reg 𝒜) R = RR1_spec 𝒜 R"
by (auto simp: RR1_spec_def)
lemma RR2_spec_simplify_reg[simp]:
"RR2_spec (simplify_reg 𝒜) R = RR2_spec 𝒜 R"
by (auto simp: RR2_spec_def)
lemma RRn_spec_simplify_reg[simp]:
"RRn_spec n (simplify_reg 𝒜) R = RRn_spec n 𝒜 R"
by (auto simp: RRn_spec_def)
lemma RR1_spec_eps_free_reg[simp]:
"RR1_spec (eps_free_reg 𝒜) R = RR1_spec 𝒜 R"
by (auto simp: RR1_spec_def ℒ_eps_free)
lemma RR2_spec_eps_free_reg[simp]:
"RR2_spec (eps_free_reg 𝒜) R = RR2_spec 𝒜 R"
by (auto simp: RR2_spec_def ℒ_eps_free)
lemma RRn_spec_eps_free_reg[simp]:
"RRn_spec n (eps_free_reg 𝒜) R = RRn_spec n 𝒜 R"
by (auto simp: RRn_spec_def ℒ_eps_free)
fun rr1_of_rr1_rel :: "('f × nat) fset ⇒ ('f :: linorder, 'v) fin_trs list ⇒ ftrs rr1_rel ⇒ (nat, 'f) reg option"
and rr2_of_rr2_rel :: "('f × nat) fset ⇒ ('f, 'v) fin_trs list ⇒ ftrs rr2_rel ⇒ (nat, 'f option × 'f option) reg option" where
"rr1_of_rr1_rel ℱ Rs R1Terms = Some (relabel_reg (term_reg ℱ))"
| "rr1_of_rr1_rel ℱ Rs (R1NF is) = liftO1 (λR. (simplify_reg (nf_reg (fst |`| R) ℱ))) (is_to_trs' Rs is)"
| "rr1_of_rr1_rel ℱ Rs (R1Inf r) = liftO1 (λR.
let 𝒜 = trim_reg R in
simplify_reg (proj_1_reg (Inf_reg_impl 𝒜))
) (rr2_of_rr2_rel ℱ Rs r)"
| "rr1_of_rr1_rel ℱ Rs (R1Proj i r) = (case i of 0 ⇒
liftO1 (trim_reg ∘ proj_1_reg) (rr2_of_rr2_rel ℱ Rs r)
| _ ⇒ liftO1 (trim_reg ∘ proj_2_reg) (rr2_of_rr2_rel ℱ Rs r))"
| "rr1_of_rr1_rel ℱ Rs (R1Union s1 s2) =
liftO2 (λ x y. relabel_reg (reg_union x y)) (rr1_of_rr1_rel ℱ Rs s1) (rr1_of_rr1_rel ℱ Rs s2)"
| "rr1_of_rr1_rel ℱ Rs (R1Inter s1 s2) =
liftO2 (λ x y. simplify_reg (reg_intersect x y)) (rr1_of_rr1_rel ℱ Rs s1) (rr1_of_rr1_rel ℱ Rs s2)"
| "rr1_of_rr1_rel ℱ Rs (R1Diff s1 s2) = liftO2 (λ x y. relabel_reg (trim_reg (difference_reg x y))) (rr1_of_rr1_rel ℱ Rs s1) (rr1_of_rr1_rel ℱ Rs s2)"
| "rr2_of_rr2_rel ℱ Rs (R2GTT_Rel g w x) =
(case w of PRoot ⇒
(case x of ESingle ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)
| EParallel ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ reflcl_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)
| EStrictParallel ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g))
| PNonRoot ⇒
(case x of ESingle ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ nhole_ctxt_closure_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)
| EParallel ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ nhole_mctxt_reflcl_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)
| EStrictParallel ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ nhole_mctxt_closure_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g))
| PAny ⇒
(case x of ESingle ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ ctxt_closure_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)
| EParallel ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ parallel_closure_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)
| EStrictParallel ⇒ liftO1 (simplify_reg ∘ eps_free_reg ∘ mctxt_closure_reg (lift_sig_RR2 |`| ℱ) ∘ GTT_to_RR2_root_reg) (gtt_of_gtt_rel ℱ Rs g)))"
| "rr2_of_rr2_rel ℱ Rs (R2Diag s) =
liftO1 (λ x. fmap_funs_reg (λf. (Some f, Some f)) x) (rr1_of_rr1_rel ℱ Rs s)"
| "rr2_of_rr2_rel ℱ Rs (R2Prod s1 s2) =
liftO2 (λ x y. simplify_reg (pair_automaton_reg x y)) (rr1_of_rr1_rel ℱ Rs s1) (rr1_of_rr1_rel ℱ Rs s2)"
| "rr2_of_rr2_rel ℱ Rs (R2Inv r) = liftO1 (fmap_funs_reg prod.swap) (rr2_of_rr2_rel ℱ Rs r)"
| "rr2_of_rr2_rel ℱ Rs (R2Union r1 r2) =
liftO2 (λ x y. relabel_reg (reg_union x y)) (rr2_of_rr2_rel ℱ Rs r1) (rr2_of_rr2_rel ℱ Rs r2)"
| "rr2_of_rr2_rel ℱ Rs (R2Inter r1 r2) =
liftO2 (λ x y. simplify_reg (reg_intersect x y)) (rr2_of_rr2_rel ℱ Rs r1) (rr2_of_rr2_rel ℱ Rs r2)"
| "rr2_of_rr2_rel ℱ Rs (R2Diff r1 r2) = liftO2 (λ x y. simplify_reg (difference_reg x y)) (rr2_of_rr2_rel ℱ Rs r1) (rr2_of_rr2_rel ℱ Rs r2)"
| "rr2_of_rr2_rel ℱ Rs (R2Comp r1 r2) = liftO2 (λ x y. simplify_reg (rr2_compositon ℱ x y))
(rr2_of_rr2_rel ℱ Rs r1) (rr2_of_rr2_rel ℱ Rs r2)"
abbreviation lhss where
"lhss R ≡ fst |`| R"
lemma rr12_of_rr12_rel_correct:
fixes Rs :: "(('f :: linorder, 'v) Term.term × ('f, 'v) Term.term) fset list"
assumes "∀R ∈ set Rs. lv_trs (fset R) ∧ ffunas_trs R |⊆| ℱ"
shows "∀ta1. rr1_of_rr1_rel ℱ Rs r1 = Some ta1 ⟶ RR1_spec ta1 (eval_rr1_rel (fset ℱ) (map fset Rs) r1)"
"∀ta2. rr2_of_rr2_rel ℱ Rs r2 = Some ta2 ⟶ RR2_spec ta2 (eval_rr2_rel (fset ℱ) (map fset Rs) r2)"
proof (induct r1 and r2)
note [simp] = bind_eq_Some_conv guard_simps
let ?F = "fset ℱ" let ?Rs = "map fset Rs"
{
case R1Terms
then show ?case using term_automaton[of ℱ]
by (simp add: 𝒯⇩G_equivalent_def)
next
case (R1NF r)
consider (a) "∃ R. is_to_trs' Rs r = Some R" | (b) "is_to_trs' Rs r = None" by auto
then show ?case
proof (cases)
case a
from a obtain R where [simp]: "is_to_trs' Rs r = Some R" "is_to_fin_trs Rs r = R"
by (auto simp: is_to_trs'_def)
from is_to_trs'_props[OF assms this(1)] have inv: "ffunas_trs R |⊆| ℱ" "lv_trs (fset R)" .
from inv have fl: "∀ l |∈| lhss R. linear_term l"
by (auto simp: lv_trs_def split!: prod.splits)
{fix s t assume ass: "(s, t) ∈ grstep (fset R)"
then obtain C l r σ where step: "(l, r) |∈| R" "term_of_gterm s = (C :: ('f, 'v) ctxt) ⟨l ⋅ σ⟩" "term_of_gterm t = C⟨r ⋅ σ⟩"
unfolding grstep_def by (auto simp: dest!: rstep_imp_C_s_r)
from step ta_nf_lang_sound[of l "lhss R" C σ ℱ]
have "s ∉ ℒ (nf_reg (lhss R) ℱ)" unfolding ℒ_def
by (metis fimage_eqI fst_conv nf_reg_def reg.sel(1, 2) term_of_gterm_in_ta_lang_conv)}
note mem = this
have funas: "funas_trs (fset R) ⊆ ?F" using inv(1)
by (simp add: ffunas_trs.rep_eq less_eq_fset.rep_eq subsetD)
{fix s assume "s ∈ ℒ (nf_reg (lhss R) ℱ)"
then have "s ∈ NF (Restr (grstep (fset R)) (𝒯⇩G (fset ℱ))) ∩ 𝒯⇩G (fset ℱ)"
by (meson IntI NF_I 𝒯⇩G_funas_gterm_conv gta_lang_nf_ta_funas inf.cobounded1 mem subset_iff)}
moreover
{fix s assume ass: "s ∈ NF (Restr (grstep (fset R)) (𝒯⇩G (fset ℱ))) ∩ 𝒯⇩G (fset ℱ)"
then have *: "(term_of_gterm s, term_of_gterm t) ∉ rstep (fset R)" for t using funas
by (auto simp: funas_trs_def grstep_def NF_iff_no_step 𝒯⇩G_funas_gterm_conv)
(meson R1NF_reps funas rstep.cases)
then have "s ∈ ℒ (nf_reg (lhss R) ℱ)" using fl ass
using ta_nf_ℒ_complete[OF fl, of _ ℱ] gta_lang_nf_ta_funas[of _ "lhss R" ℱ]
by (smt (verit, ccfv_SIG) IntE R1NF_reps 𝒯⇩G_sound fimageE funas surjective_pairing)}
ultimately have "ℒ (nf_reg (lhss R) ℱ) = NF (Restr (grstep (fset R)) (𝒯⇩G (fset ℱ))) ∩ 𝒯⇩G (fset ℱ)"
by blast
then show ?thesis using fl(1)
by (simp add: RR1_spec_def is_to_trs_conv)
qed auto
next
case (R1Inf r)
consider (a) "∃ A. rr2_of_rr2_rel ℱ Rs r = Some A" | (b) " rr2_of_rr2_rel ℱ Rs r = None" by auto
then show ?case
proof cases
case a
have [simp]: "{u. (t, u) ∈ eval_rr2_rel ?F ?Rs r ∧ funas_gterm u ⊆ ?F} =
{u. (t, u) ∈ eval_rr2_rel ?F ?Rs r}" for t
using eval_rr12_rel_sig(2)[of ?F ?Rs r] by (auto simp: 𝒯⇩G_equivalent_def)
have [simp]: "infinite {u. (t, u) ∈ eval_rr2_rel ?F ?Rs r} ⟹ funas_gterm t ⊆ ?F" for t
using eval_rr12_rel_sig(2)[of ?F ?Rs r] not_finite_existsD by (fastforce simp: 𝒯⇩G_equivalent_def)
from a obtain A where [simp]: "rr2_of_rr2_rel ℱ Rs r = Some A" by blast
from R1Inf this have spec: "RR2_spec A (eval_rr2_rel ?F ?Rs r)" by auto
then have spec_trim: "RR2_spec (trim_reg A) (eval_rr2_rel ?F ?Rs r)" by auto
let ?B = "(Inf_reg (trim_reg A) (Q_infty (ta (trim_reg A)) ℱ))"
have B: "RR2_spec ?B {(s, t) | s t. gpair s t ∈ ℒ ?B}"
using subset_trans[OF Inf_automata_subseteq[of "trim_reg A" ℱ], of "ℒ A"] spec
by (auto simp: RR2_spec_def ℒ_trim)
have *: "ℒ (Inf_reg_impl (trim_reg A)) = ℒ ?B" using spec
using eval_rr12_rel_sig(2)[of ?F ?Rs r]
by (intro Inf_reg_impl_sound) (auto simp: ℒ_trim RR2_spec_def 𝒯⇩G_equivalent_def)
then have **: "RR2_spec (Inf_reg_impl (trim_reg A)) {(s, t) | s t. gpair s t ∈ ℒ ?B}" using B
by (auto simp: RR2_spec_def)
show ?thesis
using spec eval_rr12_rel_sig(2)[of ?F ?Rs r]
using ℒ_Inf_reg[OF spec_trim, of ℱ]
by (auto simp: 𝒯⇩G_equivalent_def * RR1_spec_def ℒ_trim ℒ_proj(1)[OF **]
Inf_branching_terms_def fImage_singleton)
(metis (no_types, lifting) SigmaD1 in_mono mem_Collect_eq not_finite_existsD)
qed auto
next
case (R1Proj i r)
then show ?case
proof (cases i)
case [simp]:0 show ?thesis using R1Proj
using proj_automaton_gta_lang(1)[of "the (rr2_of_rr2_rel ℱ Rs r)" "eval_rr2_rel ?F ?Rs r"]
by simp
next
case (Suc nat) then show ?thesis using R1Proj
using proj_automaton_gta_lang(2)[of "the (rr2_of_rr2_rel ℱ Rs r)" "eval_rr2_rel ?F ?Rs r"]
by simp
qed
next
case (R1Union s1 s2)
then show ?case
by (auto simp: RR1_spec_def ℒ_union)
next
case (R1Inter s1 s2)
from R1Inter show ?case
by (auto simp: ℒ_intersect RR1_spec_def)
next
case (R1Diff s1 s2)
then show ?case
by (auto intro: RR1_difference)
next
case (R2GTT_Rel g w x)
note ass = R2GTT_Rel
consider (a) "∃ A. gtt_of_gtt_rel ℱ Rs g = Some A" | (b) "gtt_of_gtt_rel ℱ Rs g = None" by blast
then show ?case
proof cases
case a then obtain A where [simp]: "gtt_of_gtt_rel ℱ Rs g = Some A" by blast
from gtt_of_gtt_rel_correct[OF assms this]
have spec [simp]: "eval_gtt_rel ?F ?Rs g = agtt_lang A" by auto
let ?B = "GTT_to_RR2_root_reg A" note [simp] = GTT_to_RR2_root[of A]
show ?thesis
proof (cases w)
case [simp]: PRoot show ?thesis
proof (cases x)
case EParallel
then show ?thesis using reflcl_automaton[of ?B "agtt_lang A" ℱ]
by auto
qed (auto simp: GTT_to_RR2_root)
next
case PNonRoot
then show ?thesis
using nhole_ctxt_closure_automaton[of ?B "agtt_lang A" ℱ]
using nhole_mctxt_reflcl_automaton[of ?B "agtt_lang A" ℱ]
using nhole_mctxt_closure_automaton[of ?B "agtt_lang A" ℱ]
by (cases x) auto
next
case PAny
then show ?thesis
using ctxt_closure_automaton[of ?B "agtt_lang A" ℱ]
using parallel_closure_automaton[of ?B "agtt_lang A" ℱ]
using mctxt_closure_automaton[of ?B "agtt_lang A" ℱ]
by (cases x) auto
qed
qed (cases w; cases x, auto)
next
case (R2Diag s)
then show ?case
by (auto simp: RR2_spec_def RR1_spec_def fmap_funs_ℒ Id_on_iff
fmap_funs_gta_lang map_funs_term_some_gpair)
next
case (R2Prod s1 s2)
then show ?case using pair_automaton[of "the (rr1_of_rr1_rel ℱ Rs s1)" _ "the (rr1_of_rr1_rel ℱ Rs s2)"]
by auto
next
case (R2Inv r)
show ?case using R2Inv by (auto simp: swap_RR2_spec)
next
case (R2Union r1 r2)
then show ?case using union_automaton
by (auto simp: RR2_spec_def ℒ_union)
next
case (R2Inter r1 r2)
then show ?case
by (auto simp: ℒ_intersect RR2_spec_def)
next
case (R2Diff r1 r2)
then show ?case by (auto intro: RR2_difference)
next
case (R2Comp r1 r2)
then show ?case using eval_rr12_rel_sig
by (auto intro!: rr2_compositon) blast+
}
qed
subsection ‹Misc›
lemma eval_formula_arity_cong:
assumes "⋀i. i < formula_arity f ⟹ α' i = α i"
shows "eval_formula ℱ Rs α' f = eval_formula ℱ Rs α f"
proof -
have [simp]: "j < length fs ⟹ i < formula_arity (fs ! j) ⟹ i < max_list (map formula_arity fs)" for i j fs
by (simp add: less_le_trans max_list)
show ?thesis using assms
proof (induct f arbitrary: α α')
case (FAnd fs)
show ?case using FAnd(1)[OF nth_mem, of _ α' α] FAnd(2) by (auto simp: all_set_conv_all_nth)
next
case (FOr fs)
show ?case using FOr(1)[OF nth_mem, of _ α' α] FOr(2) by (auto simp: ex_set_conv_ex_nth)
next
case (FNot f)
show ?case using FNot(1)[of α' α] FNot(2) by simp
next
case (FExists f)
show ?case using FExists(1)[of "α'⟨0 : z⟩" "α⟨0 : z⟩" for z] FExists(2) by (auto simp: shift_def)
next
case (FForall f)
show ?case using FForall(1)[of "α'⟨0 : z⟩" "α⟨0 : z⟩" for z] FForall(2) by (auto simp: shift_def)
qed simp_all
qed
subsection ‹Connect semantics to FOL-Fitting›
primrec form_of_formula :: "'trs formula ⇒ (unit, 'trs rr1_rel + 'trs rr2_rel) form" where
"form_of_formula (FRR1 r1 x) = Pred (Inl r1) [Var x]"
| "form_of_formula (FRR2 r2 x y) = Pred (Inr r2) [Var x, Var y]"
| "form_of_formula (FAnd fs) = foldr And (map form_of_formula fs) TT"
| "form_of_formula (FOr fs) = foldr Or (map form_of_formula fs) FF"
| "form_of_formula (FNot f) = Neg (form_of_formula f)"
| "form_of_formula (FExists f) = Exists (And (Pred (Inl R1Terms) [Var 0]) (form_of_formula f))"
| "form_of_formula (FForall f) = Forall (Impl (Pred (Inl R1Terms) [Var 0]) (form_of_formula f))"
fun for_eval_rel :: "('f × nat) set ⇒ ('f, 'v) trs list ⇒ ftrs rr1_rel + ftrs rr2_rel ⇒ 'f gterm list ⇒ bool" where
"for_eval_rel ℱ Rs (Inl r1) [t] ⟷ t ∈ eval_rr1_rel ℱ Rs r1"
| "for_eval_rel ℱ Rs (Inr r2) [t, u] ⟷ (t, u) ∈ eval_rr2_rel ℱ Rs r2"
lemma eval_formula_conv:
"eval_formula ℱ Rs α f = eval α undefined (for_eval_rel ℱ Rs) (form_of_formula f)"
proof (induct f arbitrary: α)
case (FAnd fs) then show ?case
unfolding eval_formula.simps by (induct fs) auto
next
case (FOr fs) then show ?case
unfolding eval_formula.simps by (induct fs) auto
qed auto
subsection ‹RRn relations and formulas›
lemma shift_rangeI [intro!]:
"range α ⊆ T ⟹ x ∈ T ⟹ range (shift α i x) ⊆ T"
by (auto simp: shift_def)
definition formula_relevant where
"formula_relevant ℱ Rs vs fm ⟷
(∀α α'. range α ⊆ 𝒯⇩G ℱ ⟶ range α' ⊆ 𝒯⇩G ℱ ⟶ map α vs = map α' vs ⟶ eval_formula ℱ Rs α fm ⟶ eval_formula ℱ Rs α' fm)"
lemma formula_relevant_mono:
"set vs ⊆ set ws ⟹ formula_relevant ℱ Rs vs fm ⟹ formula_relevant ℱ Rs ws fm"
unfolding formula_relevant_def
by (meson map_eq_conv subset_code(1))
lemma formula_relevantD:
"formula_relevant ℱ Rs vs fm ⟹
range α ⊆ 𝒯⇩G ℱ ⟹ range α' ⊆ 𝒯⇩G ℱ ⟹ map α vs = map α' vs ⟹
eval_formula ℱ Rs α fm ⟹ eval_formula ℱ Rs α' fm"
unfolding formula_relevant_def
by blast
lemma trivial_formula_relevant:
assumes "⋀α. range α ⊆ 𝒯⇩G ℱ ⟹ ¬ eval_formula ℱ Rs α fm"
shows "formula_relevant ℱ Rs vs fm"
using assms unfolding formula_relevant_def
by auto
lemma formula_relevant_0_FExists:
assumes "formula_relevant ℱ Rs [0] fm"
shows "formula_relevant ℱ Rs [] (FExists fm)"
unfolding formula_relevant_def
proof (intro allI, intro impI)
fix α α' assume ass: "range α ⊆ 𝒯⇩G ℱ" "range (α' :: fvar ⇒ 'a gterm) ⊆ 𝒯⇩G ℱ"
"eval_formula ℱ Rs α (FExists fm)"
from ass(3) obtain z where "z ∈ 𝒯⇩G ℱ" "eval_formula ℱ Rs (α⟨0 : z⟩) fm"
by auto
then show "eval_formula ℱ Rs α' (FExists fm)"
using ass(1, 2) formula_relevantD[OF assms, of "α⟨0:z⟩" "α'⟨0:z⟩"]
by (auto simp: shift_rangeI intro!: exI[of _ z])
qed
definition formula_spec where
"formula_spec ℱ Rs vs A fm ⟷ sorted vs ∧ distinct vs ∧
formula_relevant ℱ Rs vs fm ∧
RRn_spec (length vs) A {map α vs |α. range α ⊆ 𝒯⇩G ℱ ∧ eval_formula ℱ Rs α fm}"
lemma formula_spec_RRn_spec:
"formula_spec ℱ Rs vs A fm ⟹ RRn_spec (length vs) A {map α vs |α. range α ⊆ 𝒯⇩G ℱ ∧ eval_formula ℱ Rs α fm}"
by (simp add: formula_spec_def)
lemma formula_spec_nt_empty_form_sat:
"¬ reg_empty A ⟹ formula_spec ℱ Rs vs A fm ⟹ ∃ α. range α ⊆ 𝒯⇩G ℱ ∧ eval_formula ℱ Rs α fm"
unfolding formula_spec_def
by (auto simp: RRn_spec_def ℒ_def)
lemma formula_spec_empty:
"reg_empty A ⟹ formula_spec ℱ Rs vs A fm ⟹ range α ⊆ 𝒯⇩G ℱ ⟹ eval_formula ℱ Rs α fm ⟷ False"
unfolding formula_spec_def
by (auto simp: RRn_spec_def ℒ_def)
text ‹In each inference step, we obtain a triple consisting of a formula @{term "fm"}, a list of
relevant variables @{term "vs"} (typically a sublist of @{term "[0..<formula_arity fm]"}), and
an RRn automaton @{term "A"}, such that the property @{term "formula_spec ℱ Rs vs A fm"} holds.›
lemma false_formula_spec:
"sorted vs ⟹ distinct vs ⟹ formula_spec ℱ Rs vs empty_reg FFalse"
by (auto simp: formula_spec_def false_RRn_spec FFalse_def formula_relevant_def)
lemma true_formula_spec:
assumes "vs ≠ [] ∨ 𝒯⇩G (fset ℱ) ≠ {}" "sorted vs" "distinct vs"
shows "formula_spec (fset ℱ) Rs vs (true_RRn ℱ (length vs)) FTrue"
proof -
have "{ts. length ts = length vs ∧ set ts ⊆ 𝒯⇩G (fset ℱ)} = {map α vs |α. range α ⊆ 𝒯⇩G (fset ℱ)}"
proof (intro equalityI subsetI CollectI, goal_cases LR RL)
case (LR ts)
moreover obtain t0 where "funas_gterm t0 ⊆ fset ℱ" using LR assms(1) unfolding 𝒯⇩G_equivalent_def
by (cases vs) fastforce+
ultimately show ?case using `distinct vs`
apply (intro exI[of _ "λt. if t ∈ set vs then ts ! inv_into {0..<length vs} ((!) vs) t else t0"])
apply (auto intro!: nth_equalityI dest!: inj_on_nth[of vs "{0..<length vs}"] simp: in_set_conv_nth 𝒯⇩G_equivalent_def)
by (metis inv_to_set mem_Collect_eq subsetD)
qed fastforce
then show ?thesis using assms true_RRn_spec[of "length vs" ℱ]
by (auto simp: formula_spec_def FTrue_def formula_relevant_def 𝒯⇩G_equivalent_def)
qed
lemma relabel_formula_spec:
"formula_spec ℱ Rs vs A fm ⟹ formula_spec ℱ Rs vs (relabel_reg A) fm"
by (simp add: formula_spec_def)
lemma trim_formula_spec:
"formula_spec ℱ Rs vs A fm ⟹ formula_spec ℱ Rs vs (trim_reg A) fm"
by (simp add: formula_spec_def)
definition fit_permute :: "nat list ⇒ nat list ⇒ nat list ⇒ nat list" where
"fit_permute vs vs' vs'' = map (λv. if v ∈ set vs then the (mem_idx v vs) else length vs + the (mem_idx v vs'')) vs'"
definition fit_rrn :: "('f × nat) fset ⇒ nat list ⇒ nat list ⇒ (nat, 'f option list) reg ⇒ (_, 'f option list) reg" where
"fit_rrn ℱ vs vs' A = (let vs'' = subtract_list_sorted vs' vs in
fmap_funs_reg (λfs. map ((!) fs) (fit_permute vs vs' vs''))
(fmap_funs_reg (pad_with_Nones (length vs) (length vs'')) (pair_automaton_reg A (true_RRn ℱ (length vs'')))))"
lemma the_mem_idx_simp [simp]:
"distinct xs ⟹ i < length xs ⟹ the (mem_idx (xs ! i) xs) = i"
using mem_idx_sound[THEN iffD1, OF nth_mem, of i xs] mem_idx_sound_output[of "xs ! i" xs] distinct_conv_nth
by fastforce
lemma fit_rrn:
assumes spec: "formula_spec (fset ℱ) Rs vs A fm" and vs: "sorted vs'" "distinct vs'" "set vs ⊆ set vs'"
shows "formula_spec (fset ℱ) Rs vs' (fit_rrn ℱ vs vs' A) fm"
using spec unfolding formula_spec_def formula_relevant_def
apply (elim conjE)
proof (intro conjI vs(1,2) allI, goal_cases rel spec)
case (rel α α') show ?case using vs(3)
by (fastforce intro!: rel(3)[rule_format, of α α'])
next
case spec
define vs'' where "vs'' = subtract_list_sorted vs' vs"
have evalI: "range α ⊆ 𝒯⇩G (fset ℱ) ⟹ range α' ⊆ 𝒯⇩G (fset ℱ) ⟹ map α vs = map α' vs
⟹ eval_formula (fset ℱ) Rs α fm ⟹ eval_formula (fset ℱ) Rs α' fm" for α α'
using spec(3) by blast
have [simp]: "set vs' = set vs ∪ set vs''" "set vs'' ∩ set vs = {}" "set vs ∩ set vs'' = {}" and d: "distinct vs''"
using vs spec(1,2) by (auto simp: vs''_def)
then have [dest]: "v ∈ set vs'' ⟹ v ∈ set vs ⟹ False" for v by blast
note * = permute_automaton[OF append_automaton[OF spec(4) true_RRn_spec, of "length vs''"]]
have [simp]: "distinct vs ⟹ i ∈ set vs ⟹ vs ! the (mem_idx i vs) = (i :: nat)" for vs i
by (simp add: mem_idx_sound mem_idx_sound_output)
have [dest]: "distinct vs ⟹ i ∈ set vs ⟹ ¬ the (mem_idx i vs) < length vs ⟹ False" for i
by (meson mem_idx_sound2 mem_idx_sound_output option.exhaust_sel)
show ?case unfolding fit_rrn_def Let_def vs''_def[symmetric] 𝒯⇩G_equivalent_def
apply (rule subst[where P = "λl. RRn_spec l _ _", OF _ subst[where P = "λta. RRn_spec _ _ ta", OF _ *]])
subgoal by (simp add: fit_permute_def)
subgoal
apply (intro equalityI subsetI CollectI imageI; elim imageE CollectE exE conjE; unfold 𝒯⇩G_equivalent_def)
subgoal for x fs ts us α
using spec(1, 2) d
apply (intro exI[of _ "λv. if v ∈ set vs'' then us ! the (mem_idx v vs'') else α v"])
apply (auto simp: fit_permute_def nth_append 𝒯⇩G_equivalent_def
intro!: nth_equalityI evalI[of α "λv. if v ∈ set vs'' then us ! the (mem_idx v vs'') else α v"])
apply (metis distinct_Ex1 in_mono mem_Collect_eq nth_mem the_mem_idx_simp)
apply (metis distinct_Ex1 in_mono mem_Collect_eq nth_mem the_mem_idx_simp)
apply blast
by (meson ‹⋀va. ⟦va ∈ set vs''; va ∈ set vs⟧ ⟹ False› nth_mem)
subgoal premises p for xs α
apply (intro rev_image_eqI[of "map α (vs @ vs'')"])
subgoal using p by (force intro!: exI[of _ "map α vs", OF exI[of _ "map α vs''"]])
subgoal using p(1)
by (force intro!: nth_equalityI simp: fit_permute_def comp_def nth_append dest: iffD1[OF mem_idx_sound] mem_idx_sound_output)
done
done
subgoal using vs spec(1,2) unfolding fit_permute_def
apply (intro equalityI subsetI)
subgoal by (auto 0 3 dest: iffD1[OF mem_idx_sound] mem_idx_sound_output)
subgoal for x
apply (simp add: Compl_eq[symmetric] Diff_eq[symmetric] Un_Diff Diff_triv Int_absorb1)
apply (simp add: nth_image[symmetric, of "length xs" xs for xs, simplified] image_iff comp_def)
using image_cong[OF refl arg_cong[OF the_mem_idx_simp]] ‹distinct vs''›
by (smt (z3) add_diff_inverse_nat add_less_cancel_left atLeast0LessThan lessThan_iff the_mem_idx_simp)
done
done
qed
definition fit_rrns :: "('f × nat) fset ⇒ (ftrs formula × nat list × (nat, 'f option list) reg) list ⇒
nat list × ((nat, 'f option list) reg) list" where
"fit_rrns ℱ rrns = (let vs' = fold union_list_sorted (map (fst ∘ snd) rrns) [] in
(vs', map (λ(fm, vs, ta). relabel_reg (trim_reg (fit_rrn ℱ vs vs' ta))) rrns))"
lemma sorted_union_list_sortedI [simp]:
"sorted xs ⟹ sorted ys ⟹ sorted (union_list_sorted xs ys)"
by (induct xs ys rule: union_list_sorted.induct) auto
lemma distinct_union_list_sortedI [simp]:
"sorted xs ⟹ sorted ys ⟹ distinct xs ⟹ distinct ys ⟹ distinct (union_list_sorted xs ys)"
by (induct xs ys rule: union_list_sorted.induct) auto
lemma fit_rrns:
assumes infs: "⋀fvA. fvA ∈ set rrns ⟹ formula_spec (fset ℱ) Rs (fst (snd fvA)) (snd (snd fvA)) (fst fvA)"
assumes "(vs', tas') = fit_rrns ℱ rrns"
shows "length tas' = length rrns" "⋀i. i < length rrns ⟹ formula_spec (fset ℱ) Rs vs' (tas' ! i) (fst (rrns ! i))"
"distinct vs'" "sorted vs'"
proof (goal_cases)
have vs': "vs' = fold union_list_sorted (map (fst ∘ snd) rrns) []" using assms(2) by (simp add: fit_rrns_def Let_def)
have *: "sorted vs'" "distinct vs'" "⋀fvA. fvA ∈ set rrns ⟹ set (fst (snd fvA)) ⊆ set vs'"
using infs[unfolded formula_spec_def, THEN conjunct2, THEN conjunct1]
infs[unfolded formula_spec_def, THEN conjunct1]
unfolding vs' by (induct rrns rule: rev_induct) auto
{
case 1 then show ?case using assms(2) by (simp add: fit_rrns_def Let_def)
next
case (2 i)
have tas': "tas' ! i = relabel_reg (trim_reg (fit_rrn ℱ (fst (snd (rrns ! i))) vs' (snd (snd (rrns ! i)))))"
using 2 assms(2) by (simp add: fit_rrns_def Let_def split: prod.splits)
from *(1,2) *(3)[OF nth_mem] show ?case using 2 unfolding tas'
by (auto intro!: relabel_formula_spec trim_formula_spec fit_rrn 2 assms(1,2))
next
case 3 show ?case by (rule *)
next
case 4 show ?case by (rule *)
}
qed
subsection ‹Building blocks›
definition for_rrn where
"for_rrn tas = fold (λA B. relabel_reg (reg_union A B)) tas (Reg {||} (TA {||} {||}))"
lemma for_rrn:
assumes "length tas = length fs" "⋀i. i < length fs ⟹ formula_spec ℱ Rs vs (tas ! i) (fs ! i)"
and vs: "sorted vs" "distinct vs"
shows "formula_spec ℱ Rs vs (for_rrn tas) (FOr fs)"
using assms(1,2) unfolding for_rrn_def
proof (induct fs arbitrary: tas rule: rev_induct)
case Nil then show ?case using vs false_formula_spec[of vs ℱ Rs] by (auto simp: FFalse_def)
next
case (snoc fm fs)
have *: "Bex (set [x]) P = P x" for P x by auto
have [intro!]: "formula_spec ℱ Rs vs (reg_union A B) (FOr (fs @ [fm]))" if
"formula_spec ℱ Rs vs A fm" "formula_spec ℱ Rs vs B (FOr fs)" for A B using that
unfolding formula_spec_def
apply (intro conjI, blast, blast)
subgoal unfolding formula_relevant_def eval_formula.simps set_append bex_Un * by blast
apply (elim conjE)
subgoal premises p by (rule subst[of _ _ "RRn_spec _ _", OF _ union_automaton[OF p(6,8)]]) auto
done
show ?case using snoc(1)[of "take (length fs) tas"] snoc(2) snoc(3)[simplified, OF less_SucI] snoc(3)[of "length fs"] vs
by (cases tas rule: rev_exhaust) (auto simp: min_def nth_append intro!: relabel_formula_spec)
qed
fun fand_rrn where
"fand_rrn ℱ n [] = true_RRn ℱ n"
| "fand_rrn ℱ n (A # tas) = fold (λA B. simplify_reg (reg_intersect A B)) tas A"
lemma fand_rrn:
assumes "𝒯⇩G (fset ℱ) ≠ {}" "length tas = length fs" "⋀i. i < length fs ⟹ formula_spec (fset ℱ) Rs vs (tas ! i) (fs ! i)"
and vs: "sorted vs" "distinct vs"
shows "formula_spec (fset ℱ) Rs vs (fand_rrn ℱ (length vs) tas) (FAnd fs)"
proof (cases fs)
case Nil
have "tas = []" using assms(2) by (auto simp: Nil)
then show ?thesis using true_formula_spec[OF _ vs, of ℱ Rs] assms(1) Nil
by (simp add: FTrue_def)
next
case (Cons fm fs)
obtain ta tas' where tas: "tas = ta # tas'" using assms(2) Cons by (cases tas) auto
show ?thesis using assms(2) assms(3)[of "Suc _"] unfolding tas Cons
unfolding list.size add_Suc_right add_0_right nat.inject Suc_less_eq nth_Cons_Suc fand_rrn.simps
proof (induct fs arbitrary: tas' rule: rev_induct)
case Nil
have "formula_relevant (fset ℱ) Rs vs (FAnd [fm])" using assms(3)[of 0]
apply (simp add: tas Cons formula_spec_def)
unfolding formula_relevant_def eval_formula.simps in_set_simps by blast
then show ?case using assms(3)[of 0, unfolded tas Cons, simplified] Nil by (simp add: formula_spec_def)
next
case (snoc fm' fs)
have *: "Ball (insert x X) P ⟷ P x ∧ Ball X P" for P x X by auto
have [intro!]: "formula_spec (fset ℱ) Rs vs (reg_intersect A B) (FAnd (fm # fs @ [fm']))" if
"formula_spec (fset ℱ) Rs vs A fm'" "formula_spec (fset ℱ) Rs vs B (FAnd (fm # fs))" for A B using that
unfolding formula_spec_def
apply (intro conjI, blast, blast)
subgoal unfolding formula_relevant_def eval_formula.simps set_append set_simps ball_simps ball_Un in_set_simps *
by blast
apply (elim conjE)
subgoal premises p
by (rule subst[of _ _ "RRn_spec _ _", OF _ intersect_automaton[OF p(6,8)]])
(auto dest: p(5)[unfolded formula_relevant_def, rule_format])
done
show ?case using snoc(1)[of "take (length fs) tas'"] snoc(2) snoc(3)[simplified, OF less_SucI] snoc(3)[of "length fs"] vs
by (cases tas' rule: rev_exhaust) (auto simp: min_def nth_append simplify_reg_def intro!: relabel_formula_spec trim_formula_spec)
qed
qed
subsubsection ‹IExists inference rule›
lemma lift_fun_gpairD:
"map_gterm lift_fun s = gpair t u ⟹ t = s"
"map_gterm lift_fun s = gpair t u ⟹ u = s"
by (metis gfst_gpair gsnd_gpair map_funs_term_some_gpair)+
definition upd_bruijn :: "nat list ⇒ nat list" where
"upd_bruijn vs = tl (map (λ x. x - 1) vs)"
lemma upd_bruijn_length[simp]:
"length (upd_bruijn vs) = length vs - 1"
by (induct vs) (auto simp: upd_bruijn_def)
lemma pres_sorted_dec:
"sorted xs ⟹ sorted (map (λx. x - Suc 0) xs)"
by (induct xs) auto
lemma upd_bruijn_pres_sorted:
"sorted xs ⟹ sorted (upd_bruijn xs)"
unfolding upd_bruijn_def
by (intro sorted_tl) (auto simp: pres_sorted_dec)
lemma pres_distinct_not_0_list_dec:
"distinct xs ⟹ 0 ∉ set xs ⟹ distinct (map (λx. x - Suc 0) xs)"
by (induct xs) (auto, metis Suc_pred neq0_conv)
lemma upd_bruijn_pres_distinct:
assumes "sorted xs" "distinct xs"
shows "distinct (upd_bruijn xs)"
proof -
have "sorted (ys :: nat list) ⟹ distinct ys ⟹ 0 ∉ set (tl ys)" for ys
by (induct ys) auto
from this[OF assms] show ?thesis using assms(2)
using pres_distinct_not_0_list_dec[OF distinct_tl, OF assms(2)]
unfolding upd_bruijn_def
by (simp add: map_tl)
qed
lemma upd_bruijn_relevant_inv:
assumes "sorted vs" "distinct vs" "0 ∈ set vs"
and "⋀ x. x ∈ set (upd_bruijn vs) ⟹ α x = α' x"
shows "⋀ x. x ∈ set vs ⟹ (shift α 0 z) x = (shift α' 0 z) x"
using assms unfolding upd_bruijn_def
by (induct vs) (auto simp add: FOL_Fitting.shift_def)
lemma ExistsI_upd_brujin_0:
assumes "sorted vs" "distinct vs" "0 ∈ set vs" "formula_relevant ℱ Rs vs fm"
shows "formula_relevant ℱ Rs (upd_bruijn vs) (FExists fm)"
unfolding formula_relevant_def
proof (intro allI, intro impI)
fix α α' assume ass: "range α ⊆ 𝒯⇩G ℱ" "range (α' :: fvar ⇒ 'a gterm) ⊆ 𝒯⇩G ℱ"
"map α (upd_bruijn vs) = map α' (upd_bruijn vs)" "eval_formula ℱ Rs α (FExists fm)"
from ass(4) obtain z where "z ∈ 𝒯⇩G ℱ" "eval_formula ℱ Rs (α⟨0 : z⟩) fm"
by auto
then show "eval_formula ℱ Rs α' (FExists fm)"
using ass(1 - 3) formula_relevantD[OF assms(4), of "α⟨0:z⟩" "α'⟨0:z⟩"]
using upd_bruijn_relevant_inv[OF assms(1 - 3), of "α" "α'"]
by (auto simp: shift_rangeI intro!: exI[of _ z])
qed
declare subsetI[rule del]
lemma ExistsI_upd_brujin_no_0:
assumes "0 ∉ set vs" and "formula_relevant ℱ Rs vs fm"
shows "formula_relevant ℱ Rs (map (λx. x - Suc 0) vs) (FExists fm)"
unfolding formula_relevant_def
proof ((intro allI)+ , (intro impI)+, unfold eval_formula.simps)
fix α α' assume st: "range α ⊆ 𝒯⇩G ℱ" "range α' ⊆ 𝒯⇩G ℱ"
"map α (map (λx. x - Suc 0) vs) = map α' (map (λx. x - Suc 0) vs)"
"∃ z ∈ 𝒯⇩G ℱ. eval_formula ℱ Rs (shift α 0 z) fm"
then obtain z where w: "z ∈ 𝒯⇩G ℱ" "eval_formula ℱ Rs (shift α 0 z) fm" by auto
from this(1) have "eval_formula ℱ Rs (shift α' 0 z) fm"
using st(1 - 3) assms(1) FOL_Fitting.shift_def
apply (intro formula_relevantD[OF assms(2) _ _ _ w(2), of "shift α' 0 z"])
by auto (simp add: FOL_Fitting.shift_def)
then show "∃ z ∈ 𝒯⇩G ℱ. eval_formula ℱ Rs (shift α' 0 z) fm" using w(1)
by blast
qed
definition shift_right where
"shift_right α ≡ λ i. α (i + 1)"
lemma shift_right_nt_0:
"i ≠ 0 ⟹ α i = shift_right α (i - Suc 0)"
unfolding shift_right_def
by auto
lemma shift_shift_right_id [simp]:
"shift (shift_right α) 0 (α 0) = α"
by (auto simp: shift_def shift_right_def)
lemma shift_right_rangeI [intro]:
"range α ⊆ T ⟹ range (shift_right α) ⊆ T"
by (auto simp: shift_right_def intro: subsetI)
lemma eval_formula_shift_right_eval:
"eval_formula ℱ Rs α fm ⟹ eval_formula ℱ Rs (shift (shift_right α) 0 (α 0)) fm"
"eval_formula ℱ Rs (shift (shift_right α) 0 (α 0)) fm ⟹ eval_formula ℱ Rs α fm"
by (auto)
declare subsetI[intro!]
lemma nt_rel_0_trivial_shift:
assumes "0 ∉ set vs"
shows "{map α vs |α. range α ⊆ 𝒯⇩G ℱ ∧ eval_formula ℱ Rs α fm} =
{map (λx. α (x - Suc 0)) vs |α. range α ⊆ 𝒯⇩G ℱ ∧ (∃z ∈ 𝒯⇩G ℱ. eval_formula ℱ Rs (α⟨0:z⟩) fm)}"
(is "?Ls = ?Rs")
proof
{fix α assume ass: "range α ⊆ 𝒯⇩G ℱ" "eval_formula ℱ Rs α fm"
then have "map α vs = map (λx. (shift_right α) (x - Suc 0)) vs"
"range (shift_right α) ⊆ 𝒯⇩G ℱ" "α 0 ∈𝒯⇩G ℱ" "eval_formula ℱ Rs (shift (shift_right α) 0 (α 0)) fm"
using shift_right_rangeI[OF ass(1)] assms
by (auto intro: eval_formula_shift_right_eval(1), metis shift_right_nt_0)}
then show "?Ls ⊆ ?Rs"
by blast
next
show "?Rs ⊆ ?Ls"
by auto (metis FOL_Fitting.shift_def One_nat_def assms not_less0 shift_rangeI)
qed
lemma relevant_vars_upd_bruijn_tl:
assumes "sorted vs" "distinct vs"
shows "map (shift_right α) (upd_bruijn vs) = tl (map α vs)" using assms
proof (induct vs)
case (Cons a vs) then show ?case
using le_antisym
by (auto simp: upd_bruijn_def shift_right_def)
(metis One_nat_def Suc_eq_plus1 le_0_eq shift_right_def shift_right_nt_0)
qed (auto simp: upd_bruijn_def)
lemma drop_upd_bruijn_set:
assumes "sorted vs" "distinct vs"
shows "drop 1 ` {map α vs |α. range α ⊆ 𝒯⇩G ℱ ∧ eval_formula ℱ Rs α fm} =
{map α (upd_bruijn vs) |α. range α ⊆ 𝒯⇩G ℱ ∧ (∃z∈𝒯⇩G ℱ. eval_formula ℱ Rs (α⟨0:z⟩) fm)}"
(is "?Ls = ?Rs")
proof
{fix α assume ass: "range α ⊆ 𝒯⇩G ℱ" "eval_formula ℱ Rs α fm"
then have "drop 1 (map α vs) = map (shift_right α) (upd_bruijn vs)"
"range (shift_right α) ⊆ 𝒯⇩G ℱ" "α 0 ∈𝒯⇩G ℱ" "eval_formula ℱ Rs (shift (shift_right α) 0 (α 0)) fm"
using shift_right_rangeI[OF ass(1)]
by (auto simp: tl_drop_conv relevant_vars_upd_bruijn_tl[OF assms(1, 2)])}
then show "?Ls ⊆ ?Rs"
by blast
next
have [dest]: "0 ∈ set (tl vs) ⟹ False" using assms(1, 2)
by (cases vs) auto
{fix α z assume ass: "range α ⊆ 𝒯⇩G ℱ" "z ∈ 𝒯⇩G ℱ" "eval_formula ℱ Rs (α⟨0:z⟩) fm"
then have "map α (upd_bruijn vs) = tl (map (α⟨0:z⟩) vs)"
"range (α⟨0:z⟩) ⊆ 𝒯⇩G ℱ" "eval_formula ℱ Rs (α⟨0:z⟩) fm"
using shift_rangeI[OF ass(1)]
by (auto simp: upd_bruijn_def shift_def simp flip: map_tl)}
then show "?Rs ⊆ ?Ls"
by (auto simp: tl_drop_conv image_def) blast
qed
lemma closed_sat_form_env_dom:
assumes "formula_relevant ℱ Rs [] (FExists fm)" "range α ⊆ 𝒯⇩G ℱ" "eval_formula ℱ Rs α fm"
shows "{[α 0] |α. range α ⊆ 𝒯⇩G ℱ ∧ (∃ z ∈ 𝒯⇩G ℱ. eval_formula ℱ Rs (α⟨0:z⟩) fm)} = {[t] | t. t ∈ 𝒯⇩G ℱ}"
using formula_relevantD[OF assms(1)] assms(2-)
apply auto
apply blast
by (smt rangeI shift_eq shift_rangeI shift_right_rangeI shift_shift_right_id subsetD)
lemma find_append:
"find P (xs @ ys) = (if find P xs ≠ None then find P xs else find P ys)"
by (induct xs arbitrary: ys) (auto split!: if_splits)
subsection ‹Checking inferences›