Kevin Lee (Jul 06 2023 at 17:20): Kevin Lee (Jul 06 2023 at 17:20):Given have "⟦i ∈ {0..m-1}; j ∈ {0..m-1}; (f i) mod m = (f j) mod m⟧ ⟹ i = j", how can I show
"∀i ∈ {0..m-1}. ∀j ∈ {0..m-1}. (f i) mod m = (f j) mod m ⟶ i = j"?
Wolfgang Jeltsch (Jul 06 2023 at 17:51):By using the introduction rules for ∀ and →, which are named something like allI and impI. The standard method is doing that for ∀ and →; so something like standard+ might work (but could apply standard too often).
In general it’s advisable to stay away from object logic counterparts of meta-logic connectors as much as possible, as Isar and the proof methods are tailored towards the meta-logic (and are to a large degree not specific to HOL). So avoid ∀, →, and ∧ where you can, as long as it doesn’t create really unreasonable situations. :smile: In definitions of predicates, for example, you still need them, because you need to construct booleans, which don’t exist on the meta-level, but statements like yours above should be made using the meta-logic and thus rather be treated as logical derivation rules instead of single logical statements.
Jan van Brügge (Jul 07 2023 at 07:16):In this case you would need ballI not allI because of forall _ in _. But yeah, don't use HOL quantifiers in theorems if you don't have to
Kevin Lee (Jul 07 2023 at 16:15):Thanks!
Last updated: Nov 13 2025 at 04:27 UTC