Yiming Xu (Oct 12 2024 at 04:56): Yiming Xu (Oct 12 2024 at 04:56):My goal looks like:
⋀x vl.
cwff (τ, Φ) (cBOX m fl) ⟹
∀m wl. R m wl ⟶ length wl = Suc (snd τ m) ⟹
∀m wl. R m wl ⟶ list_all (λw. w ∈ W) wl ⟹
∀m. Ex (R m) ⟶ m ∈ fst τ ⟹
x ∈ W ⟹
csatis (τ, Φ) (W, R, V) w (cBOX m fl) ⟹
length vl = length fl ⟹
R m (w # vl) ⟹
∃i<length fl.
csatis (τ, Φ) (W, R, V) (vl ! i) (fl ! i)
I would like to write in the format
fix w vl
assume ...
show...
I wrote:
fix w vl
assume "length vl = length fl"
then show
"∃i<length fl.
csatis (τ, Φ) (W, R, V) (vl ! i) (fl ! i)"
The color looks like:
image.png
Yiming Xu (Oct 12 2024 at 05:00):I do not understand why is the type error. I think the fixed variables should automatically have the type that the goal wants. If I delete the assume... then, then the error goes away.
Yiming Xu (Oct 12 2024 at 05:01):May I please ask why is this type error, and how should I solve that?
Mathias Fleury (Oct 12 2024 at 05:52):Add the types you need in the fix. Usually the type inference does the right thing, but not always.
Yiming Xu (Oct 12 2024 at 05:55):Sorry, what is the syntax?
fix w "vl::'b list" does not seem to work.
Yiming Xu (Oct 12 2024 at 05:58):It says: Legacy feature! Bad name binding: "vl::'d list"⌂
Mathias Fleury (Oct 12 2024 at 06:00):$ grep -r --include \*.thy " fix " * | grep "::" | head
thys/WebAssembly/Wasm_Interpreter.thy: fix xs::"e list" and as b bs
thys/Physical_Quantities/ISQ_Dimensions.thy: fix x y :: "'n list"
thys/Multitape_To_Singletape_TM/STM_Renaming.thy: fix trans :: "('q \<times> 'a \<times> 'q \<times> 'a \<times> dir)"
thys/Multitape_To_Singletape_TM/Multi_Single_TM_Translation.thy: fix x :: "('a, 'k) st_tape_symbol list"
thys/Multitape_To_Singletape_TM/Multi_Single_TM_Translation.thy: fix x :: "('a, 'k) st_tape_symbol list"
thys/Nullstellensatz/Univariate_PM.thy: fix x::'x and p::"'a poly"
thys/Nullstellensatz/Nullstellensatz.thy: fix A B :: "('x \<Rightarrow> 'a) set"
thys/Nullstellensatz/Nullstellensatz.thy: fix F G :: "(('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) set"
thys/Nullstellensatz/Nullstellensatz.thy: fix p and a::"'x \<Rightarrow> 'a"
thys/LambdaAuth/FMap_Lemmas.thy: fix p and f :: "'a \<rightharpoonup> 'b"
When something does not work, look at how others are doing it
Yiming Xu (Oct 12 2024 at 06:02):Thanks a lot for always attempting to teaching me how to fishing instead of just giving me the fish!
Mathias Fleury (Oct 12 2024 at 06:07):Yiming Xu said:
It says: Legacy feature! Bad name binding: "vl::'d list"⌂
BTW: this warning means that you gave the name vl::'d list to a single constant (yes the full thing). It is legacy since I am using Isabelle and it is feature you never want.
Yiming Xu (Oct 12 2024 at 06:09):By "the full thing", may I please confirm that Isabelle thinks "`vl::'d list" is a name, not a type-annotated term?
Mathias Fleury (Oct 12 2024 at 06:09):Exactly
Yiming Xu (Oct 12 2024 at 06:10):Yes indeed I never want this, very surprising. Thank you!
Mathias Fleury (Oct 12 2024 at 06:12):Isabelle 2024 does not seem to accept that at all anymore
Yiming Xu (Oct 12 2024 at 06:13):I am using Isabelle 2024. I still see this error. I will be careful with that.
Last updated: Dec 21 2024 at 16:20 UTC