Yiming Xu (Nov 03 2024 at 09:07): Yiming Xu (Nov 03 2024 at 09:07):I am proving the following. I defined:
definition nbisim ::
"(nat ⇒ 'a ⇒ 'b ⇒ bool) ⇒ nat ⇒
('m,'p,'a) model ⇒ ('m,'p,'b) model ⇒
'a ⇒ 'b ⇒ bool" where
"nbisim Z n M M' w w' ≡
(∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ∧
(∀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v') ∧
(∀v v' p. Z 0 v v' ⟶ valt M p v = valt M' p v') ∧
(∀i v v' ul m.
i + 1 ≤ n ∧ Z (i + 1) v v' ∧ rel M m (v # ul) ⟶
(∃ul'.
rel M' m (v' # ul') ∧
(∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) ∧
(∀i v v' ul' m.
i + 1 ≤ n ∧ Z (i + 1) v v' ∧ rel M' m (v' # ul') ⟶
(∃ul.
rel M' m (v' # ul') ∧
(∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) ∧
Z n w w'
"
and want to prove:
lemma nbisim_on_worlds:
assumes "nbisim Z n M M' w w'" and "Z m v v'"
shows "v ∈ world M"
using assms nbisim_def sledgehammer
sledgehammer found the proof very quicky, it says:
Sledgehammering...
verit found a proof...
cvc4 found a proof...
cvc4 found a proof...
vampire found a proof...
spass found a proof...
cvc4: Try this: by (smt (verit)) (> 1.0 s, timed out)
verit: Duplicate proof
cvc4: Duplicate proof
vampire: Try this: by metis (> 1.0 s, timed out)
spass: Duplicate proof
Done
This is a particularly easy proof-even without looking at what are the relevant definitions are, it should be killed by metis, I expected. But both of the proofs gives by sledgehammer does not work. May I please ask what should I try?
Yiming Xu (Nov 03 2024 at 09:16):As the first obvious thing to try, I tried to restrict the searching space to a part of the definition nbisim_def. I went:
lemma equivD1 : "A ≡ B ⟹ A ⟹ B" by simp
thm nbisim_def[THEN equivD1, THEN conjunct1]
This gives me
nbisim (?Z2::nat ⇒ ?'a2 ⇒ ?'b2 ⇒ bool) (?n2::nat) (?M2::?'a2 set × (?'m2 ⇒ ?'a2 list ⇒ bool) × (?'p2 ⇒ ?'a2 ⇒ bool))
(?M'2::?'b2 set × (?'m2 ⇒ ?'b2 list ⇒ bool) × (?'p2 ⇒ ?'b2 ⇒ bool)) (?w2::?'a2) (?w'2::?'b2) ⟹
∀(i::nat) (v::?'a2) v'::?'b2. ?Z2 i v v' ⟶ i ≤ ?n2 ∧ v ∈ world ?M2 ∧ v' ∈ world ?M'2
I think I can just apply function to extract relevant part of this definition to obtain the theorem I want. But it does not accept another step of "THEN conjunct2". I think it is because "THEN conjunct2" does not go underneath the non-meta quantification and implication.
Yiming Xu (Nov 03 2024 at 09:26):From:
nbisim (?Z2::nat ⇒ ?'a2 ⇒ ?'b2 ⇒ bool) (?n2::nat) (?M2::?'a2 set × (?'m2 ⇒ ?'a2 list ⇒ bool) × (?'p2 ⇒ ?'a2 ⇒ bool))
(?M'2::?'b2 set × (?'m2 ⇒ ?'b2 list ⇒ bool) × (?'p2 ⇒ ?'b2 ⇒ bool)) (?w2::?'a2) (?w'2::?'b2) ⟹
∀(i::nat) (v::?'a2) v'::?'b2. ?Z2 i v v' ⟶ i ≤ ?n2 ∧ v ∈ world ?M2 ∧ v' ∈ world ?M'2
I tried
lemma PULL_metaall : "(A ⟹ (∀x. B)) ⟹ (⋀ x. A ⟹ B)" by simp
But for the next step, the theorem cannot be unified with PULL_metaall:
thm nbisim_def[THEN equivD1, THEN conjunct1, THEN PULL_metaall]
does not work.
The error message is:
exception THM 1 raised (line 2601 of "thm.ML"):
RSN: no unifiers
nbisim (?Z2::nat ⇒ ?'a2 ⇒ ?'b2 ⇒ bool) (?n2::nat) (?M2::?'a2 set × (?'m2 ⇒ ?'a2 list ⇒ bool) × (?'p2 ⇒ ?'a2 ⇒ bool))
(?M'2::?'b2 set × (?'m2 ⇒ ?'b2 list ⇒ bool) × (?'p2 ⇒ ?'b2 ⇒ bool)) (?w2::?'a2) (?w'2::?'b2) ⟹
∀(i::nat) (v::?'a2) v'::?'b2. ?Z2 i v v' ⟶ i ≤ ?n2 ∧ v ∈ world ?M2 ∧ v' ∈ world ?M'2
(?A::bool ⟹ ∀x::?'a. (?B::bool)) ⟹ ?A ⟹ ?B
Maybe a screenshot with color makes more sense.
image.png
Yiming Xu (Nov 03 2024 at 09:26):May I please ask why the unification fail? (I guess because of multiple quantifiers?)
Can we do something to force the unifcation?
Yong Kiam (Nov 03 2024 at 10:25):I don't think your PULL_metaall is doing what you want
Yong Kiam (Nov 03 2024 at 10:26):look carefully at the types: ?B is a constant while you want it to be a predicate in order to unify
Yiming Xu (Nov 03 2024 at 10:33):Thanks for the swift reply and sorry I am afraid that I do not get it. The "?B" is of type "bool", in which sense is it a constant, and in which sense is a predicate required?
It seems unexpected to me because I see "?B" is asking for a bool, and the thing below the first quantifier, i.e.
term "∀(v::'a2) v'::'b2. Z2 i v v' ⟶ i ≤ n2 ∧ v ∈ world M2 ∧ v' ∈ world M'2"
is indeed of type bool.
Yong Kiam (Nov 03 2024 at 11:03):it is of type bool, but the term has a free variable i
Yong Kiam (Nov 03 2024 at 11:05):∀x. B <-- here B is of type bool which means it is a predicate independent of x
Yiming Xu (Nov 03 2024 at 11:07):Thank you! I see. now it works and gives me:
(?A::bool ⟹
nbisim (?Z3::nat ⇒ ?'a3 ⇒ ?'b3 ⇒ bool) (?n3::nat) (?M3::?'a3 set × (?'m3 ⇒ ?'a3 list ⇒ bool) × (?'p3 ⇒ ?'a3 ⇒ bool))
(?M'3::?'b3 set × (?'m3 ⇒ ?'b3 list ⇒ bool) × (?'p3 ⇒ ?'b3 ⇒ bool)) (?w3::?'a3) (?w'3::?'b3)) ⟹
?A ⟹ ∀(v::?'a3) v'::?'b3. ?Z3 (?x::nat) v v' ⟶ ?x ≤ ?n3 ∧ v ∈ world ?M3 ∧ v' ∈ world ?M'3
That is what I expected.
Yiming Xu (Nov 03 2024 at 11:10):It seems not such a common approach though. May I please ask if there is a quicker way to, from:
nbisim Z n M M' w w' ≡
(∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ∧
(∀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v') ∧
(∀v v' p. Z 0 v v' ⟶ valt M p v = valt M' p v') ∧
(∀i v v' ul m.
i + 1 ≤ n ∧ Z (i + 1) v v' ∧ rel M m (v # ul) ⟶
(∃ul'.
rel M' m (v' # ul') ∧
(∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) ∧
(∀i v v' ul' m.
i + 1 ≤ n ∧ Z (i + 1) v v' ∧ rel M' m (v' # ul') ⟶
(∃ul.
rel M' m (v' # ul') ∧
(∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) ∧
Z n w w'
get
nbisim Z n M M' w w' ==>
(∀i v v'. Z i v v' ⟶ i ≤ n )
(or other equivalent form, up to meta-equivalence)
I prefer the function-application approach in that case, can this be done in a quicker way?
irvin (Nov 03 2024 at 11:12):you could use mkide
irvin (Nov 03 2024 at 11:13):https://www.isa-afp.org/entries/Intro_Dest_Elim.html
Yiming Xu (Nov 03 2024 at 11:13):irvin said:
you could use mkide
I have not heard about this. Thanks for directing! Is there any minimal working example?
irvin (Nov 03 2024 at 11:14):https://www.isa-afp.org/sessions/intro_dest_elim/#IDE_Reference
Yiming Xu (Nov 03 2024 at 11:14):Let me check. I see there is a documentation, but seems very minimal.
irvin (Nov 03 2024 at 11:15):it does simple generation of intro dest and elim rules for definitions of the form A = B /\ C .. /\ N
Yiming Xu (Nov 03 2024 at 11:18):Thanks! It seems relevant. I will read it.
Mathias Fleury (Nov 03 2024 at 16:24):Yiming Xu said:
It seems not such a common approach though. May I please ask if there is a quicker way to, from:
nbisim Z n M M' w w' ≡ (∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ∧ (∀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v') ∧ (∀v v' p. Z 0 v v' ⟶ valt M p v = valt M' p v') ∧ (∀i v v' ul m. i + 1 ≤ n ∧ Z (i + 1) v v' ∧ rel M m (v # ul) ⟶ (∃ul'. rel M' m (v' # ul') ∧ (∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) ∧ (∀i v v' ul' m. i + 1 ≤ n ∧ Z (i + 1) v v' ∧ rel M' m (v' # ul') ⟶ (∃ul. rel M' m (v' # ul') ∧ (∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) ∧ Z n w w'get
nbisim Z n M M' w w' ==> (∀i v v'. Z i v v' ⟶ i ≤ n )(or other equivalent form, up to meta-equivalence)
I prefer the function-application approach in that case, can this be done in a quicker way?
You can also destroy the equivalence by hand with
nbisim_def[THEN iffD1]
Yes, but it takes multiple steps. I tried several layers and during proof I wrote sth like
nbs[unfolded nbisim_def, THEN conjunct2, THEN conjunct2,
THEN conjunct1]
It would be nice if we have something like "conjunct3, conjunct4,etc".
Yiming Xu (Nov 03 2024 at 16:26):Oh I remember it is not the main thing I am complaining about!
Yiming Xu (Nov 03 2024 at 16:26):I am not satisfied with the fact that there is no obvious way to pass the quantifier and implication to get into "i <= n" in the first conjunct.
Yiming Xu (Nov 03 2024 at 16:27):It is easy to get
nbisim Z n M M' w w' ==>
(∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M')
My problem is mainly how to easily get from the above to
nbisim Z n M M' w w' ==>
Z i v v' --> i ≤ n
Or sth like
nbisim Z n M M' w w' ==>
Z i v v' ==> i ≤ n
nbisim Z n M M' w w' ==>
!!i v v. Z i v v' ==> i ≤ n
(maybe this one is illegal...) (edit: yes it is illegal and the i's are not the same, silly me.)
Mathias Fleury (Nov 03 2024 at 16:30):First, you could change your definition to use !!
Yiming Xu (Nov 03 2024 at 16:31):It then seems to me that it would help to have a function that takes a theorem, and destroy it apart into as-meta-as-possible version, since it seems to me that conjunct1 can get underneath meta connectives.
Yiming Xu (Nov 03 2024 at 16:31):Mathias Fleury said:
First, you could change your definition to use
!!
Let me try a bit the syntax...
Mathias Fleury (Nov 03 2024 at 16:31):Second, once only one conjunct remain, you can use
lemma Q: ‹nbisim Z n M M' w w' ==>
(∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M')
›
sorry
thm Q[rule_format]
Yiming Xu said:
Mathias Fleury said:
First, you could change your definition to use
!!Let me try a bit the syntax...
A bit tricky. May I please ask, say I have 2 conjuncts:
definition nbisim ::
"(nat ⇒ 'a ⇒ 'b ⇒ bool) ⇒ nat ⇒
('m,'p,'a) model ⇒ ('m,'p,'b) model ⇒
'a ⇒ 'b ⇒ bool" where
"nbisim Z n M M' w w' ≡
(∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ∧
(∀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v')"
How would I define it use "!!"?
Mathias Fleury (Nov 03 2024 at 16:34):(but maybe read: https://proofcraft.org/blog/isabelle-style-part2.html)
Yiming Xu (Nov 03 2024 at 16:34):Mathias Fleury said:
Second, once only one conjunct remain, you can use
lemma Q: ‹nbisim Z n M M' w w' ==> (∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') › sorry thm Q[rule_format]
I see, it seems like rule_format is exactly the function I am asking for. i.e. make a theorem as meta-as-possible.
Yiming Xu (Nov 03 2024 at 16:36):Avoid theorem-transforming attributes such as `[simplified]` and `[rule_format]` in lemma statements.
Sad...
Yiming Xu (Nov 03 2024 at 16:36):But is there any concrete reason that rule_format is bad?
Yiming Xu (Nov 03 2024 at 16:37):It seems to be predictable to me. Unlike the simplifier that changes over time, I expect it to stay the same because it is very clear that what it is supposed to do.
Mathias Fleury (Nov 03 2024 at 16:37):Yiming Xu said:
But is there any concrete reason that rule_format is bad?
from a maintainers point of view: the output can change in different Isabelle version, hence you have to look at the old version to find what changed, which is annoying
Mathias Fleury (Nov 03 2024 at 16:38):but the main reason is that it goes a bit against the idea of nice Isar proofs
Yiming Xu (Nov 03 2024 at 16:39):It is helpful to have. Thank you and then I will try to only use it for proof exploration then!
Mathias Fleury (Nov 03 2024 at 16:40):Yiming Xu said:
Yiming Xu said:
Mathias Fleury said:
First, you could change your definition to use
!!Let me try a bit the syntax...
A bit tricky. May I please ask, say I have 2 conjuncts:
definition nbisim :: "(nat ⇒ 'a ⇒ 'b ⇒ bool) ⇒ nat ⇒ ('m,'p,'a) model ⇒ ('m,'p,'b) model ⇒ 'a ⇒ 'b ⇒ bool" where "nbisim Z n M M' w w' ≡ (∀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ∧ (∀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v')"How would I define it use "!!"?
ah that is really ugly because there is no conjunction in Pure. Use induction is probably better at that point
Mathias Fleury (Nov 03 2024 at 16:40):I mean this is really ugly:
definition nbisim where
"nbisim Z n M M' w w' ≡
(⋀thesis. (⋀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ⟹
(⋀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v') ⟹ thesis)"
This is unfortunately not an inductive definition.
Mathias Fleury (Nov 03 2024 at 16:40):every definition is also an inductive definition
Yiming Xu (Nov 03 2024 at 16:41):Mathias Fleury said:
I mean this is really ugly:
definition nbisim where "nbisim Z n M M' w w' ≡ (⋀thesis. (⋀i v v'. Z i v v' ⟶ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') ⟹ (⋀i v v'. i + 1 ≤ n --> Z (i + 1) v v' ⟶ Z i v v') ⟹ thesis)"
In this sense I will agree (since it is a shape of an inductive principle). I am not aware that such a thing is generated.
Yiming Xu (Nov 03 2024 at 16:42):How would you suggest reshaping it or is it even possible? I was proving little lemmas like:
lemma nbisim_bound :
assumes nbs: "nbisim Z n M M' w w'"
and Z:"Z i v v'" shows "i ≤ n"
using nbs[unfolded nbisim_def, THEN conjunct1] Z by blast
lemma nbisim_Z_world1 :
assumes nbs: "nbisim Z n M M' w w'"
and Z:"Z i v v'" shows "v ∈ world M"
using nbs[unfolded nbisim_def, THEN conjunct1] Z by simp
lemma nbisim_Z_world2 :
assumes nbs: "nbisim Z n M M' w w'"
and Z:"Z i v v'" shows "v' ∈ world M'"
using nbs[unfolded nbisim_def, THEN conjunct1] Z by simp
lemma nbisim_valt:
assumes nbs: "nbisim Z n M M' w w'"
and Z:"Z i v v'" shows "valt M p v = valt M' p v'"
proof -
from assms have "Z 0 v v'" using nbisim_chain[OF nbs] nbisim_bound[OF nbs Z]
by blast
then show ?thesis
using nbs[unfolded nbisim_def, THEN conjunct2, THEN conjunct2,
THEN conjunct1] by blast
qed
to take out the conjuncts and reshape them into rules...
Yiming Xu (Nov 03 2024 at 16:47):Umm? In which sense do we not have conjunction in Pure? We have the &&&.
Mathias Fleury (Nov 03 2024 at 16:48):inductive nbisim for Z n M M' w w' where
1: ‹nbisim Z n M M' w w'›
if ‹⋀i v v'. Z i v v' ⟹ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M'› and
‹⋀i v v'. i + 1 ≤ n ⟹ Z (i + 1) v v' ⟹ Z i v v'›
inductive_cases nbisimE: ‹nbisim Z n M M' w w'›
lemma nbisim_bound:
assumes ‹nbisim Z n M M' w w'›
shows ‹⋀i v v'. Z i v v' ⟹ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M'›
using assms by (rule nbisim.cases) blast
thm nbisim_bound[THEN conjunct2]
Wow black technology!!!
Yiming Xu (Nov 03 2024 at 16:53):So it would have the same effect as the iff, where the "inductive clauses" gives "_ /\ _ ....==> nbisim" and the induction principle gives "nbisim ==> ... /\ ...".
Mathias Fleury (Nov 03 2024 at 16:53):Yiming Xu said:
Umm? In which sense do we not have conjunction in Pure? We have the
&&&.
ah try I forgot that:
definition nbisim' where
"nbisim' Z n M M' w w' ≡
((⋀i v v'. Z i v v' ⟹ i ≤ n ∧ v ∈ world M ∧ v' ∈ world M') &&&
(⋀i v v'. i + 1 ≤ n ⟹ Z (i + 1) v v' ⟹ Z i v v'))"
thm equal_elim_rule1[OF nbisim'_def, THEN conjunctionD1]
thm equal_elim_rule1[OF nbisim'_def, THEN conjunctionD2]
thm iffD1 conjunct2
EDIT: with ⟹
Yiming Xu (Nov 03 2024 at 16:55):Ahh it works...
Yiming Xu (Nov 03 2024 at 16:57):Tried that meta-logic is happy even with
definition nbisim' where
"nbisim' Z n M M' w w' ≡
((⋀i v v'. Z i v v' ⟹ i ≤ n &&& v ∈ world M &&& v' ∈ world M') &&&
(⋀i v v'. i + 1 ≤ n ⟹ Z (i + 1) v v' ⟹ Z i v v'))"
But maybe a better idea is just to split them up into different conjuncts...
Yiming Xu (Nov 04 2024 at 09:46):I have trouble stating theorems with the new definition:
lemma nbisim_below:
assumes M: "is_model sig M"
and M': "is_model sig M'"
and nbs: "nbisim' Z n M M' w w'"
and k: "k ≤ n"
shows "nbisim' Z1 k M M' w w'"
reports error.
with error message:
Type unification failed: Clash of types "prop" and "bool"
Type error in application: incompatible operand type
Operator: Trueprop :: bool ⇒ prop
Operand: nbisim' Z n M M' w w' :: prop
What might be wrong here?
Yiming Xu (Nov 04 2024 at 09:47):I defined:
definition nbisim' where
"nbisim' Z n M M' w w' ≡
((⋀i v v'. Z i v v' ⟹ i ≤ n &&& v ∈ world M &&& v' ∈ world M') &&&
(⋀i v v'. i + 1 ≤ n ⟹ Z (i + 1) v v' ⟹ Z i v v') &&&
(⋀v v' p. Z 0 v v' ⟹ valt M p v = valt M' p v') &&&
(⋀i v v' ul m.
i + 1 ≤ n ⟹ Z (i + 1) v v' ⟹ rel M m (v # ul) ⟹
(∃ul'.
rel M' m (v' # ul') ∧
(∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) &&&
(⋀i v v' ul' m.
i + 1 ≤ n ⟹ Z (i + 1) v v' ⟹ rel M' m (v' # ul') ⟹
(∃ul.
rel M' m (v' # ul') ∧
(∀u u'. (u,u') ∈ set (zip ul ul') ⟶ Z i u u'))) &&&
Z n w w')"
definition X :: ‹_› where
‹X ≡ Trueprop True›
lemma shows "PROP X"
There is an implicit conversion from bool (the HOL thing) to prop (the Pure thing) , which is bad in this case
Mathias Fleury (Nov 04 2024 at 09:51):There is no easy way around that
Yiming Xu (Nov 04 2024 at 09:54):I checked "PROP" is not a term, so PROP is not a HOL-level function.
Mathias Fleury (Nov 04 2024 at 09:55):Trueprop is the implicit conversion
Yiming Xu (Nov 04 2024 at 09:56):I think I am confused by these subtle things. Where is the position that "Trueprop" is implicitly inserted in
lemma nbisim_below:
assumes M: "is_model sig M"
and M': "is_model sig M'"
and nbs: "nbisim' Z n M M' w w'"
and k: "k ≤ n"
shows "nbisim' Z1 k M M' w w'"
?
Mathias Fleury (Nov 04 2024 at 09:56):It is parsed as
shows "Trueprop (nbisim' Z1 k M M' w w')"
(like shows "Trueprop True")
Mathias Fleury (Nov 04 2024 at 09:57):It is (nearly) always the right thing
Yiming Xu (Nov 04 2024 at 09:58):I see, so for the meta-definition, it defines nbisim' Z1 k M M' w w' to be a prop instead of bool. And if there is any way to get rid of that, that would be to force it not to parse it as "Trueprop (nbisim' Z1 k M M' w w')", i.e. to insert the Trueprop, but to keep the original nbisim' Z1 k M M' w w'. Is that correct?
Yiming Xu (Nov 04 2024 at 09:58):And it would be tricky because parsing is at implementation level...
Mathias Fleury (Nov 04 2024 at 10:00):Yiming Xu said:
I see, so for the meta-definition, it defines
nbisim' Z1 k M M' w w'to be a prop instead of bool. And if there is any way to get rid of that, that would be to force it not to parse it as "Trueprop (nbisim' Z1 k M M' w w')", i.e. to insert the Trueprop, but to keep the originalnbisim' Z1 k M M' w w'. Is that correct?
that is what the PROP does yes
Yiming Xu (Nov 04 2024 at 10:01):lemma nbisim_below:
assumes M: "is_model sig M"
and M': "is_model sig M'"
and nbs: "nbisim' Z n M M' w w'"
and k: "k ≤ n"
shows "PROP (nbisim' Z1 k M M' w w')"
still not accepted, with the same error message. A bit unfortunate.
Yiming Xu (Nov 04 2024 at 10:02):I can live with the original definition. Thank you! That is good to know!
Mathias Fleury (Nov 04 2024 at 10:02):and nbs: "nbisim' Z n M M' w w'"
needs to be fixed too
Yiming Xu (Nov 04 2024 at 10:04):Vielen Danke that works!
Yiming Xu (Nov 04 2024 at 10:04):lemma nbisim_below:
assumes M: "(is_model sig M)"
and M': "(is_model sig M')"
and nbs: "PROP (nbisim' Z n M M' w w')"
and k: "k ≤ n"
shows "PROP (nbisim' Z1 k M M' w w')" unfolding nbisim'_def
That is what is accepted.
Last updated: Dec 21 2024 at 16:20 UTC