diff options
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index d80503f..b8e6809 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -271,9 +271,9 @@ section Freshness We also write Π a, P for for_fresh (fun a => P), using the cyrillic letter Π. -A proposition holds for "suitably fresh" atoms iff there are infinitely many such "suitably fresh" atoms to choose from. -/ +A proposition holds for "suitably fresh" atoms iff the set of atoms that are not "suitably fresh" is finite. -/ def NominalSet.ForFresh {πΈ : Type} [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] (P : πΈ β Prop) : Prop := - {a : πΈ | P a}.Infinite + {a : πΈ | P a}αΆ.Finite macro "Π" x:ident "," t:term : term => `(NominalSet.ForFresh (fun $x => $t)) @@ -318,6 +318,8 @@ lemma fresh_swap_fix {a b : πΈ} {x : X} : a # x β b # x β βΈ¨a, bβΈ© β P /-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ lemma for_fresh_exists {P : πΈ β Prop} : (Π a, P a) β (β a, P a) := by simp only [ForFresh]; intro h + apply Set.Finite.infinite_compl at h + rw [compl_compl] at h exact h.nonempty /-- Extensionality lemma for the freshness quantifier. -/ @@ -327,6 +329,18 @@ lemma for_fresh_ext {P Q : πΈ β Prop} : (β a, P a β Q a) β (Π a, P a) suffices {a | P a} = {a | Q a} by rw [this] exact Set.ext h +/-- The freshness quantifier preserves implications. -/ +lemma for_fresh_imp {P Q : πΈ β Prop} : (Π a, P a) β (β a, P a β Q a) β (Π a, Q a) := by + intro hfin himp + apply Set.Finite.subset + Β· exact hfin + Β· simp only [Set.compl_subset_compl, Set.setOf_subset_setOf] + exact himp + +/-- The freshness quantifier commutes with conjunctions. -/ +lemma for_fresh_and {P Q : πΈ β Prop} : (Π a, P a) β§ (Π a, Q a) β (Π a, P a β§ Q a) := by + simp [ForFresh, Set.setOf_and, Set.compl_inter] + end NominalSet end Freshness |