Theory First_Order_Ordering
theory First_Order_Ordering
imports
First_Order_Clause
Ground_Ordering
Relation_Extra
begin
context ground_ordering
begin
lemmas less⇩l⇩G_transitive_on = literal_order.transp_on_less
lemmas less⇩l⇩G_asymmetric_on = literal_order.asymp_on_less
lemmas less⇩l⇩G_total_on = literal_order.totalp_on_less
lemmas less⇩c⇩G_transitive_on = clause_order.transp_on_less
lemmas less⇩c⇩G_asymmetric_on = clause_order.asymp_on_less
lemmas less⇩c⇩G_total_on = clause_order.totalp_on_less
lemmas is_maximal_lit_def = is_maximal_in_mset_wrt_iff[OF less⇩l⇩G_transitive_on less⇩l⇩G_asymmetric_on]
lemmas is_strictly_maximal_lit_def =
is_strictly_maximal_in_mset_wrt_iff[OF less⇩l⇩G_transitive_on less⇩l⇩G_asymmetric_on]
end
section ‹First order ordering›
locale first_order_ordering = term_ordering_lifting less⇩t
for
less⇩t :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≺⇩t" 50) +
assumes
less⇩t_total_on [intro]: "totalp_on {term. term.is_ground term} (≺⇩t)" and
less⇩t_wellfounded_on: "wfp_on {term. term.is_ground term} (≺⇩t)" and
less⇩t_ground_context_compatible:
"⋀context term⇩1 term⇩2.
term⇩1 ≺⇩t term⇩2 ⟹
term.is_ground term⇩1 ⟹
term.is_ground term⇩2 ⟹
context.is_ground context ⟹
context⟨term⇩1⟩ ≺⇩t context⟨term⇩2⟩" and
less⇩t_ground_subst_stability:
"⋀term⇩1 term⇩2 (γ :: 'v ⇒ ('f, 'v) term).
term.is_ground (term⇩1 ⋅t γ) ⟹
term.is_ground (term⇩2 ⋅t γ) ⟹
term⇩1 ≺⇩t term⇩2 ⟹
term⇩1 ⋅t γ ≺⇩t term⇩2 ⋅t γ" and
less⇩t_ground_subterm_property:
"⋀term⇩G context⇩G.
term.is_ground term⇩G ⟹
context.is_ground context⇩G ⟹
context⇩G ≠ □ ⟹
term⇩G ≺⇩t context⇩G⟨term⇩G⟩"
begin
lemmas less⇩t_transitive = transp_less_trm
lemmas less⇩t_asymmetric = asymp_less_trm
subsection ‹Definitions›
abbreviation less_eq⇩t (infix "≼⇩t" 50) where
"less_eq⇩t ≡ (≺⇩t)⇧=⇧="
definition less⇩t⇩G :: "'f ground_term ⇒ 'f ground_term ⇒ bool" (infix "≺⇩t⇩G" 50) where
"term⇩G⇩1 ≺⇩t⇩G term⇩G⇩2 ≡ term.from_ground term⇩G⇩1 ≺⇩t term.from_ground term⇩G⇩2"
notation less_lit (infix "≺⇩l" 50)
notation less_cls (infix "≺⇩c" 50)
lemma
assumes
L_in: "L ∈# C" and
subst_stability: "⋀L K. L ≺⇩l K ⟹ (L ⋅l σ) ≺⇩l (K ⋅l σ)" and
Lσ_max_in_Cσ: "literal_order.is_maximal_in_mset (C ⋅ σ) (L ⋅l σ)"
shows "literal_order.is_maximal_in_mset C L"
proof -
have Lσ_in: "L ⋅l σ ∈# C ⋅ σ" and Lσ_max: "∀y∈#C ⋅ σ. y ≠ L ⋅l σ ⟶ ¬ L ⋅l σ ≺⇩l y"
using Lσ_max_in_Cσ
unfolding atomize_conj literal_order.is_maximal_in_mset_iff
by argo
show "literal_order.is_maximal_in_mset C L"
unfolding literal_order.is_maximal_in_mset_iff
proof (intro conjI ballI impI)
show "L ∈# C"
using L_in .
next
show "⋀y. y ∈# C ⟹ y ≠ L ⟹ ¬ L ≺⇩l y"
using subst_stability
by (metis Lσ_max clause.subst_in_to_set_subst literal_order.order.strict_iff_order)
qed
qed
lemmas less⇩l_def = less_lit_def
lemmas less⇩c_def = less_cls_def
abbreviation less_eq⇩l (infix "≼⇩l" 50) where
"less_eq⇩l ≡ (≺⇩l)⇧=⇧="
abbreviation less_eq⇩c (infix "≼⇩c" 50) where
"less_eq⇩c ≡ (≺⇩c)⇧=⇧="
abbreviation is_maximal⇩l ::
"('f, 'v) atom literal ⇒ ('f, 'v) atom clause ⇒ bool" where
"is_maximal⇩l literal clause ≡ is_maximal_in_mset_wrt (≺⇩l) clause literal"
abbreviation is_strictly_maximal⇩l ::
"('f, 'v) atom literal ⇒ ('f, 'v) atom clause ⇒ bool" where
"is_strictly_maximal⇩l literal clause ≡ is_strictly_maximal_in_mset_wrt (≺⇩l) clause literal"
subsection ‹Term ordering›
lemmas less⇩t_asymmetric_on = term_order.asymp_on_less
lemmas less⇩t_irreflexive_on = term_order.irreflp_on_less
lemmas less⇩t_transitive_on = term_order.transp_on_less
lemma less⇩t_wellfounded_on': "Wellfounded.wfp_on (term.from_ground ` terms⇩G) (≺⇩t)"
proof (rule Wellfounded.wfp_on_subset)
show "Wellfounded.wfp_on {term. term.is_ground term} (≺⇩t)"
using less⇩t_wellfounded_on .
next
show "term.from_ground ` terms⇩G ⊆ {term. term.is_ground term}"
by force
qed
lemma less⇩t_total_on': "totalp_on (term.from_ground ` terms⇩G) (≺⇩t)"
using less⇩t_total_on
by (simp add: totalp_on_def)
lemma less⇩t⇩G_wellfounded: "wfp (≺⇩t⇩G)"
proof -
have "Wellfounded.wfp_on (range term.from_ground) (≺⇩t)"
using less⇩t_wellfounded_on' by metis
hence "wfp (λterm⇩G⇩1 term⇩G⇩2. term.from_ground term⇩G⇩1 ≺⇩t term.from_ground term⇩G⇩2)"
unfolding Wellfounded.wfp_on_image[symmetric] .
thus "wfp (≺⇩t⇩G)"
unfolding less⇩t⇩G_def .
qed
subsection ‹Ground term ordering›
lemma less⇩t⇩G_asymmetric [intro]: "asymp (≺⇩t⇩G)"
by (simp add: wfP_imp_asymp less⇩t⇩G_wellfounded)
lemmas less⇩t⇩G_asymmetric_on = less⇩t⇩G_asymmetric[THEN asymp_on_subset, OF subset_UNIV]
lemma less⇩t⇩G_transitive [intro]: "transp (≺⇩t⇩G)"
using less⇩t⇩G_def less⇩t_transitive transpE transpI
by (metis (full_types))
lemmas less⇩t⇩G_transitive_on = less⇩t⇩G_transitive[THEN transp_on_subset, OF subset_UNIV]
lemma less⇩t⇩G_total [intro]: "totalp (≺⇩t⇩G)"
unfolding less⇩t⇩G_def
using totalp_on_image[OF inj_term_of_gterm] less⇩t_total_on'
by blast
lemmas less⇩t⇩G_total_on = less⇩t⇩G_total[THEN totalp_on_subset, OF subset_UNIV]
lemma less⇩t⇩G_context_compatible [simp]:
assumes "term⇩1 ≺⇩t⇩G term⇩2"
shows "context⟨term⇩1⟩⇩G ≺⇩t⇩G context⟨term⇩2⟩⇩G"
using assms less⇩t_ground_context_compatible
unfolding less⇩t⇩G_def
by (metis context.ground_is_ground term.ground_is_ground ground_term_with_context(3))
lemma less⇩t⇩G_subterm_property [simp]:
assumes "context ≠ □⇩G"
shows "term ≺⇩t⇩G context⟨term⟩⇩G"
using
assms
less⇩t_ground_subterm_property[OF term.ground_is_ground context.ground_is_ground]
context_from_ground_hole
unfolding less⇩t⇩G_def ground_term_with_context(3)
by blast
lemma less⇩t_less⇩t⇩G [clause_simp]:
assumes "term.is_ground term⇩1" and "term.is_ground term⇩2"
shows "term⇩1 ≺⇩t term⇩2 ⟷ term.to_ground term⇩1 ≺⇩t⇩G term.to_ground term⇩2"
by (simp add: assms less⇩t⇩G_def)
lemma less_eq⇩t_ground_subst_stability:
assumes "term.is_ground (term⇩1 ⋅t γ)" "term.is_ground (term⇩2 ⋅t γ)" "term⇩1 ≼⇩t term⇩2"
shows "term⇩1 ⋅t γ ≼⇩t term⇩2 ⋅t γ"
using less⇩t_ground_subst_stability[OF assms(1, 2)] assms(3)
by auto
subsection ‹Literal ordering›
lemmas less⇩l_asymmetric [intro] = literal_order.asymp_on_less[of UNIV]
lemmas less⇩l_asymmetric_on [intro] = literal_order.asymp_on_less
lemmas less⇩l_transitive [intro] = literal_order.transp_on_less[of UNIV]
lemmas less⇩l_transitive_on = literal_order.transp_on_less
lemmas is_maximal⇩l_def = is_maximal_in_mset_wrt_iff[OF less⇩l_transitive_on less⇩l_asymmetric_on]
lemmas is_strictly_maximal⇩l_def =
is_strictly_maximal_in_mset_wrt_iff[OF less⇩l_transitive_on less⇩l_asymmetric_on]
lemmas is_maximal⇩l_if_is_strictly_maximal⇩l =
is_maximal_in_mset_wrt_if_is_strictly_maximal_in_mset_wrt[OF
less⇩l_transitive_on less⇩l_asymmetric_on
]
lemma less⇩l_ground_subst_stability:
assumes
"literal.is_ground (literal ⋅l γ)"
"literal.is_ground (literal' ⋅l γ)"
shows "literal ≺⇩l literal' ⟹ literal ⋅l γ ≺⇩l literal' ⋅l γ"
unfolding less⇩l_def mset_mset_lit_subst[symmetric]
proof (elim multp_map_strong[rotated -1])
show "monotone_on (set_mset (mset_lit literal + mset_lit literal')) (≺⇩t) (≺⇩t) (λterm. term ⋅t γ)"
by (rule monotone_onI)
(metis assms(1,2) less⇩t_ground_subst_stability ground_term_in_ground_literal_subst union_iff)
qed (use less⇩t_asymmetric less⇩t_transitive in simp_all)
lemma maximal⇩l_in_clause:
assumes "is_maximal⇩l literal clause"
shows "literal ∈# clause"
using assms
unfolding is_maximal⇩l_def
by(rule conjunct1)
lemma strictly_maximal⇩l_in_clause:
assumes "is_strictly_maximal⇩l literal clause"
shows "literal ∈# clause"
using assms
unfolding is_strictly_maximal⇩l_def
by(rule conjunct1)
subsection ‹Clause ordering›
lemmas less⇩c_asymmetric [intro] = clause_order.asymp_on_less[of UNIV]
lemmas less⇩c_asymmetric_on [intro] = clause_order.asymp_on_less
lemmas less⇩c_transitive [intro] = clause_order.transp_on_less[of UNIV]
lemmas less⇩c_transitive_on [intro] = clause_order.transp_on_less
lemma less⇩c_ground_subst_stability:
assumes
"clause.is_ground (clause ⋅ γ)"
"clause.is_ground (clause' ⋅ γ)"
shows "clause ≺⇩c clause' ⟹ clause ⋅ γ ≺⇩c clause' ⋅ γ"
unfolding clause.subst_def less⇩c_def
proof (elim multp_map_strong[rotated -1])
show "monotone_on (set_mset (clause + clause')) (≺⇩l) (≺⇩l) (λliteral. literal ⋅l γ)"
by (rule monotone_onI)
(metis assms(1,2) clause.to_set_is_ground_subst less⇩l_ground_subst_stability union_iff)
qed (use less⇩l_asymmetric less⇩l_transitive in simp_all)
subsection ‹Grounding›
sublocale ground: ground_ordering "(≺⇩t⇩G)"
apply unfold_locales
by(simp_all add: less⇩t⇩G_transitive less⇩t⇩G_asymmetric less⇩t⇩G_wellfounded less⇩t⇩G_total)
notation ground.less_lit (infix "≺⇩l⇩G" 50)
notation ground.less_cls (infix "≺⇩c⇩G" 50)
notation ground.lesseq_trm (infix "≼⇩t⇩G" 50)
notation ground.lesseq_lit (infix "≼⇩l⇩G" 50)
notation ground.lesseq_cls (infix "≼⇩c⇩G" 50)
lemma not_less_eq⇩t⇩G: "¬ term⇩G⇩2 ≼⇩t⇩G term⇩G⇩1 ⟷ term⇩G⇩1 ≺⇩t⇩G term⇩G⇩2"
using ground.term_order.not_le .
lemma less_eq⇩t_less_eq⇩t⇩G:
assumes "term.is_ground term⇩1" and "term.is_ground term⇩2"
shows "term⇩1 ≼⇩t term⇩2 ⟷ term.to_ground term⇩1 ≼⇩t⇩G term.to_ground term⇩2"
unfolding reflclp_iff less⇩t_less⇩t⇩G[OF assms]
using assms[THEN term.to_ground_inverse]
by auto
lemma less_eq⇩t⇩G_less_eq⇩t:
"term⇩G⇩1 ≼⇩t⇩G term⇩G⇩2 ⟷ term.from_ground term⇩G⇩1 ≼⇩t term.from_ground term⇩G⇩2"
unfolding
less_eq⇩t_less_eq⇩t⇩G[OF term.ground_is_ground term.ground_is_ground]
term.from_ground_inverse
..
lemma not_less_eq⇩t:
assumes "term.is_ground term⇩1" and "term.is_ground term⇩2"
shows "¬ term⇩2 ≼⇩t term⇩1 ⟷ term⇩1 ≺⇩t term⇩2"
unfolding less⇩t_less⇩t⇩G[OF assms] less_eq⇩t_less_eq⇩t⇩G[OF assms(2, 1)] not_less_eq⇩t⇩G
..
lemma less⇩l⇩G_less⇩l:
"literal⇩G⇩1 ≺⇩l⇩G literal⇩G⇩2 ⟷ literal.from_ground literal⇩G⇩1 ≺⇩l literal.from_ground literal⇩G⇩2"
unfolding less⇩l_def ground.less_lit_def less⇩t⇩G_def mset_literal_from_ground
using
multp_image_mset_image_msetI[OF _ less⇩t_transitive]
multp_image_mset_image_msetD[OF _ less⇩t_transitive_on term.inj_from_ground]
by blast
lemma less⇩l_less⇩l⇩G:
assumes "literal.is_ground literal⇩1" "literal.is_ground literal⇩2"
shows "literal⇩1 ≺⇩l literal⇩2 ⟷ literal.to_ground literal⇩1 ≺⇩l⇩G literal.to_ground literal⇩2"
using assms
by (simp add: less⇩l⇩G_less⇩l)
lemma less_eq⇩l_less_eq⇩l⇩G:
assumes "literal.is_ground literal⇩1" and "literal.is_ground literal⇩2"
shows "literal⇩1 ≼⇩l literal⇩2 ⟷ literal.to_ground literal⇩1 ≼⇩l⇩G literal.to_ground literal⇩2"
unfolding reflclp_iff less⇩l_less⇩l⇩G[OF assms]
using assms[THEN literal.to_ground_inverse]
by auto
lemma less_eq⇩l⇩G_less_eq⇩l:
"literal⇩G⇩1 ≼⇩l⇩G literal⇩G⇩2 ⟷ literal.from_ground literal⇩G⇩1 ≼⇩l literal.from_ground literal⇩G⇩2"
unfolding
less_eq⇩l_less_eq⇩l⇩G[OF literal.ground_is_ground literal.ground_is_ground]
literal.from_ground_inverse
..
lemma maximal_lit_in_clause:
assumes "ground.is_maximal_lit literal⇩G clause⇩G"
shows "literal⇩G ∈# clause⇩G"
using assms
unfolding ground.is_maximal_lit_def
by(rule conjunct1)
lemma is_maximal⇩l_empty [simp]:
assumes "is_maximal⇩l literal {#}"
shows False
using assms maximal⇩l_in_clause
by fastforce
lemma is_strictly_maximal⇩l_empty [simp]:
assumes "is_strictly_maximal⇩l literal {#}"
shows False
using assms strictly_maximal⇩l_in_clause
by fastforce
lemma is_maximal_lit_iff_is_maximal⇩l:
"ground.is_maximal_lit literal⇩G clause⇩G ⟷
is_maximal⇩l (literal.from_ground literal⇩G) (clause.from_ground clause⇩G)"
unfolding
is_maximal⇩l_def
ground.is_maximal_lit_def
clause.ground_sub_in_ground[symmetric]
using
less⇩l_less⇩l⇩G[OF literal.ground_is_ground clause.sub_in_ground_is_ground]
clause.sub_in_ground_is_ground
clause.ground_sub_in_ground
by (metis literal.to_ground_inverse literal.from_ground_inverse)
lemma is_strictly_maximal⇩G⇩l_iff_is_strictly_maximal⇩l:
"ground.is_strictly_maximal_lit literal⇩G clause⇩G
⟷ is_strictly_maximal⇩l (literal.from_ground literal⇩G) (clause.from_ground clause⇩G)"
unfolding
is_strictly_maximal_in_mset_wrt_iff_is_greatest_in_mset_wrt[OF
ground.less⇩l⇩G_transitive_on ground.less⇩l⇩G_asymmetric_on ground.less⇩l⇩G_total_on, symmetric
]
ground.is_strictly_maximal_lit_def
is_strictly_maximal⇩l_def
clause.ground_sub_in_ground[symmetric]
remove1_mset_literal_from_ground
clause.ground_sub
less_eq⇩l⇩G_less_eq⇩l
..
lemma not_less_eq⇩l⇩G: "¬ literal⇩G⇩2 ≼⇩l⇩G literal⇩G⇩1 ⟷ literal⇩G⇩1 ≺⇩l⇩G literal⇩G⇩2"
using asympD[OF ground.less⇩l⇩G_asymmetric_on] totalpD[OF ground.less⇩l⇩G_total_on]
by blast
lemma not_less_eq⇩l:
assumes "literal.is_ground literal⇩1" and "literal.is_ground literal⇩2"
shows "¬ literal⇩2 ≼⇩l literal⇩1 ⟷ literal⇩1 ≺⇩l literal⇩2"
unfolding less⇩l_less⇩l⇩G[OF assms] less_eq⇩l_less_eq⇩l⇩G[OF assms(2, 1)] not_less_eq⇩l⇩G
..
lemma less⇩c⇩G_less⇩c:
"clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2 ⟷ clause.from_ground clause⇩G⇩1 ≺⇩c clause.from_ground clause⇩G⇩2"
proof (rule iffI)
show "clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2 ⟹ clause.from_ground clause⇩G⇩1 ≺⇩c clause.from_ground clause⇩G⇩2"
unfolding less⇩c_def
by (auto simp: clause.from_ground_def ground.less_cls_def less⇩l⇩G_less⇩l
intro!: multp_image_mset_image_msetI elim: multp_mono_strong)
next
have "transp (λx y. literal.from_ground x ≺⇩l literal.from_ground y)"
by (metis (no_types, lifting) literal_order.less_trans transpI)
thus "clause.from_ground clause⇩G⇩1 ≺⇩c clause.from_ground clause⇩G⇩2 ⟹ clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2"
unfolding ground.less_cls_def clause.from_ground_def less⇩c_def
by (auto simp: less⇩l⇩G_less⇩l
dest!: multp_image_mset_image_msetD[OF _ less⇩l_transitive literal.inj_from_ground]
elim!: multp_mono_strong)
qed
lemma less⇩c_less⇩c⇩G:
assumes "clause.is_ground clause⇩1" "clause.is_ground clause⇩2"
shows "clause⇩1 ≺⇩c clause⇩2 ⟷ clause.to_ground clause⇩1 ≺⇩c⇩G clause.to_ground clause⇩2"
using assms
by (simp add: less⇩c⇩G_less⇩c)
lemma less_eq⇩c_less_eq⇩c⇩G:
assumes "clause.is_ground clause⇩1" and "clause.is_ground clause⇩2"
shows "clause⇩1 ≼⇩c clause⇩2 ⟷ clause.to_ground clause⇩1 ≼⇩c⇩G clause.to_ground clause⇩2"
unfolding reflclp_iff less⇩c_less⇩c⇩G[OF assms]
using assms[THEN clause.to_ground_inverse]
by fastforce
lemma less_eq⇩c⇩G_less_eq⇩c:
"clause⇩G⇩1 ≼⇩c⇩G clause⇩G⇩2 ⟷ clause.from_ground clause⇩G⇩1 ≼⇩c clause.from_ground clause⇩G⇩2"
unfolding
less_eq⇩c_less_eq⇩c⇩G[OF clause.ground_is_ground clause.ground_is_ground]
clause.from_ground_inverse
..
lemma not_less_eq⇩c⇩G: "¬ clause⇩G⇩2 ≼⇩c⇩G clause⇩G⇩1 ⟷ clause⇩G⇩1 ≺⇩c⇩G clause⇩G⇩2"
using asympD[OF ground.less⇩c⇩G_asymmetric_on] totalpD[OF ground.less⇩c⇩G_total_on]
by blast
lemma not_less_eq⇩c:
assumes "clause.is_ground clause⇩1" and "clause.is_ground clause⇩2"
shows "¬ clause⇩2 ≼⇩c clause⇩1 ⟷ clause⇩1 ≺⇩c clause⇩2"
unfolding less⇩c_less⇩c⇩G[OF assms] less_eq⇩c_less_eq⇩c⇩G[OF assms(2, 1)] not_less_eq⇩c⇩G
..
lemma less⇩t_ground_context_compatible':
assumes
"context.is_ground context"
"term.is_ground term"
"term.is_ground term'"
"context⟨term⟩ ≺⇩t context⟨term'⟩"
shows "term ≺⇩t term'"
using assms
by (metis less⇩t_ground_context_compatible not_less_eq⇩t term_order.dual_order.asym
term_order.order.not_eq_order_implies_strict)
lemma less⇩t_ground_context_compatible_iff:
assumes
"context.is_ground context"
"term.is_ground term"
"term.is_ground term'"
shows "context⟨term⟩ ≺⇩t context⟨term'⟩ ⟷ term ≺⇩t term'"
using assms less⇩t_ground_context_compatible less⇩t_ground_context_compatible'
by blast
subsection ‹Stability under ground substitution›
lemma less⇩t_less_eq⇩t_ground_subst_stability:
assumes
"term.is_ground (term⇩1 ⋅t γ)"
"term.is_ground (term⇩2 ⋅t γ)"
"term⇩1 ⋅t γ ≺⇩t term⇩2 ⋅t γ"
shows
"¬ term⇩2 ≼⇩t term⇩1"
proof
assume assumption: "term⇩2 ≼⇩t term⇩1"
have "term⇩2 ⋅t γ ≼⇩t term⇩1 ⋅t γ"
using less_eq⇩t_ground_subst_stability[OF
assms(2, 1)
assumption
].
then show False
using assms(3) by order
qed
lemma less_eq⇩l_ground_subst_stability:
assumes
"literal.is_ground (literal⇩1 ⋅l γ)"
"literal.is_ground (literal⇩2 ⋅l γ)"
"literal⇩1 ≼⇩l literal⇩2"
shows "literal⇩1 ⋅l γ ≼⇩l literal⇩2 ⋅l γ"
using less⇩l_ground_subst_stability[OF assms(1, 2)] assms(3)
by auto
lemma less⇩l_less_eq⇩l_ground_subst_stability: assumes
"literal.is_ground (literal⇩1 ⋅l γ)"
"literal.is_ground (literal⇩2 ⋅l γ)"
"literal⇩1 ⋅l γ ≺⇩l literal⇩2 ⋅l γ"
shows
"¬ literal⇩2 ≼⇩l literal⇩1"
by (meson assms less_eq⇩l_ground_subst_stability not_less_eq⇩l)
lemma less_eq⇩c_ground_subst_stability:
assumes
"clause.is_ground (clause⇩1 ⋅ γ)"
"clause.is_ground (clause⇩2 ⋅ γ)"
"clause⇩1 ≼⇩c clause⇩2"
shows "clause⇩1 ⋅ γ ≼⇩c clause⇩2 ⋅ γ"
using less⇩c_ground_subst_stability[OF assms(1, 2)] assms(3)
by auto
lemma less⇩c_less_eq⇩c_ground_subst_stability: assumes
"clause.is_ground (clause⇩1 ⋅ γ)"
"clause.is_ground (clause⇩2 ⋅ γ)"
"clause⇩1 ⋅ γ ≺⇩c clause⇩2 ⋅ γ"
shows
"¬ clause⇩2 ≼⇩c clause⇩1"
by (meson assms less_eq⇩c_ground_subst_stability not_less_eq⇩c)
lemma is_maximal⇩l_ground_subst_stability:
assumes
clause_not_empty: "clause ≠ {#}" and
clause_grounding: "clause.is_ground (clause ⋅ γ)"
obtains literal
where "is_maximal⇩l literal clause" "is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
proof-
assume assumption:
"⋀literal. is_maximal⇩l literal clause ⟹ is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ) ⟹ thesis"
from clause_not_empty
have clause_grounding_not_empty: "clause ⋅ γ ≠ {#}"
unfolding clause.subst_def
by simp
obtain literal where
literal: "literal ∈# clause" and
literal_grounding_is_maximal: "is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
using
ex_maximal_in_mset_wrt[OF less⇩l_transitive_on less⇩l_asymmetric_on clause_grounding_not_empty]
maximal⇩l_in_clause
unfolding clause.subst_def
by force
from literal_grounding_is_maximal
have no_bigger_than_literal:
"∀literal' ∈# clause ⋅ γ. literal' ≠ literal ⋅l γ ⟶ ¬ literal ⋅l γ ≺⇩l literal'"
unfolding is_maximal⇩l_def
by simp
show ?thesis
proof(cases "is_maximal⇩l literal clause")
case True
with literal_grounding_is_maximal assumption show ?thesis
by blast
next
case False
then obtain literal' where
literal': "literal' ∈# clause" "literal ≺⇩l literal'"
unfolding is_maximal⇩l_def
using literal
by blast
note literals_in_clause = literal(1) literal'(1)
note literals_grounding = literals_in_clause[THEN
clause.to_set_is_ground_subst[OF _ clause_grounding]
]
have "literal ⋅l γ ≺⇩l literal' ⋅l γ"
using less⇩l_ground_subst_stability[OF literals_grounding literal'(2)].
then have False
using
no_bigger_than_literal
clause.subst_in_to_set_subst[OF literal'(1)]
by (metis asymp_onD less⇩l_asymmetric_on)
then show ?thesis..
qed
qed
lemma is_maximal⇩l_ground_subst_stability':
assumes
"literal ∈# clause"
"clause.is_ground (clause ⋅ γ)"
"is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
shows
"is_maximal⇩l literal clause"
proof(rule ccontr)
assume "¬ is_maximal⇩l literal clause"
then obtain literal' where literal':
"literal ≺⇩l literal'"
"literal' ∈# clause "
using assms(1)
unfolding is_maximal⇩l_def
by blast
then have literal'_grounding: "literal.is_ground (literal' ⋅l γ)"
using assms(2) clause.to_set_is_ground_subst by blast
have literal_grounding: "literal.is_ground (literal ⋅l γ)"
using assms(1) assms(2) clause.to_set_is_ground_subst by blast
have literal_γ_in_premise: "literal' ⋅l γ ∈# clause ⋅ γ"
using clause.subst_in_to_set_subst[OF literal'(2)]
by simp
have "literal ⋅l γ ≺⇩l literal' ⋅l γ"
using less⇩l_ground_subst_stability[OF literal_grounding literal'_grounding literal'(1)].
then have "¬ is_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
using literal_γ_in_premise
unfolding is_maximal⇩l_def literal.subst_comp_subst
by (metis asympD less⇩l_asymmetric)
then show False
using assms(3)
by blast
qed
lemma less⇩l_total_on [intro]: "totalp_on (literal.from_ground ` literals⇩G) (≺⇩l)"
by (smt (verit, best) image_iff less⇩l⇩G_less⇩l totalpD ground.less⇩l⇩G_total_on totalp_on_def)
lemmas less⇩l_total_on_set_mset =
less⇩l_total_on[THEN totalp_on_subset, OF clause.to_set_from_ground[THEN equalityD1]]
lemma less⇩c_total_on: "totalp_on (clause.from_ground ` clauses) (≺⇩c)"
by (smt ground.clause_order.totalp_on_less image_iff less⇩c⇩G_less⇩c totalpD totalp_onI)
lemma unique_maximal_in_ground_clause:
assumes
"clause.is_ground clause"
"is_maximal⇩l literal clause"
"is_maximal⇩l literal' clause"
shows
"literal = literal'"
using assms(2, 3)
unfolding is_maximal⇩l_def
by (metis assms(1) less⇩l_total_on_set_mset clause.to_ground_inverse totalp_onD)
lemma unique_strictly_maximal_in_ground_clause:
assumes
"clause.is_ground clause"
"is_strictly_maximal⇩l literal clause"
"is_strictly_maximal⇩l literal' clause"
shows
"literal = literal'"
proof-
note are_maximal⇩l = assms(2, 3)[THEN is_maximal⇩l_if_is_strictly_maximal⇩l]
show ?thesis
using unique_maximal_in_ground_clause[OF assms(1) are_maximal⇩l].
qed
lemma is_strictly_maximal⇩l_ground_subst_stability:
assumes
clause_grounding: "clause.is_ground (clause ⋅ γ)" and
ground_strictly_maximal: "is_strictly_maximal⇩l literal⇩G (clause ⋅ γ)"
obtains literal where
"is_strictly_maximal⇩l literal clause" "literal ⋅l γ = literal⇩G"
proof-
assume assumption: "⋀literal.
is_strictly_maximal⇩l literal clause ⟹ literal ⋅l γ = literal⇩G ⟹ thesis"
have clause_grounding_not_empty: "clause ⋅ γ ≠ {#}"
using ground_strictly_maximal
unfolding is_strictly_maximal⇩l_def
by fastforce
have literal⇩G_in_clause_grounding: "literal⇩G ∈# clause ⋅ γ"
using ground_strictly_maximal is_strictly_maximal⇩l_def by blast
obtain literal where literal: "literal ∈# clause" "literal ⋅l γ = literal⇩G"
by (smt (verit, best) clause.subst_def imageE literal⇩G_in_clause_grounding multiset.set_map)
show ?thesis
proof(cases "is_strictly_maximal⇩l literal clause")
case True
then show ?thesis
using assumption
using literal(2) by blast
next
case False
then obtain literal' where literal':
"literal' ∈# clause - {# literal #}"
"literal ≼⇩l literal'"
unfolding is_strictly_maximal⇩l_def
using literal(1)
by blast
note literal_grounding =
clause.to_set_is_ground_subst[OF literal(1) clause_grounding]
have literal'_grounding: "literal.is_ground (literal' ⋅l γ)"
using literal'(1) clause_grounding
by (meson clause.to_set_is_ground_subst in_diffD)
have "literal ⋅l γ ≼⇩l literal' ⋅l γ"
using less_eq⇩l_ground_subst_stability[OF literal_grounding literal'_grounding literal'(2)].
then have False
using clause.subst_in_to_set_subst[OF literal'(1)] ground_strictly_maximal
unfolding
is_strictly_maximal⇩l_def
literal(2)[symmetric]
subst_clause_remove1_mset[OF literal(1)]
by blast
then show ?thesis..
qed
qed
lemma is_strictly_maximal⇩l_ground_subst_stability':
assumes
"literal ∈# clause"
"clause.is_ground (clause ⋅ γ)"
"is_strictly_maximal⇩l (literal ⋅l γ) (clause ⋅ γ)"
shows
"is_strictly_maximal⇩l literal clause"
using
is_maximal⇩l_ground_subst_stability'[OF
assms(1,2)
is_maximal⇩l_if_is_strictly_maximal⇩l[OF assms(3)]
]
assms(3)
unfolding
is_strictly_maximal⇩l_def is_maximal⇩l_def
subst_clause_remove1_mset[OF assms(1), symmetric]
by (metis in_diffD clause.subst_in_to_set_subst reflclp_iff)
lemma less⇩t_less⇩l:
assumes "term⇩1 ≺⇩t term⇩2"
shows
"term⇩1 ≈ term⇩3 ≺⇩l term⇩2 ≈ term⇩3"
"term⇩1 !≈ term⇩3 ≺⇩l term⇩2 !≈ term⇩3"
using assms
unfolding less⇩l_def multp_eq_multp⇩H⇩O[OF less⇩t_asymmetric less⇩t_transitive] multp⇩H⇩O_def
by (auto simp: add_mset_eq_add_mset)
lemma less⇩t_less⇩l':
assumes
"∀term ∈ set_uprod (atm_of literal). term ⋅t σ' ≼⇩t term ⋅t σ"
"∃term ∈ set_uprod (atm_of literal). term ⋅t σ' ≺⇩t term ⋅t σ"
shows "literal ⋅l σ' ≺⇩l literal ⋅l σ"
proof(cases literal)
case (Pos atom)
show ?thesis
proof(cases atom)
case (Upair term⇩1 term⇩2)
have "term⇩2 ⋅t σ' ≺⇩t term⇩2 ⋅t σ ⟹
multp (≺⇩t) {#term⇩1 ⋅t σ, term⇩2 ⋅t σ'#} {#term⇩1 ⋅t σ, term⇩2 ⋅t σ#}"
using multp_add_mset'[of "(≺⇩t)" "term⇩2 ⋅t σ'" "term⇩2 ⋅t σ" "{#term⇩1 ⋅t σ#}"] add_mset_commute
by metis
then show ?thesis
using assms
unfolding less⇩l_def Pos subst_literal(1) Upair subst_atom
by (auto simp: multp_add_mset multp_add_mset')
qed
next
case (Neg atom)
show ?thesis
proof(cases atom)
case (Upair term⇩1 term⇩2)
have "term⇩2 ⋅t σ' ≺⇩t term⇩2 ⋅t σ ⟹
multp (≺⇩t)
{#term⇩1 ⋅t σ, term⇩1 ⋅t σ, term⇩2 ⋅t σ', term⇩2 ⋅t σ'#}
{#term⇩1 ⋅t σ, term⇩1 ⋅t σ, term⇩2 ⋅t σ, term⇩2 ⋅t σ#}"
using multp_add_mset' multp_add_same[OF less⇩t_asymmetric less⇩t_transitive]
by simp
then show ?thesis
using assms
unfolding less⇩l_def Neg subst_literal(2) Upair subst_atom
by (auto simp: multp_add_mset multp_add_mset' add_mset_commute)
qed
qed
lemmas less⇩c_add_mset = multp_add_mset_reflclp[OF less⇩l_asymmetric less⇩l_transitive, folded less⇩c_def]
lemmas less⇩c_add_same = multp_add_same[OF less⇩l_asymmetric less⇩l_transitive, folded less⇩c_def]
lemma less_eq⇩l_less_eq⇩c:
assumes "∀literal ∈# clause. literal ⋅l σ' ≼⇩l literal ⋅l σ"
shows "clause ⋅ σ' ≼⇩c clause ⋅ σ"
using assms
by(induction clause)(clause_auto simp: less⇩c_add_same less⇩c_add_mset)
lemma less⇩l_less⇩c:
assumes
"∀literal ∈# clause. literal ⋅l σ' ≼⇩l literal ⋅l σ"
"∃literal ∈# clause. literal ⋅l σ' ≺⇩l literal ⋅l σ"
shows "clause ⋅ σ' ≺⇩c clause ⋅ σ"
using assms
proof(induction clause)
case empty
then show ?case by auto
next
case (add literal clause)
then have less_eq: "∀literal ∈# clause. literal ⋅l σ' ≼⇩l literal ⋅l σ"
by (metis add_mset_remove_trivial in_diffD)
show ?case
proof(cases "literal ⋅l σ' ≺⇩l literal ⋅l σ")
case True
moreover have "clause ⋅ σ' ≼⇩c clause ⋅ σ"
using less_eq⇩l_less_eq⇩c[OF less_eq].
ultimately show ?thesis
using less⇩c_add_mset
unfolding subst_clause_add_mset less⇩c_def
by blast
next
case False
then have less: "∃literal ∈# clause. literal ⋅l σ' ≺⇩l literal ⋅l σ"
using add.prems(2) by auto
from False have eq: "literal ⋅l σ' = literal ⋅l σ"
using add.prems(1) by force
show ?thesis
using add(1)[OF less_eq less] less⇩c_add_same
unfolding subst_clause_add_mset eq less⇩c_def
by blast
qed
qed
subsection ‹Substitution update›
lemma less⇩t_subst_upd:
fixes γ :: "('f, 'v) subst"
assumes
update_is_ground: "term.is_ground update" and
update_less: "update ≺⇩t γ var" and
term_grounding: "term.is_ground (term ⋅t γ)" and
var: "var ∈ term.vars term"
shows "term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
using assms(3, 4)
proof(induction "term")
case Var
then show ?case
using update_is_ground update_less
by simp
next
case (Fun f terms)
then have "∀term ∈ set terms. term ⋅t γ(var := update) ≼⇩t term ⋅t γ"
by (metis eval_with_fresh_var is_ground_iff reflclp_iff term.set_intros(4))
moreover then have "∃term ∈ set terms. term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
using Fun assms(2)
by (metis (full_types) fun_upd_same term.distinct(1) term.sel(4) term.set_cases(2)
term_order.dual_order.strict_iff_order term_subst_eq_rev)
ultimately show ?case
using Fun(2, 3)
proof(induction "filter (λterm. term ⋅t γ(var := update) ≺⇩t term ⋅t γ) terms"
arbitrary: terms)
case Nil
then show ?case
unfolding empty_filter_conv
by blast
next
case first: (Cons t ts)
have update_grounding [simp]: "term.is_ground (t ⋅t γ(var := update))"
using first.prems(3) update_is_ground first.hyps(2)
by (metis (no_types, lifting) filter_eq_ConsD fun_upd_other fun_upd_same in_set_conv_decomp
is_ground_iff term.set_intros(4))
then have t_grounding [simp]: "term.is_ground (t ⋅t γ)"
using update_grounding Fun.prems(1,2)
by (metis fun_upd_other is_ground_iff)
show ?case
proof(cases ts)
case Nil
then obtain ss1 ss2 where terms: "terms = ss1 @ t # ss2"
using filter_eq_ConsD[OF first.hyps(2)[symmetric]]
by blast
have ss1: "∀term ∈ set ss1. term ⋅t γ(var := update) = term ⋅t γ"
using first.hyps(2) first.prems(1)
unfolding Nil terms
by (smt (verit, del_insts) Un_iff append_Cons_eq_iff filter_empty_conv filter_eq_ConsD
set_append term_order.antisym_conv2)
have ss2: "∀term ∈ set ss2. term ⋅t γ(var := update) = term ⋅t γ"
using first.hyps(2) first.prems(1)
unfolding Nil terms
by (smt (verit, ccfv_SIG) Un_iff append_Cons_eq_iff filter_empty_conv filter_eq_ConsD
list.set_intros(2) set_append term_order.antisym_conv2)
let ?context = "More f (map (λterm. (term ⋅t γ)) ss1) □ (map (λterm. (term ⋅t γ)) ss2)"
have 1: "term.is_ground (t ⋅t γ)"
using terms first(5)
by auto
moreover then have "term.is_ground (t ⋅t γ(var := update))"
by (metis assms(1) fun_upd_other fun_upd_same is_ground_iff)
moreover have "context.is_ground ?context"
using terms first(5)
by auto
moreover have "t ⋅t γ(var := update) ≺⇩t t ⋅t γ"
using first.hyps(2)
by (meson Cons_eq_filterD)
ultimately have "?context⟨t ⋅t γ(var := update)⟩ ≺⇩t ?context⟨t ⋅t γ⟩"
using less⇩t_ground_context_compatible
by blast
moreover have "Fun f terms ⋅t γ(var := update) = ?context⟨t ⋅t γ(var := update)⟩"
unfolding terms
using ss1 ss2
by simp
moreover have "Fun f terms ⋅t γ = ?context⟨t ⋅t γ⟩"
unfolding terms
by auto
ultimately show ?thesis
by argo
next
case (Cons t' ts')
from first(2)
obtain ss1 ss2 where
terms: "terms = ss1 @ t # ss2" and
ss1: "∀s∈set ss1. ¬ s ⋅t γ(var := update) ≺⇩t s ⋅t γ" and
less: "t ⋅t γ(var := update) ≺⇩t t ⋅t γ" and
ts: "ts = filter (λterm. term ⋅t γ(var := update)≺⇩t term ⋅t γ) ss2"
using Cons_eq_filter_iff[of t ts "(λterm. term ⋅t γ(var := update) ≺⇩t term ⋅t γ)"]
by blast
let ?terms' = "ss1 @ (t ⋅t γ(var := update)) # ss2"
have [simp]: "t ⋅t γ(var := update) ⋅t γ = t ⋅t γ(var := update)"
using first.prems(3) update_is_ground
unfolding terms
by (simp add: is_ground_iff)
have [simp]: "t ⋅t γ(var := update) ⋅t γ(var := update) = t ⋅t γ(var := update)"
using first.prems(3) update_is_ground
unfolding terms
by (simp add: is_ground_iff)
have "ts = filter (λterm. term ⋅t γ(var := update) ≺⇩t term ⋅t γ) ?terms'"
using ss1 ts
by auto
moreover have "∀term ∈ set ?terms'. term ⋅t γ(var := update) ≼⇩t term ⋅t γ"
using first.prems(1)
unfolding terms
by simp
moreover have "∃term ∈ set ?terms'. term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
using calculation(1) Cons neq_Nil_conv by force
moreover have terms'_grounding: "term.is_ground (Fun f ?terms' ⋅t γ)"
using first.prems(3)
unfolding terms
by simp
moreover have "var ∈ term.vars (Fun f ?terms')"
by (metis calculation(3) eval_with_fresh_var term.set_intros(4) term_order.less_irrefl)
ultimately have less_terms': "Fun f ?terms' ⋅t γ(var := update) ≺⇩t Fun f ?terms' ⋅t γ"
using first.hyps(1) first.prems(3) by blast
have context_grounding: "context.is_ground (More f ss1 □ ss2 ⋅t⇩c γ)"
using terms'_grounding
by auto
have "Fun f (ss1 @ t ⋅t γ(var := update) # ss2) ⋅t γ ≺⇩t Fun f terms ⋅t γ"
unfolding terms
using less⇩t_ground_context_compatible[OF less _ _ context_grounding]
by simp
with less_terms' show ?thesis
unfolding terms
by auto
qed
qed
qed
lemma less⇩l_subst_upd:
fixes γ :: "('f, 'v) subst"
assumes
update_is_ground: "term.is_ground update" and
update_less: "update ≺⇩t γ var" and
literal_grounding: "literal.is_ground (literal ⋅l γ)" and
var: "var ∈ literal.vars literal"
shows "literal ⋅l γ(var := update) ≺⇩l literal ⋅l γ"
proof-
note less⇩t_subst_upd = less⇩t_subst_upd[of _ γ, OF update_is_ground update_less]
have all_ground_terms: "∀term ∈ set_uprod (atm_of literal). term.is_ground (term ⋅t γ)"
using assms(3)
apply(cases literal)
by (simp add: ground_term_in_ground_literal_subst)+
then have
"∀term ∈ set_uprod (atm_of literal).
var ∈ term.vars term ⟶ term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
using less⇩t_subst_upd
by blast
moreover have
"∀term ∈ set_uprod (atm_of literal).
var ∉ term.vars term ⟶ term ⋅t γ(var := update) = term ⋅t γ"
by (meson eval_with_fresh_var)
ultimately have "∀term ∈ set_uprod (atm_of literal). term ⋅t γ(var := update) ≼⇩t term ⋅t γ"
by blast
moreover have "∃term ∈ set_uprod (atm_of literal). term ⋅t γ(var := update) ≺⇩t term ⋅t γ"
using update_less var less⇩t_subst_upd all_ground_terms
unfolding literal.vars_def atom.vars_def set_literal_atm_of
by blast
ultimately show ?thesis
using less⇩t_less⇩l'
by blast
qed
lemma less⇩c_subst_upd:
assumes
update_is_ground: "term.is_ground update" and
update_less: "update ≺⇩t γ var" and
literal_grounding: "clause.is_ground (clause ⋅ γ)" and
var: "var ∈ clause.vars clause"
shows "clause ⋅ γ(var := update) ≺⇩c clause ⋅ γ"
proof-
note less⇩l_subst_upd = less⇩l_subst_upd[of _ γ, OF update_is_ground update_less]
have all_ground_literals: "∀literal ∈# clause. literal.is_ground (literal ⋅l γ)"
using clause.to_set_is_ground_subst[OF _ literal_grounding] by blast
then have
"∀literal ∈# clause.
var ∈ literal.vars literal ⟶ literal ⋅l γ(var := update) ≺⇩l literal ⋅l γ"
using less⇩l_subst_upd
by blast
then have "∀literal ∈# clause. literal ⋅l γ(var := update) ≼⇩l literal ⋅l γ"
by fastforce
moreover have "∃literal ∈# clause. literal ⋅l γ(var := update) ≺⇩l literal ⋅l γ"
using update_less var less⇩l_subst_upd all_ground_literals
unfolding clause.vars_def
by blast
ultimately show ?thesis
using less⇩l_less⇩c
by blast
qed
end
end