Email Gateway (Aug 22 2022 at 18:51): Email Gateway (Aug 22 2022 at 18:51):From: Denis Nikiforov <denis.nikif@gmail.com>
Hi
I'm trying to describe semantics of the Object Constraint Language:
https://github.com/AresEkb/Simple_OCL
I've almost described its type system. The last lemma I can't prove is that
the typing rules are deterministic:
https://github.com/AresEkb/Simple_OCL/blob/master/OCL_Typing.thy
lemma
typing_det: "Γ1 ⊢ expr : τ1 ⟹ Γ1 ⊢ expr : σ1 ⟹ τ1 = σ1" and
collection_parts_typing_det:
"collection_parts_typing Γ2 prts τ2 ⟹
collection_parts_typing Γ2 prts σ2 ⟹ τ2 = σ2" and
iterator_typing_det:
"iterator_typing Γ3 src its body τ31 σ31 ρ31 ⟹
iterator_typing Γ3 src its body τ32 σ32 ρ32 ⟹
τ31 = τ32 ∧ σ31 = σ32 ∧ ρ31 = ρ32"
The problem is that I can't apply any of the following induction rules to
my lemmas:
apply (induct expr and prts and src body)
apply (induct rule:
typing_collection_parts_typing_iterator_typing.inducts)
These answers doesn't help me:
https://stackoverflow.com/questions/53905744/how-to-prove-lemmas-for-mutually-recursive-types/53906944
https://stackoverflow.com/questions/33020622/how-to-fix-illegal-schematic-variables-in-mutually-recursive-rule-induction
Everithing works fine on simple examples. But my predicates are more
complicated. And I can't localize what's wrong with my definitions. I can't
reproduce the problem on a simpler example.
Could you help me to understand what induction rule I should apply to this
lemma?
Email Gateway (Aug 22 2022 at 18:51):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Denis,
I haven't tried out your example, but I've seen that your typing
judgements contain type variables in their types. So I suspect that the
types in your lemma are too general: All three statements contain
different variables, so Isabelle will type-check them with different
type variables. The induct proof method then cannot apply the rule,
which requires all type variables to match like in the inductive
definition. I suggest that you constrain all contexts to the same type,
e.g., using
lemma fixes Γ1 Γ2 Γ3 :: "'a :: semilatice_sup type env" shows
Hope this helps
Andreas
Email Gateway (Aug 22 2022 at 18:51):From: Denis Nikiforov <denis.nikif@gmail.com>
Hi Andreas,
Thanks! It was one of the problems. As I see now I can use the same
variables (just Γ instead of Γ1 Γ2 Γ3) in these lemmas. Also I should
specify all variables used in the induction rule.
The following works:
lemma
typing_det: "Γ ⊢ expr : τ ⟹ Γ ⊢ expr : σ ⟹ τ = σ" and
collection_parts_typing_det:
"collection_parts_typing Γ prts τ ⟹
collection_parts_typing Γ prts σ ⟹ τ = σ" and
iterator_typing_det:
"iterator_typing Γ src its body τ⇩1 σ⇩1 ρ⇩1 ⟹
iterator_typing Γ src its body τ⇩2 σ⇩2 ρ⇩2 ⟹
τ⇩1 = τ⇩2 ∧ σ⇩1 = σ⇩2 ∧ ρ⇩1 = ρ⇩2"
proof (induct Γ expr τ and Γ prts τ and Γ src its body τ⇩1 σ⇩1 ρ⇩1
arbitrary: σ and σ and τ⇩2 σ⇩2 ρ⇩2
rule: typing_collection_parts_typing_iterator_typing.inducts)
It was very tricky for me to understand that I should specify both
induction rule and all induction variables. Non-mutual induction doesn't
require it.
вт, 25 дек. 2018 г. в 21:44, Andreas Lochbihler <mail@andreas-lochbihler.de
Last updated: Apr 25 2024 at 20:15 UTC