Yiming Xu (Sep 17 2024 at 13:15): Yiming Xu (Sep 17 2024 at 13:15):Relevant definitions:
inductive KGproof :: "form set ⇒ form list ⇒ bool" where
"KGproof G []"
| "KGproof G p ∧ List.member p (IMP f1 f2) ∧ List.member p f1 ⟹ KGproof G (p @ [f2])"
| "KGproof G p ∧ List.member p f ⟹ KGproof G (p @ [subst σ f])"
| "KGproof G p ∧ List.member p f ⟹ KGproof G (p @ [BOX f])"
| "KGproof G p ⟹ KGproof G (p @ [IMP (DIAM form) (NOT (BOX (NOT form)))])"
| "KGproof G p ∧ ptaut f ⟹ KGproof G (p @ [f])"
| "KGproof G p ∧ f ∈ G ⟹ KGproof G (p @ [f])"
definition KG_provable_def :
"KG_provable Γ form ≡ ∃p. KGproof Γ p ∧ KGproof Γ (p @ [form])"
definition is_NML_def :
"is_NML s =
(∀ A B p q f form.
(ptaut form ⟶ form ∈ s) ∧
(IMP (BOX (IMP p q)) (IMP (BOX p) (BOX q))) ∈ s ∧
(IMP (DIAM p) (NOT (BOX (NOT p)))) ∈ s ∧
(IMP (NOT (BOX (NOT p))) (DIAM p)) ∈ s ∧
(A ∈ s ⟶ (subst f A) ∈ s) ∧
(A ∈ s ⟶ (BOX A) ∈ s) ∧
((IMP A B) ∈ s ∧ A ∈ s ⟶ B ∈ s))"
definition NMLG_def:
"NMLG Γ = ⋂ {A. ((is_NML A) ∧ (subset_eq Γ A))}"
Problem on proving:
lemma exercise_1_6_6_d2:
"f ∈ NMLG Γ ⟶ f ∈ { phi. KG_provable Γ phi }"
proof (rule NMLG_ind)
qed
After "rule NMLG_ind" , it gives me something of the pattern I like, looks like:
image.png
Yiming Xu (Sep 17 2024 at 13:18):From here, I want to:
1.expand the definition of KG_provable.
2.use the definition collection to eliminate the "{}".
Yiming Xu (Sep 17 2024 at 13:19):1 itself can be done by unfolding before the apply. But it will give me the following:
image.png
Yiming Xu (Sep 17 2024 at 13:19):There leaves a "{}" which I do not know how to get rid of simultaneously on all the subgoals.
Yiming Xu (Sep 17 2024 at 13:19):How can I achieve these two?
Last updated: Dec 30 2024 at 16:22 UTC