Email Gateway (Aug 23 2022 at 08:25): Email Gateway (Aug 23 2022 at 08:25):From: "Siu, Tony" <tony.siu.17@ucl.ac.uk>
Hi all,
I am trying to prove a property on two mutually defined inductive predicates. The following is a portion of the predicates:
inductive pos :: "Structure ⇒ Structure ⇒ bool"
and neg:: "Structure ⇒ Structure ⇒ bool"
where
"pos X X" |
"neg (Inl Z) (Inr X) ⟹ pos (Inl Z) (Inl (♯⇩A X))"|
"pos (Inl Z) (Inl X1) ⟹ pos (Inl Z) (Inl (X1 ;⇩A X2))"|
"pos (Inl Z) (Inl X2) ⟹ pos (Inl Z) (Inl (X1 ;⇩A X2))"|
"pos (Inl Z) (Inl X1) ⟹ pos (Inl Z) (Inl (X1 ,⇩A X2))"|
"pos (Inl Z) (Inl X2) ⟹ pos (Inl Z) (Inl (X1 ,⇩A X2))"|
The following is my lemma:
"pos (Inl Z) (Inl X) ⟹ ∃W. (X ⊢⇩C Y) ≡⇩D (Z ⊢⇩C W)" and " neg (Inl Z) (Inr Y) ⟹ ∃W. (X ⊢⇩C Y) ≡⇩D (Z ⊢⇩C W)"
When I try to apply pos_neg.induct, it failed to apply initial proof method.
However, if I change the lemma to the following:
"((pos (Inl Z) (Inl X) ⟶ (∃W. (X ⊢⇩C Y) ≡⇩D (Z ⊢⇩C W)))) ∧ ((neg (Inl Z) (Inr Y) ⟶ (∃W. (X ⊢⇩C Y) ≡⇩D (Z ⊢⇩C W))))"
I can apply pos_neg.induct, but it does not yield desired goals for the lemma.
My question is what is the difference between those two lemmas in terms of Isabelle mechanism? Secondly, why can't I apply rule induction on my first lemma?
Thanks in advance for any help.
Kind Regards,
Tony
Last updated: Apr 25 2024 at 20:15 UTC