Theory Predicates
chapter‹Basic Predicates›
theory Predicates
imports SyntaxN
begin
section ‹The Subset Relation›
nominal_function Subset :: "tm ⇒ tm ⇒ fm" (infixr "SUBS" 150)
where "atom z ♯ (t, u) ⟹ t SUBS u = All2 z t ((Var z) IN u)"
by (auto simp: eqvt_def Subset_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
declare Subset.simps [simp del]
lemma Subset_fresh_iff [simp]: "a ♯ t SUBS u ⟷ a ♯ t ∧ a ♯ u"
apply (rule obtain_fresh [where x="(t, u)"])
apply (subst Subset.simps, auto)
done
lemma subst_fm_Subset [simp]: "(t SUBS u)(i::=x) = (subst i x t) SUBS (subst i x u)"
proof -
obtain j::name where "atom j ♯ (i,x,t,u)"
by (rule obtain_fresh)
thus ?thesis
by (auto simp: Subset.simps [of j])
qed
lemma Subset_I:
assumes "insert ((Var i) IN t) H ⊢ (Var i) IN u" "atom i ♯ (t,u)" "∀B ∈ H. atom i ♯ B"
shows "H ⊢ t SUBS u"
by (subst Subset.simps [of i]) (auto simp: assms)
lemma Subset_D:
assumes major: "H ⊢ t SUBS u" and minor: "H ⊢ a IN t" shows "H ⊢ a IN u"
proof -
obtain i::name where i: "atom i ♯ (t, u)"
by (rule obtain_fresh)
hence "H ⊢ (Var i IN t IMP Var i IN u) (i::=a)"
by (metis Subset.simps major All_D)
thus ?thesis
using i by simp (metis MP_same minor)
qed
lemma Subset_E: "H ⊢ t SUBS u ⟹ H ⊢ a IN t ⟹ insert (a IN u) H ⊢ A ⟹ H ⊢ A"
by (metis Subset_D cut_same)
lemma Subset_cong: "H ⊢ t EQ t' ⟹ H ⊢ u EQ u' ⟹ H ⊢ t SUBS u IFF t' SUBS u'"
by (rule P2_cong) auto
lemma Set_MP: "x SUBS y ∈ H ⟹ z IN x ∈ H ⟹ insert (z IN y) H ⊢ A ⟹ H ⊢ A"
by (metis Assume Subset_D cut_same insert_absorb)
lemma Zero_Subset_I [intro!]: "H ⊢ Zero SUBS t"
proof -
have "{} ⊢ Zero SUBS t"
by (rule obtain_fresh [where x="(Zero,t)"]) (auto intro: Subset_I)
thus ?thesis
by (auto intro: thin)
qed
lemma Zero_SubsetE: "H ⊢ A ⟹ insert (Zero SUBS X) H ⊢ A"
by (rule thin1)
lemma Subset_Zero_D:
assumes "H ⊢ t SUBS Zero" shows "H ⊢ t EQ Zero"
proof -
obtain i::name where i [iff]: "atom i ♯ t"
by (rule obtain_fresh)
have "{t SUBS Zero} ⊢ t EQ Zero"
proof (rule Eq_Zero_I)
fix A
show "{Var i IN t, t SUBS Zero} ⊢ A"
by (metis Hyp Subset_D insertI1 thin1 Mem_Zero_E cut1)
qed auto
thus ?thesis
by (metis assms cut1)
qed
lemma Subset_refl: "H ⊢ t SUBS t"
proof -
obtain i::name where "atom i ♯ t"
by (rule obtain_fresh)
thus ?thesis
by (metis Assume Subset_I empty_iff fresh_Pair thin0)
qed
lemma Eats_Subset_Iff: "H ⊢ Eats x y SUBS z IFF (x SUBS z) AND (y IN z)"
proof -
obtain i::name where i: "atom i ♯ (x,y,z)"
by (rule obtain_fresh)
have "{} ⊢ (Eats x y SUBS z) IFF (x SUBS z AND y IN z)"
proof (rule Iff_I)
show "{Eats x y SUBS z} ⊢ x SUBS z AND y IN z"
proof (rule Conj_I)
show "{Eats x y SUBS z} ⊢ x SUBS z"
apply (rule Subset_I [where i=i]) using i
apply (auto intro: Subset_D Mem_Eats_I1)
done
next
show "{Eats x y SUBS z} ⊢ y IN z"
by (metis Subset_D Assume Mem_Eats_I2 Refl)
qed
next
show "{x SUBS z AND y IN z} ⊢ Eats x y SUBS z" using i
by (auto intro!: Subset_I [where i=i] intro: Subset_D Mem_cong [THEN Iff_MP2_same])
qed
thus ?thesis
by (rule thin0)
qed
lemma Eats_Subset_I [intro!]: "H ⊢ x SUBS z ⟹ H ⊢ y IN z ⟹ H ⊢ Eats x y SUBS z"
by (metis Conj_I Eats_Subset_Iff Iff_MP2_same)
lemma Eats_Subset_E [intro!]:
"insert (x SUBS z) (insert (y IN z) H) ⊢ C ⟹ insert (Eats x y SUBS z) H ⊢ C"
by (metis Conj_E Eats_Subset_Iff Iff_MP_left')
text‹A surprising proof: a consequence of @{thm Eats_Subset_Iff} and reflexivity!›
lemma Subset_Eats_I [intro!]: "H ⊢ x SUBS Eats x y"
by (metis Conj_E1 Eats_Subset_Iff Iff_MP_same Subset_refl)
lemma SUCC_Subset_I [intro!]: "H ⊢ x SUBS z ⟹ H ⊢ x IN z ⟹ H ⊢ SUCC x SUBS z"
by (metis Eats_Subset_I SUCC_def)
lemma SUCC_Subset_E [intro!]:
"insert (x SUBS z) (insert (x IN z) H) ⊢ C ⟹ insert (SUCC x SUBS z) H ⊢ C"
by (metis Eats_Subset_E SUCC_def)
lemma Subset_trans0: "{ a SUBS b, b SUBS c } ⊢ a SUBS c"
proof -
obtain i::name where [simp]: "atom i ♯ (a,b,c)"
by (rule obtain_fresh)
show ?thesis
by (rule Subset_I [of i]) (auto intro: Subset_D)
qed
lemma Subset_trans: "H ⊢ a SUBS b ⟹ H ⊢ b SUBS c ⟹ H ⊢ a SUBS c"
by (metis Subset_trans0 cut2)
lemma Subset_SUCC: "H ⊢ a SUBS (SUCC a)"
by (metis SUCC_def Subset_Eats_I)
lemma All2_Subset_lemma: "atom l ♯ (k',k) ⟹ {P} ⊢ P' ⟹ {All2 l k P, k' SUBS k} ⊢ All2 l k' P'"
apply auto
apply (rule Ex_I [where x = "Var l"])
apply (auto intro: ContraProve Set_MP cut1)
done
lemma All2_Subset: "⟦H ⊢ All2 l k P; H ⊢ k' SUBS k; {P} ⊢ P'; atom l ♯ (k', k)⟧ ⟹ H ⊢ All2 l k' P'"
by (rule cut2 [OF All2_Subset_lemma]) auto
section‹Extensionality›
lemma Extensionality: "H ⊢ x EQ y IFF x SUBS y AND y SUBS x"
proof -
obtain i::name and j::name and k::name
where atoms: "atom i ♯ (x,y)" "atom j ♯ (i,x,y)" "atom k ♯ (i,j,y)"
by (metis obtain_fresh)
have "{} ⊢ (Var i EQ y IFF Var i SUBS y AND y SUBS Var i)" (is "{} ⊢ ?scheme")
proof (rule Ind [of j])
show "atom j ♯ (i, ?scheme)" using atoms
by simp
next
show "{} ⊢ ?scheme(i::=Zero)" using atoms
proof auto
show "{Zero EQ y} ⊢ y SUBS Zero"
by (rule Subset_cong [OF Assume Refl, THEN Iff_MP_same]) (rule Subset_refl)
next
show "{Zero SUBS y, y SUBS Zero} ⊢ Zero EQ y"
by (metis AssumeH(2) Subset_Zero_D Sym)
qed
next
show "{} ⊢ All i (All j (?scheme IMP ?scheme(i::=Var j) IMP ?scheme(i::=Eats (Var i) (Var j))))"
using atoms
apply auto
apply (metis Subset_cong [OF Refl Assume, THEN Iff_MP_same] Subset_Eats_I)
apply (metis Mem_cong [OF Refl Assume, THEN Iff_MP_same] Mem_Eats_I2 Refl)
apply (metis Subset_cong [OF Assume Refl, THEN Iff_MP_same] Subset_refl)
apply (rule Eq_Eats_I [of _ k, THEN Sym])
apply (auto intro: Set_MP [where x=y] Subset_D [where t = "Var i"] Disj_I1 Disj_I2)
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], auto)
done
qed
hence "{} ⊢ (Var i EQ y IFF Var i SUBS y AND y SUBS Var i)(i::=x)"
by (metis Subst emptyE)
thus ?thesis using atoms
by (simp add: thin0)
qed
lemma Equality_I: "H ⊢ y SUBS x ⟹ H ⊢ x SUBS y ⟹ H ⊢ x EQ y"
by (metis Conj_I Extensionality Iff_MP2_same)
lemma EQ_imp_SUBS: "insert (t EQ u) H ⊢ (t SUBS u)"
proof -
have "{t EQ u} ⊢ (t SUBS u)"
by (metis Assume Conj_E Extensionality Iff_MP_left')
thus ?thesis
by (metis Assume cut1)
qed
lemma EQ_imp_SUBS2: "insert (u EQ t) H ⊢ (t SUBS u)"
by (metis EQ_imp_SUBS Sym_L)
lemma Equality_E: "insert (t SUBS u) (insert (u SUBS t) H) ⊢ A ⟹ insert (t EQ u) H ⊢ A"
by (metis Conj_E Extensionality Iff_MP_left')
section ‹The Disjointness Relation›
text‹The following predicate is defined in order to prove Lemma 2.3, Foundation›
nominal_function Disjoint :: "tm ⇒ tm ⇒ fm"
where "atom z ♯ (t, u) ⟹ Disjoint t u = All2 z t (Neg ((Var z) IN u))"
by (auto simp: eqvt_def Disjoint_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
declare Disjoint.simps [simp del]
lemma Disjoint_fresh_iff [simp]: "a ♯ Disjoint t u ⟷ a ♯ t ∧ a ♯ u"
proof -
obtain j::name where j: "atom j ♯ (a,t,u)"
by (rule obtain_fresh)
thus ?thesis
by (auto simp: Disjoint.simps [of j])
qed
lemma subst_fm_Disjoint [simp]:
"(Disjoint t u)(i::=x) = Disjoint (subst i x t) (subst i x u)"
proof -
obtain j::name where j: "atom j ♯ (i,x,t,u)"
by (rule obtain_fresh)
thus ?thesis
by (auto simp: Disjoint.simps [of j])
qed
lemma Disjoint_cong: "H ⊢ t EQ t' ⟹ H ⊢ u EQ u' ⟹ H ⊢ Disjoint t u IFF Disjoint t' u'"
by (rule P2_cong) auto
lemma Disjoint_I:
assumes "insert ((Var i) IN t) (insert ((Var i) IN u) H) ⊢ Fls"
"atom i ♯ (t,u)" "∀B ∈ H. atom i ♯ B"
shows "H ⊢ Disjoint t u"
by (subst Disjoint.simps [of i]) (auto simp: assms insert_commute)
lemma Disjoint_E:
assumes major: "H ⊢ Disjoint t u" and minor: "H ⊢ a IN t" "H ⊢ a IN u" shows "H ⊢ A"
proof -
obtain i::name where i: "atom i ♯ (t, u)"
by (rule obtain_fresh)
hence "H ⊢ (Var i IN t IMP Neg (Var i IN u)) (i::=a)"
by (metis Disjoint.simps major All_D)
thus ?thesis using i
by simp (metis MP_same Neg_D minor)
qed
lemma Disjoint_commute: "{ Disjoint t u } ⊢ Disjoint u t"
proof -
obtain i::name where "atom i ♯ (t,u)"
by (rule obtain_fresh)
thus ?thesis
by (auto simp: fresh_Pair intro: Disjoint_I Disjoint_E)
qed
lemma Disjoint_commute_I: "H ⊢ Disjoint t u ⟹ H ⊢ Disjoint u t"
by (metis Disjoint_commute cut1)
lemma Disjoint_commute_D: "insert (Disjoint t u) H ⊢ A ⟹ insert (Disjoint u t) H ⊢ A"
by (metis Assume Disjoint_commute_I cut_same insert_commute thin1)
lemma Zero_Disjoint_I1 [iff]: "H ⊢ Disjoint Zero t"
proof -
obtain i::name where i: "atom i ♯ t"
by (rule obtain_fresh)
hence "{} ⊢ Disjoint Zero t"
by (auto intro: Disjoint_I [of i])
thus ?thesis
by (metis thin0)
qed
lemma Zero_Disjoint_I2 [iff]: "H ⊢ Disjoint t Zero"
by (metis Disjoint_commute Zero_Disjoint_I1 cut1)
lemma Disjoint_Eats_D1: "{ Disjoint (Eats x y) z } ⊢ Disjoint x z"
proof -
obtain i::name where i: "atom i ♯ (x,y,z)"
by (rule obtain_fresh)
show ?thesis
apply (rule Disjoint_I [of i])
apply (blast intro: Disjoint_E Mem_Eats_I1)
using i apply auto
done
qed
lemma Disjoint_Eats_D2: "{ Disjoint (Eats x y) z } ⊢ Neg(y IN z)"
proof -
obtain i::name where i: "atom i ♯ (x,y,z)"
by (rule obtain_fresh)
show ?thesis
by (force intro: Disjoint_E [THEN rotate2] Mem_Eats_I2)
qed
lemma Disjoint_Eats_E:
"insert (Disjoint x z) (insert (Neg(y IN z)) H) ⊢ A ⟹ insert (Disjoint (Eats x y) z) H ⊢ A"
apply (rule cut_same [OF cut1 [OF Disjoint_Eats_D2, OF Assume]])
apply (rule cut_same [OF cut1 [OF Disjoint_Eats_D1, OF Hyp]])
apply (auto intro: thin)
done
lemma Disjoint_Eats_E2:
"insert (Disjoint z x) (insert (Neg(y IN z)) H) ⊢ A ⟹ insert (Disjoint z (Eats x y)) H ⊢ A"
by (metis Disjoint_Eats_E Disjoint_commute_D)
lemma Disjoint_Eats_Imp: "{ Disjoint x z, Neg(y IN z) } ⊢ Disjoint (Eats x y) z"
proof -
obtain i::name where"atom i ♯ (x,y,z)"
by (rule obtain_fresh)
then show ?thesis
by (auto intro: Disjoint_I [of i] Disjoint_E [THEN rotate3]
Mem_cong [OF Assume Refl, THEN Iff_MP_same])
qed
lemma Disjoint_Eats_I [intro!]: "H ⊢ Disjoint x z ⟹ insert (y IN z) H ⊢ Fls ⟹ H ⊢ Disjoint (Eats x y) z"
by (metis Neg_I cut2 [OF Disjoint_Eats_Imp])
lemma Disjoint_Eats_I2 [intro!]: "H ⊢ Disjoint z x ⟹ insert (y IN z) H ⊢ Fls ⟹ H ⊢ Disjoint z (Eats x y)"
by (metis Disjoint_Eats_I Disjoint_commute cut1)
section ‹The Foundation Theorem›
lemma Foundation_lemma:
assumes i: "atom i ♯ z"
shows "{ All2 i z (Neg (Disjoint (Var i) z)) } ⊢ Neg (Var i IN z) AND Disjoint (Var i) z"
proof -
obtain j::name where j: "atom j ♯ (z,i)"
by (metis obtain_fresh)
show ?thesis
apply (rule Ind [of j]) using i j
apply auto
apply (rule Ex_I [where x=Zero], auto)
apply (rule Ex_I [where x="Eats (Var i) (Var j)"], auto)
apply (metis ContraAssume insertI1 insert_commute)
apply (metis ContraProve Disjoint_Eats_Imp rotate2 thin1)
apply (metis Assume Disj_I1 anti_deduction rotate3)
done
qed
theorem Foundation: "atom i ♯ z ⟹ {} ⊢ All2 i z (Neg (Disjoint (Var i) z)) IMP z EQ Zero"
apply auto
apply (rule Eq_Zero_I)
apply (rule cut_same [where A = "(Neg ((Var i) IN z) AND Disjoint (Var i) z)"])
apply (rule Foundation_lemma [THEN cut1], auto)
done
lemma Mem_Neg_refl: "{} ⊢ Neg (x IN x)"
proof -
obtain i::name where i: "atom i ♯ x"
by (metis obtain_fresh)
have "{} ⊢ Disjoint x (Eats Zero x)"
apply (rule cut_same [OF Foundation [where z = "Eats Zero x"]]) using i
apply auto
apply (rule cut_same [where A = "Disjoint x (Eats Zero x)"])
apply (metis Assume thin1 Disjoint_cong [OF Assume Refl, THEN Iff_MP_same])
apply (metis Assume AssumeH(4) Disjoint_E Mem_Eats_I2 Refl)
done
thus ?thesis
by (metis Disjoint_Eats_D2 Disjoint_commute cut_same)
qed
lemma Mem_refl_E [intro!]: "insert (x IN x) H ⊢ A"
by (metis Disj_I1 Mem_Neg_refl anti_deduction thin0)
lemma Mem_non_refl: assumes "H ⊢ x IN x" shows "H ⊢ A"
by (metis Mem_refl_E assms cut_same)
lemma Mem_Neg_sym: "{ x IN y, y IN x } ⊢ Fls"
proof -
obtain i::name where i: "atom i ♯ (x,y)"
by (metis obtain_fresh)
have "{} ⊢ Disjoint x (Eats Zero y) OR Disjoint y (Eats Zero x)"
apply (rule cut_same [OF Foundation [where i=i and z = "Eats (Eats Zero y) x"]]) using i
apply (auto intro!: Disjoint_Eats_E2 [THEN rotate2])
apply (rule Disj_I2, auto)
apply (metis Assume EQ_imp_SUBS2 Subset_D insert_commute)
apply (blast intro!: Disj_I1 Disjoint_cong [OF Hyp Refl, THEN Iff_MP_same])
done
thus ?thesis
by (auto intro: cut0 Disjoint_Eats_E2)
qed
lemma Mem_not_sym: "insert (x IN y) (insert (y IN x) H) ⊢ A"
by (rule cut_thin [OF Mem_Neg_sym]) auto
section ‹The Ordinal Property›
nominal_function OrdP :: "tm ⇒ fm"
where "⟦atom y ♯ (x, z); atom z ♯ x⟧ ⟹
OrdP x = All2 y x ((Var y) SUBS x AND All2 z (Var y) ((Var z) SUBS (Var y)))"
by (auto simp: eqvt_def OrdP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows OrdP_fresh_iff [simp]: "a ♯ OrdP x ⟷ a ♯ x" (is ?thesis1)
proof -
obtain z::name and y::name where "atom z ♯ x" "atom y ♯ (x, z)"
by (metis obtain_fresh)
thus ?thesis1
by (auto simp: OrdP.simps [of y _ z] Ord_def Transset_def)
qed
lemma subst_fm_OrdP [simp]: "(OrdP t)(i::=x) = OrdP (subst i x t)"
proof -
obtain z::name and y::name where "atom z ♯ (t,i,x)" "atom y ♯ (t,i,x,z)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: OrdP.simps [of y _ z])
qed
lemma OrdP_cong: "H ⊢ x EQ x' ⟹ H ⊢ OrdP x IFF OrdP x'"
by (rule P1_cong) auto
lemma OrdP_Mem_lemma:
assumes z: "atom z ♯ (k,l)" and l: "insert (OrdP k) H ⊢ l IN k"
shows "insert (OrdP k) H ⊢ l SUBS k AND All2 z l (Var z SUBS l)"
proof -
obtain y::name where y: "atom y ♯ (k,l,z)"
by (metis obtain_fresh)
have "insert (OrdP k) H
⊢ (Var y IN k IMP (Var y SUBS k AND All2 z (Var y) (Var z SUBS Var y)))(y::=l)"
by (rule All_D) (simp add: OrdP.simps [of y _ z] y z Assume)
also have "... = l IN k IMP (l SUBS k AND All2 z l (Var z SUBS l))"
using y z by simp
finally show ?thesis
by (metis MP_same l)
qed
lemma OrdP_Mem_E:
assumes "atom z ♯ (k,l)"
"insert (OrdP k) H ⊢ l IN k"
"insert (l SUBS k) (insert (All2 z l (Var z SUBS l)) H) ⊢ A"
shows "insert (OrdP k) H ⊢ A"
apply (rule OrdP_Mem_lemma [THEN cut_same])
apply (auto simp: insert_commute)
apply (blast intro: assms thin1)+
done
lemma OrdP_Mem_imp_Subset:
assumes k: "H ⊢ k IN l" and l: "H ⊢ OrdP l" shows "H ⊢ k SUBS l"
apply (rule obtain_fresh [of "(l,k)"])
apply (rule cut_same [OF l])
using k apply (auto intro: OrdP_Mem_E thin1)
done
lemma SUCC_Subset_Ord_lemma: "{ k' IN k, OrdP k } ⊢ SUCC k' SUBS k"
by auto (metis Assume thin1 OrdP_Mem_imp_Subset)
lemma SUCC_Subset_Ord: "H ⊢ k' IN k ⟹ H ⊢ OrdP k ⟹ H ⊢ SUCC k' SUBS k"
by (blast intro!: cut2 [OF SUCC_Subset_Ord_lemma])
lemma OrdP_Trans_lemma: "{ OrdP k, i IN j, j IN k } ⊢ i IN k"
proof -
obtain m::name where "atom m ♯ (i,j,k)"
by (metis obtain_fresh)
thus ?thesis
by (auto intro: OrdP_Mem_E [of m k j] Subset_D [THEN rotate3])
qed
lemma OrdP_Trans: "H ⊢ OrdP k ⟹ H ⊢ i IN j ⟹ H ⊢ j IN k ⟹ H ⊢ i IN k"
by (blast intro: cut3 [OF OrdP_Trans_lemma])
lemma Ord_IN_Ord0:
assumes l: "H ⊢ l IN k"
shows "insert (OrdP k) H ⊢ OrdP l"
proof -
obtain z::name and y::name where z: "atom z ♯ (k,l)" and y: "atom y ♯ (k,l,z)"
by (metis obtain_fresh)
have "{Var y IN l, OrdP k, l IN k} ⊢ All2 z (Var y) (Var z SUBS Var y)" using y z
apply (simp add: insert_commute [of _ "OrdP k"])
apply (auto intro: OrdP_Mem_E [of z k "Var y"] OrdP_Trans_lemma del: All_I Neg_I)
done
hence "{OrdP k, l IN k} ⊢ OrdP l" using z y
apply (auto simp: OrdP.simps [of y l z])
apply (simp add: insert_commute [of _ "OrdP k"])
apply (rule OrdP_Mem_E [of y k l], simp_all)
apply (metis Assume thin1)
apply (rule All_E [where x= "Var y", THEN thin1], simp)
apply (metis Assume anti_deduction insert_commute)
done
thus ?thesis
by (metis (full_types) Assume l cut2 thin1)
qed
lemma Ord_IN_Ord: "H ⊢ l IN k ⟹ H ⊢ OrdP k ⟹ H ⊢ OrdP l"
by (metis Ord_IN_Ord0 cut_same)
lemma OrdP_I:
assumes "insert (Var y IN x) H ⊢ (Var y) SUBS x"
and "insert (Var z IN Var y) (insert (Var y IN x) H) ⊢ (Var z) SUBS (Var y)"
and "atom y ♯ (x, z)" "∀B ∈ H. atom y ♯ B" "atom z ♯ x" "∀B ∈ H. atom z ♯ B"
shows "H ⊢ OrdP x"
using assms by auto
lemma OrdP_Zero [simp]: "H ⊢ OrdP Zero"
proof -
obtain y::name and z::name where "atom y ♯ z"
by (rule obtain_fresh)
hence "{} ⊢ OrdP Zero"
by (auto intro: OrdP_I [of y _ _ z])
thus ?thesis
by (metis thin0)
qed
lemma OrdP_SUCC_I0: "{ OrdP k } ⊢ OrdP (SUCC k)"
proof -
obtain w::name and y::name and z::name where atoms: "atom w ♯ (k,y,z)" "atom y ♯ (k,z)" "atom z ♯ k"
by (metis obtain_fresh)
have 1: "{Var y IN SUCC k, OrdP k} ⊢ Var y SUBS SUCC k"
apply (rule Mem_SUCC_E)
apply (rule OrdP_Mem_E [of w _ "Var y", THEN rotate2]) using atoms
apply auto
apply (metis Assume Subset_SUCC Subset_trans)
apply (metis EQ_imp_SUBS Subset_SUCC Subset_trans)
done
have in_case: "{Var y IN k, Var z IN Var y, OrdP k} ⊢ Var z SUBS Var y"
apply (rule OrdP_Mem_E [of w _ "Var y", THEN rotate3]) using atoms
apply (auto intro: All2_E [THEN thin1])
done
have "{Var y EQ k, Var z IN k, OrdP k} ⊢ Var z SUBS Var y"
by (metis AssumeH(2) AssumeH(3) EQ_imp_SUBS2 OrdP_Mem_imp_Subset Subset_trans)
hence eq_case: "{Var y EQ k, Var z IN Var y, OrdP k} ⊢ Var z SUBS Var y"
by (rule cut3) (auto intro: EQ_imp_SUBS [THEN cut1] Subset_D)
have 2: "{Var z IN Var y, Var y IN SUCC k, OrdP k} ⊢ Var z SUBS Var y"
by (metis rotate2 Mem_SUCC_E in_case eq_case)
show ?thesis
apply (rule OrdP_I [OF 1 2])
using atoms apply auto
done
qed
lemma OrdP_SUCC_I: "H ⊢ OrdP k ⟹ H ⊢ OrdP (SUCC k)"
by (metis OrdP_SUCC_I0 cut1)
lemma Zero_In_OrdP: "{ OrdP x } ⊢ x EQ Zero OR Zero IN x"
proof -
obtain i::name and j::name
where i: "atom i ♯ x" and j: "atom j ♯ (x,i)"
by (metis obtain_fresh)
show ?thesis
apply (rule cut_thin [where HB = "{OrdP x}", OF Foundation [where i=i and z = x]])
using i j apply auto
prefer 2 apply (metis Assume Disj_I1)
apply (rule Disj_I2)
apply (rule cut_same [where A = "Var i EQ Zero"])
prefer 2 apply (blast intro: Iff_MP_same [OF Mem_cong [OF Assume Refl]])
apply (auto intro!: Eq_Zero_I [where i=j] Ex_I [where x="Var i"])
apply (blast intro: Disjoint_E Subset_D)
done
qed
lemma OrdP_HPairE: "insert (OrdP (HPair x y)) H ⊢ A"
proof -
have "{ OrdP (HPair x y) } ⊢ A"
by (rule cut_same [OF Zero_In_OrdP]) (auto simp: HPair_def)
thus ?thesis
by (metis Assume cut1)
qed
lemmas OrdP_HPairEH = OrdP_HPairE OrdP_HPairE [THEN rotate2] OrdP_HPairE [THEN rotate3] OrdP_HPairE [THEN rotate4] OrdP_HPairE [THEN rotate5]
OrdP_HPairE [THEN rotate6] OrdP_HPairE [THEN rotate7] OrdP_HPairE [THEN rotate8] OrdP_HPairE [THEN rotate9] OrdP_HPairE [THEN rotate10]
declare OrdP_HPairEH [intro!]
lemma Zero_Eq_HPairE: "insert (Zero EQ HPair x y) H ⊢ A"
by (metis Eats_EQ_Zero_E2 HPair_def)
lemmas Zero_Eq_HPairEH = Zero_Eq_HPairE Zero_Eq_HPairE [THEN rotate2] Zero_Eq_HPairE [THEN rotate3] Zero_Eq_HPairE [THEN rotate4] Zero_Eq_HPairE [THEN rotate5]
Zero_Eq_HPairE [THEN rotate6] Zero_Eq_HPairE [THEN rotate7] Zero_Eq_HPairE [THEN rotate8] Zero_Eq_HPairE [THEN rotate9] Zero_Eq_HPairE [THEN rotate10]
declare Zero_Eq_HPairEH [intro!]
lemma HPair_Eq_ZeroE: "insert (HPair x y EQ Zero) H ⊢ A"
by (metis Sym_L Zero_Eq_HPairE)
lemmas HPair_Eq_ZeroEH = HPair_Eq_ZeroE HPair_Eq_ZeroE [THEN rotate2] HPair_Eq_ZeroE [THEN rotate3] HPair_Eq_ZeroE [THEN rotate4] HPair_Eq_ZeroE [THEN rotate5]
HPair_Eq_ZeroE [THEN rotate6] HPair_Eq_ZeroE [THEN rotate7] HPair_Eq_ZeroE [THEN rotate8] HPair_Eq_ZeroE [THEN rotate9] HPair_Eq_ZeroE [THEN rotate10]
declare HPair_Eq_ZeroEH [intro!]
section ‹Induction on Ordinals›
lemma OrdInd_lemma:
assumes j: "atom (j::name) ♯ (i,A)"
shows "{ OrdP (Var i) } ⊢ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) IMP A"
proof -
obtain l::name and k::name
where l: "atom l ♯ (i,j,A)" and k: "atom k ♯ (i,j,l,A)"
by (metis obtain_fresh)
have "{ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) }
⊢ (All2 l (Var i) (OrdP (Var l) IMP A(i::= Var l)))"
apply (rule Ind [of k])
using j k l apply auto
apply (rule All_E [where x="Var l", THEN rotate5], auto)
apply (metis Assume Disj_I1 anti_deduction thin1)
apply (rule Ex_I [where x="Var l"], auto)
apply (rule All_E [where x="Var j", THEN rotate6], auto)
apply (blast intro: ContraProve Iff_MP_same [OF Mem_cong [OF Refl]])
apply (metis Assume Ord_IN_Ord0 ContraProve insert_commute)
apply (metis Assume Neg_D thin1)+
done
hence "{ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) }
⊢ (All2 l (Var i) (OrdP (Var l) IMP A(i::= Var l)))(i::= Eats Zero (Var i))"
by (rule Subst, auto)
hence indlem: "{ All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A)) }
⊢ All2 l (Eats Zero (Var i)) (OrdP (Var l) IMP A(i::=Var l))"
using j l by simp
show ?thesis
apply (rule Imp_I)
apply (rule cut_thin [OF indlem, where HB = "{OrdP (Var i)}"])
apply (rule All2_Eats_E) using j l
apply auto
done
qed
lemma OrdInd:
assumes j: "atom (j::name) ♯ (i,A)"
and x: "H ⊢ OrdP (Var i)" and step: "H ⊢ All i (OrdP (Var i) IMP (All2 j (Var i) (A(i::= Var j)) IMP A))"
shows "H ⊢ A"
apply (rule cut_thin [OF x, where HB=H])
apply (rule MP_thin [OF OrdInd_lemma step])
apply (auto simp: j)
done
lemma OrdIndH:
assumes "atom (j::name) ♯ (i,A)"
and "H ⊢ All i (OrdP (Var i) IMP (All2 j (Var i) (A(i::= Var j)) IMP A))"
shows "insert (OrdP (Var i)) H ⊢ A"
by (metis assms thin1 Assume OrdInd)
section ‹Linearity of Ordinals›
lemma OrdP_linear_lemma:
assumes j: "atom j ♯ i"
shows "{ OrdP (Var i) } ⊢ All j (OrdP (Var j) IMP (Var i IN Var j OR Var i EQ Var j OR Var j IN Var i))"
(is "_ ⊢ ?scheme")
proof -
obtain k::name and l::name and m::name
where k: "atom k ♯ (i,j)" and l: "atom l ♯ (i,j,k)" and m: "atom m ♯ (i,j)"
by (metis obtain_fresh)
show ?thesis
proof (rule OrdIndH [where i=i and j=k])
show "atom k ♯ (i, ?scheme)"
using k by (force simp add: fresh_Pair)
next
show "{} ⊢ All i (OrdP (Var i) IMP (All2 k (Var i) (?scheme(i::= Var k)) IMP ?scheme))"
using j k
apply simp
apply (rule All_I Imp_I)+
defer 1
apply auto [2]
apply (rule OrdIndH [where i=j and j=l]) using l
apply (force simp add: fresh_Pair)
apply simp
apply (rule All_I Imp_I)+
prefer 2 apply force
apply (rule Disj_3I)
apply (rule Equality_I)
apply (rule Subset_I [where i=m])
apply (rule All2_E [THEN rotate4]) using l m
apply auto
apply (blast intro: ContraProve [THEN rotate3] OrdP_Trans)
apply (blast intro: ContraProve [THEN rotate3] Mem_cong [OF Hyp Refl, THEN Iff_MP2_same])
apply (rule Subset_I [where i=m])
apply (rule All2_E [THEN rotate6], auto)
apply (rule All_E [where x = "Var j"], auto)
apply (blast intro: ContraProve [THEN rotate4] Mem_cong [OF Hyp Refl, THEN Iff_MP_same])
apply (blast intro: ContraProve [THEN rotate4] OrdP_Trans)
done
qed
qed
lemma OrdP_linear_imp: "{} ⊢ OrdP x IMP OrdP y IMP x IN y OR x EQ y OR y IN x"
proof -
obtain i::name and j::name
where atoms: "atom i ♯ (x,y)" "atom j ♯ (x,y,i)"
by (metis obtain_fresh)
have "{ OrdP (Var i) } ⊢ (OrdP (Var j) IMP (Var i IN Var j OR Var i EQ Var j OR Var j IN Var i))(j::=y)"
using atoms by (metis All_D OrdP_linear_lemma fresh_Pair)
hence "{} ⊢ OrdP (Var i) IMP OrdP y IMP (Var i IN y OR Var i EQ y OR y IN Var i)"
using atoms by auto
hence "{} ⊢ (OrdP (Var i) IMP OrdP y IMP (Var i IN y OR Var i EQ y OR y IN Var i))(i::=x)"
by (metis Subst empty_iff)
thus ?thesis
using atoms by auto
qed
lemma OrdP_linear:
assumes "H ⊢ OrdP x" "H ⊢ OrdP y"
"insert (x IN y) H ⊢ A" "insert (x EQ y) H ⊢ A" "insert (y IN x) H ⊢ A"
shows "H ⊢ A"
proof -
have "{ OrdP x, OrdP y } ⊢ x IN y OR x EQ y OR y IN x"
by (metis OrdP_linear_imp Imp_Imp_commute anti_deduction)
thus ?thesis
using assms by (metis cut2 Disj_E cut_same)
qed
lemma Zero_In_SUCC: "{OrdP k} ⊢ Zero IN SUCC k"
by (rule OrdP_linear [OF OrdP_Zero OrdP_SUCC_I]) (force simp: SUCC_def)+
section ‹The predicate ‹OrdNotEqP››
nominal_function OrdNotEqP :: "tm ⇒ tm ⇒ fm" (infixr "NEQ" 150)
where "OrdNotEqP x y = OrdP x AND OrdP y AND (x IN y OR y IN x)"
by (auto simp: eqvt_def OrdNotEqP_graph_aux_def)
nominal_termination (eqvt)
by lexicographic_order
lemma OrdNotEqP_fresh_iff [simp]: "a ♯ OrdNotEqP x y ⟷ a ♯ x ∧ a ♯ y"
by auto
lemma OrdNotEqP_subst [simp]: "(OrdNotEqP x y)(i::=t) = OrdNotEqP (subst i t x) (subst i t y)"
by simp
lemma OrdNotEqP_cong: "H ⊢ x EQ x' ⟹ H ⊢ y EQ y' ⟹ H ⊢ OrdNotEqP x y IFF OrdNotEqP x' y'"
by (rule P2_cong) auto
lemma OrdNotEqP_self_contra: "{x NEQ x} ⊢ Fls"
by auto
lemma OrdNotEqP_OrdP_E: "insert (OrdP x) (insert (OrdP y) H) ⊢ A ⟹ insert (x NEQ y) H ⊢ A"
by (auto intro: thin1 rotate2)
lemma OrdNotEqP_I: "insert (x EQ y) H ⊢ Fls ⟹ H ⊢ OrdP x ⟹ H ⊢ OrdP y ⟹ H ⊢ x NEQ y"
by (rule OrdP_linear [of _ x y]) (auto intro: ExFalso thin1 Disj_I1 Disj_I2)
declare OrdNotEqP.simps [simp del]
lemma OrdNotEqP_imp_Neg_Eq: "{x NEQ y} ⊢ Neg (x EQ y)"
by (blast intro: OrdNotEqP_cong [THEN Iff_MP2_same] OrdNotEqP_self_contra [of x, THEN cut1])
lemma OrdNotEqP_E: "H ⊢ x EQ y ⟹ insert (x NEQ y) H ⊢ A"
by (metis ContraProve OrdNotEqP_imp_Neg_Eq rcut1)
section ‹Predecessor of an Ordinal›
lemma OrdP_set_max_lemma:
assumes j: "atom (j::name) ♯ i" and k: "atom (k::name) ♯ (i,j)"
shows "{} ⊢ (Neg (Var i EQ Zero) AND (All2 j (Var i) (OrdP (Var j)))) IMP
(Ex j (Var j IN Var i AND (All2 k (Var i) (Var k SUBS Var j))))"
proof -
obtain l::name where l: "atom l ♯ (i,j,k)"
by (metis obtain_fresh)
show ?thesis
apply (rule Ind [of l i]) using j k l
apply simp_all
apply (metis Conj_E Refl Swap Imp_I)
apply (rule All_I Imp_I)+
apply simp_all
apply clarify
apply (rule thin1)
apply (rule thin1 [THEN rotate2])
apply (rule Disj_EH)
apply (rule Neg_Conj_E)
apply (auto simp: All2_Eats_E1)
apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
apply (metis Assume Eq_Zero_D rotate3)
apply (metis Assume EQ_imp_SUBS Neg_D thin1)
apply (rule Cases [where A = "Var j IN Var l"])
apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
apply (rule Ex_I [where x="Var k"], auto)
apply (metis Assume Subset_trans OrdP_Mem_imp_Subset thin1)
apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
apply (metis ContraProve EQ_imp_SUBS rotate3)
apply (rule All2_Eats_E [THEN rotate4], simp_all)
apply (rule Ex_I [where x="Var j"], auto intro: Mem_Eats_I1)
apply (rule All2_E [where x = "Var k", THEN rotate3], auto)
apply (rule Ex_I [where x="Var k"], simp)
apply (metis Assume NegNeg_I Neg_Disj_I rotate3)
apply (rule cut_same [where A = "OrdP (Var j)"])
apply (rule All2_E [where x = "Var j", THEN rotate3], auto)
apply (rule cut_same [where A = "Var l EQ Var j OR Var l IN Var j"])
apply (rule OrdP_linear [of _ "Var l" "Var j"], auto intro: Disj_CI)
apply (metis Assume ContraProve rotate7)
apply (metis ContraProve [THEN rotate4] EQ_imp_SUBS Subset_trans rotate3)
apply (blast intro: ContraProve [THEN rotate4] OrdP_Mem_imp_Subset Iff_MP2_same [OF Mem_cong])
done
qed
lemma OrdP_max_imp:
assumes j: "atom j ♯ (x)" and k: "atom k ♯ (x,j)"
shows "{ OrdP x, Neg (x EQ Zero) } ⊢ Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
proof -
obtain i::name where i: "atom i ♯ (x,j,k)"
by (metis obtain_fresh)
have "{} ⊢ ((Neg (Var i EQ Zero) AND (All2 j (Var i) (OrdP (Var j)))) IMP
(Ex j (Var j IN Var i AND (All2 k (Var i) (Var k SUBS Var j)))))(i::=x)"
apply (rule Subst [OF OrdP_set_max_lemma])
using i k apply auto
done
hence "{ Neg (x EQ Zero) AND (All2 j x (OrdP (Var j))) }
⊢ Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
using i j k by simp (metis anti_deduction)
hence "{ All2 j x (OrdP (Var j)), Neg (x EQ Zero) }
⊢ Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
by (rule cut1) (metis Assume Conj_I thin1)
moreover have "{ OrdP x } ⊢ All2 j x (OrdP (Var j))" using j
by auto (metis Assume Ord_IN_Ord thin1)
ultimately show ?thesis
by (metis rcut1)
qed
declare OrdP.simps [simp del]
section ‹Case Analysis and Zero/SUCC Induction›
lemma OrdP_cases_lemma:
assumes p: "atom p ♯ x"
shows "{ OrdP x, Neg (x EQ Zero) } ⊢ Ex p (OrdP (Var p) AND x EQ SUCC (Var p))"
proof -
obtain j::name and k::name where j: "atom j ♯ (x,p)" and k: "atom k ♯ (x,j,p)"
by (metis obtain_fresh)
show ?thesis
apply (rule cut_same [OF OrdP_max_imp [of j x k]])
using p j k apply auto
apply (rule Ex_I [where x="Var j"], auto)
apply (metis Assume Ord_IN_Ord thin1)
apply (rule cut_same [where A = "OrdP (SUCC (Var j))"])
apply (metis Assume Ord_IN_Ord0 OrdP_SUCC_I rotate2 thin1)
apply (rule OrdP_linear [where x = x, OF _ Assume], auto intro!: Mem_SUCC_EH)
apply (metis Mem_not_sym rotate3)
apply (rule Mem_non_refl, blast intro: Mem_cong [OF Assume Refl, THEN Iff_MP2_same])
apply (force intro: thin1 All2_E [where x = "SUCC (Var j)", THEN rotate4])
done
qed
lemma OrdP_cases_disj:
assumes p: "atom p ♯ x"
shows "insert (OrdP x) H ⊢ x EQ Zero OR Ex p (OrdP (Var p) AND x EQ SUCC (Var p))"
by (metis Disj_CI Assume cut2 [OF OrdP_cases_lemma [OF p]] Swap thin1)
lemma OrdP_cases_E:
"⟦insert (x EQ Zero) H ⊢ A;
insert (x EQ SUCC (Var k)) (insert (OrdP (Var k)) H) ⊢ A;
atom k ♯ (x,A); ∀C ∈ H. atom k ♯ C⟧
⟹ insert (OrdP x) H ⊢ A"
by (rule cut_same [OF OrdP_cases_disj [of k]]) (auto simp: insert_commute intro: thin1)
lemma OrdInd2_lemma:
"{ OrdP (Var i), A(i::= Zero), (All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))) } ⊢ A"
proof -
obtain j::name and k::name where atoms: "atom j ♯ (i,A)" "atom k ♯ (i,j,A)"
by (metis obtain_fresh)
show ?thesis
apply (rule OrdIndH [where i=i and j=j])
using atoms apply auto
apply (rule OrdP_cases_E [where k=k, THEN rotate3])
apply (rule ContraProve [THEN rotate2]) using Var_Eq_imp_subst_Iff
apply (metis Assume AssumeH(3) Iff_MP_same)
apply (rule Ex_I [where x="Var k"], simp)
apply (rule Neg_Imp_I, blast)
apply (rule cut_same [where A = "A(i::=Var k)"])
apply (rule All2_E [where x = "Var k", THEN rotate5])
apply (auto intro: Mem_SUCC_I2 Mem_cong [OF Refl, THEN Iff_MP2_same])
apply (rule ContraProve [THEN rotate5])
by (metis Assume Iff_MP_left' Var_Eq_subst_Iff thin1)
qed
lemma OrdInd2:
assumes "H ⊢ OrdP (Var i)"
and "H ⊢ A(i::= Zero)"
and "H ⊢ All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))"
shows "H ⊢ A"
by (metis cut3 [OF OrdInd2_lemma] assms)
lemma OrdInd2H:
assumes "H ⊢ A(i::= Zero)"
and "H ⊢ All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))"
shows "insert (OrdP (Var i)) H ⊢ A"
by (metis assms thin1 Assume OrdInd2)
section ‹The predicate ‹HFun_Sigma››
text‹To characterise the concept of a function using only bounded universal quantifiers.›
text‹See the note after the proof of Lemma 2.3.›
definition hfun_sigma where
"hfun_sigma r ≡ ∀z ❙∈ r. ∀z' ❙∈ r. ∃x y x' y'. z = ⟨x,y⟩ ∧ z' = ⟨x',y'⟩ ∧ (x=x' ⟶ y=y')"
definition hfun_sigma_ord where
"hfun_sigma_ord r ≡ ∀z ❙∈ r. ∀z' ❙∈ r. ∃x y x' y'. z = ⟨x,y⟩ ∧ z' = ⟨x',y'⟩ ∧ Ord x ∧ Ord x' ∧ (x=x' ⟶ y=y')"
nominal_function HFun_Sigma :: "tm ⇒ fm"
where "⟦atom z ♯ (r,z',x,y,x',y'); atom z' ♯ (r,x,y,x',y');
atom x ♯ (r,y,x',y'); atom y ♯ (r,x',y'); atom x' ♯ (r,y'); atom y' ♯ (r) ⟧ ⟹
HFun_Sigma r =
All2 z r (All2 z' r (Ex x (Ex y (Ex x' (Ex y'
(Var z EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
AND OrdP (Var x) AND OrdP (Var x') AND
((Var x EQ Var x') IMP (Var y EQ Var y'))))))))"
by (auto simp: eqvt_def HFun_Sigma_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows HFun_Sigma_fresh_iff [simp]: "a ♯ HFun_Sigma r ⟷ a ♯ r" (is ?thesis1)
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
where "atom z ♯ (r,z',x,y,x',y')" "atom z' ♯ (r,x,y,x',y')"
"atom x ♯ (r,y,x',y')" "atom y ♯ (r,x',y')"
"atom x' ♯ (r,y')" "atom y' ♯ (r)"
by (metis obtain_fresh)
thus ?thesis1
by (auto simp: HBall_def hfun_sigma_ord_def)
qed
lemma HFun_Sigma_subst [simp]: "(HFun_Sigma r)(i::=t) = HFun_Sigma (subst i t r)"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
where "atom z ♯ (r,t,i,z',x,y,x',y')" "atom z' ♯ (r,t,i,x,y,x',y')"
"atom x ♯ (r,t,i,y,x',y')" "atom y ♯ (r,t,i,x',y')"
"atom x' ♯ (r,t,i,y')" "atom y' ♯ (r,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
qed
lemma HFun_Sigma_Zero: "H ⊢ HFun_Sigma Zero"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
where "atom z'' ♯ (z,z',x,y,x',y')" "atom z ♯ (z',x,y,x',y')" "atom z' ♯ (x,y,x',y')"
"atom x ♯ (y,x',y')" "atom y ♯ (x',y')" "atom x' ♯ y'"
by (metis obtain_fresh)
hence "{} ⊢ HFun_Sigma Zero"
by (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
thus ?thesis
by (metis thin0)
qed
lemma Subset_HFun_Sigma: "{HFun_Sigma s, s' SUBS s} ⊢ HFun_Sigma s'"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
where "atom z'' ♯ (z,z',x,y,x',y',s,s')"
"atom z ♯ (z',x,y,x',y',s,s')" "atom z' ♯ (x,y,x',y',s,s')"
"atom x ♯ (y,x',y',s,s')" "atom y ♯ (x',y',s,s')"
"atom x' ♯ (y',s,s')" "atom y' ♯ (s,s')"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
apply (rule Ex_I [where x="Var z"], auto)
apply (blast intro: Subset_D ContraProve)
apply (rule All_E [where x="Var z'"], auto intro: Subset_D ContraProve)
done
qed
text‹Captures the property of being a relation, using fewer variables than the full definition›
lemma HFun_Sigma_Mem_imp_HPair:
assumes "H ⊢ HFun_Sigma r" "H ⊢ a IN r"
and xy: "atom x ♯ (y,a,r)" "atom y ♯ (a,r)"
shows "H ⊢ (Ex x (Ex y (a EQ HPair (Var x) (Var y))))" (is "_ ⊢ ?concl")
proof -
obtain x'::name and y'::name and z::name and z'::name
where atoms: "atom z ♯ (z',x',y',x,y,a,r)" "atom z' ♯ (x',y',x,y,a,r)"
"atom x' ♯ (y',x,y,a,r)" "atom y' ♯ (x,y,a,r)"
by (metis obtain_fresh)
hence "{HFun_Sigma r, a IN r} ⊢ ?concl" using xy
apply (auto simp: HFun_Sigma.simps [of z r z' x y x' y'])
apply (rule All_E [where x=a], auto)
apply (rule All_E [where x=a], simp)
apply (rule Imp_E, blast)
apply (rule Ex_EH Conj_EH)+
apply simp_all
apply (rule Ex_I [where x="Var x"], simp)
apply (rule Ex_I [where x="Var y"], auto)
done
thus ?thesis
by (rule cut2) (rule assms)+
qed
section ‹The predicate ‹HDomain_Incl››
text ‹This is an internal version of @{term "∀x ❙∈ d. ∃y z. z ❙∈ r ∧ z = ⟨x,y⟩"}.›
nominal_function HDomain_Incl :: "tm ⇒ tm ⇒ fm"
where "⟦atom x ♯ (r,d,y,z); atom y ♯ (r,d,z); atom z ♯ (r,d)⟧ ⟹
HDomain_Incl r d = All2 x d (Ex y (Ex z (Var z IN r AND Var z EQ HPair (Var x) (Var y))))"
by (auto simp: eqvt_def HDomain_Incl_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows HDomain_Incl_fresh_iff [simp]:
"a ♯ HDomain_Incl r d ⟷ a ♯ r ∧ a ♯ d" (is ?thesis1)
proof -
obtain x::name and y::name and z::name
where "atom x ♯ (r,d,y,z)" "atom y ♯ (r,d,z)" "atom z ♯ (r,d)"
by (metis obtain_fresh)
thus ?thesis1
by (auto simp: HDomain_Incl.simps [of x _ _ y z] hdomain_def)
qed
lemma HDomain_Incl_subst [simp]:
"(HDomain_Incl r d)(i::=t) = HDomain_Incl (subst i t r) (subst i t d)"
proof -
obtain x::name and y::name and z::name
where "atom x ♯ (r,d,y,z,t,i)" "atom y ♯ (r,d,z,t,i)" "atom z ♯ (r,d,t,i)"
by (metis obtain_fresh)
thus ?thesis
by (auto simp: HDomain_Incl.simps [of x _ _ y z])
qed
lemma HDomain_Incl_Subset_lemma: "{ HDomain_Incl r k, k' SUBS k } ⊢ HDomain_Incl r k'"
proof -
obtain x::name and y::name and z::name
where "atom x ♯ (r,k,k',y,z)" "atom y ♯ (r,k,k',z)" "atom z ♯ (r,k,k')"
by (metis obtain_fresh)
thus ?thesis
apply (simp add: HDomain_Incl.simps [of x _ _ y z], auto)
apply (rule Ex_I [where x = "Var x"], auto intro: ContraProve Subset_D)
done
qed
lemma HDomain_Incl_Subset: "H ⊢ HDomain_Incl r k ⟹ H ⊢ k' SUBS k ⟹ H ⊢ HDomain_Incl r k'"
by (metis HDomain_Incl_Subset_lemma cut2)
lemma HDomain_Incl_Mem_Ord: "H ⊢ HDomain_Incl r k ⟹ H ⊢ k' IN k ⟹ H ⊢ OrdP k ⟹ H ⊢ HDomain_Incl r k'"
by (metis HDomain_Incl_Subset OrdP_Mem_imp_Subset)
lemma HDomain_Incl_Zero [simp]: "H ⊢ HDomain_Incl r Zero"
proof -
obtain x::name and y::name and z::name
where "atom x ♯ (r,y,z)" "atom y ♯ (r,z)" "atom z ♯ r"
by (metis obtain_fresh)
hence "{} ⊢ HDomain_Incl r Zero"
by (auto simp: HDomain_Incl.simps [of x _ _ y z])
thus ?thesis
by (metis thin0)
qed
lemma HDomain_Incl_Eats: "{ HDomain_Incl r d } ⊢ HDomain_Incl (Eats r (HPair d d')) (SUCC d)"
proof -
obtain x::name and y::name and z::name
where x: "atom x ♯ (r,d,d',y,z)" and y: "atom y ♯ (r,d,d',z)" and z: "atom z ♯ (r,d,d')"
by (metis obtain_fresh)
thus ?thesis
apply (auto simp: HDomain_Incl.simps [of x _ _ y z] intro!: Mem_SUCC_EH)
apply (rule Ex_I [where x = "Var x"], auto)
apply (rule Ex_I [where x = "Var y"], auto)
apply (rule Ex_I [where x = "Var z"], auto intro: Mem_Eats_I1)
apply (rule rotate2 [OF Swap])
apply (rule Ex_I [where x = d'], auto)
apply (rule Ex_I [where x = "HPair d d'"], auto intro: Mem_Eats_I2 HPair_cong Sym)
done
qed
lemma HDomain_Incl_Eats_I: "H ⊢ HDomain_Incl r d ⟹ H ⊢ HDomain_Incl (Eats r (HPair d d')) (SUCC d)"
by (metis HDomain_Incl_Eats cut1)
section ‹@{term HPair} is Provably Injective›
lemma Doubleton_E:
assumes "insert (a EQ c) (insert (b EQ d) H) ⊢ A"
"insert (a EQ d) (insert (b EQ c) H) ⊢ A"
shows "insert ((Eats (Eats Zero b) a) EQ (Eats (Eats Zero d) c)) H ⊢ A"
apply (rule Equality_E) using assms
apply (auto intro!: Zero_SubsetE rotate2 [of "a IN b"])
apply (rule_tac [!] rotate3)
apply (auto intro!: Zero_SubsetE rotate2 [of "a IN b"])
apply (metis Sym_L insert_commute thin1)+
done
lemma HFST: "{HPair a b EQ HPair c d} ⊢ a EQ c"
unfolding HPair_def by (metis Assume Doubleton_E thin1)
lemma b_EQ_d_1: "{a EQ c, a EQ d, b EQ c} ⊢ b EQ d"
by (metis Assume thin1 Sym Trans)
lemma HSND: "{HPair a b EQ HPair c d} ⊢ b EQ d"
unfolding HPair_def
by (metis AssumeH(2) Doubleton_E b_EQ_d_1 rotate3 thin2)
lemma HPair_E [intro!]:
assumes "insert (a EQ c) (insert (b EQ d) H) ⊢ A"
shows "insert (HPair a b EQ HPair c d) H ⊢ A"
by (metis Conj_E [OF assms] Conj_I [OF HFST HSND] rcut1)
declare HPair_E [THEN rotate2, intro!]
declare HPair_E [THEN rotate3, intro!]
declare HPair_E [THEN rotate4, intro!]
declare HPair_E [THEN rotate5, intro!]
declare HPair_E [THEN rotate6, intro!]
declare HPair_E [THEN rotate7, intro!]
declare HPair_E [THEN rotate8, intro!]
lemma HFun_Sigma_E:
assumes r: "H ⊢ HFun_Sigma r"
and b: "H ⊢ HPair a b IN r"
and b': "H ⊢ HPair a b' IN r"
shows "H ⊢ b EQ b'"
proof -
obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
where atoms: "atom z ♯ (r,a,b,b',z',x,y,x',y')" "atom z' ♯ (r,a,b,b',x,y,x',y')"
"atom x ♯ (r,a,b,b',y,x',y')" "atom y ♯ (r,a,b,b',x',y')"
"atom x' ♯ (r,a,b,b',y')" "atom y' ♯ (r,a,b,b')"
by (metis obtain_fresh)
hence d1: "H ⊢ All2 z r (All2 z' r (Ex x (Ex y (Ex x' (Ex y'
(Var z EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y'))))))))"
using r HFun_Sigma.simps [of z r z' x y x' y']
by simp
have d2: "H ⊢ All2 z' r (Ex x (Ex y (Ex x' (Ex y'
(HPair a b EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y')))))))"
using All_D [where x = "HPair a b", OF d1] atoms
by simp (metis MP_same b)
have d4: "H ⊢ Ex x (Ex y (Ex x' (Ex y'
(HPair a b EQ HPair (Var x) (Var y) AND HPair a b' EQ HPair (Var x') (Var y')
AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y'))))))"
using All_D [where x = "HPair a b'", OF d2] atoms
by simp (metis MP_same b')
have d': "{ Ex x (Ex y (Ex x' (Ex y'
(HPair a b EQ HPair (Var x) (Var y) AND HPair a b' EQ HPair (Var x') (Var y')
AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y')))))) } ⊢ b EQ b'"
using atoms
by (auto intro: ContraProve Trans Sym)
thus ?thesis
by (rule cut_thin [OF d4], auto)
qed
section ‹@{term SUCC} is Provably Injective›
lemma SUCC_SUBS_lemma: "{SUCC x SUBS SUCC y} ⊢ x SUBS y"
apply (rule obtain_fresh [where x="(x,y)"])
apply (auto simp: SUCC_def)
prefer 2 apply (metis Assume Conj_E1 Extensionality Iff_MP_same)
apply (auto intro!: Subset_I)
apply (blast intro: Set_MP cut_same [OF Mem_cong [OF Refl Assume, THEN Iff_MP2_same]]
Mem_not_sym thin2)
done
lemma SUCC_SUBS: "insert (SUCC x SUBS SUCC y) H ⊢ x SUBS y"
by (metis Assume SUCC_SUBS_lemma cut1)
lemma SUCC_inject: "insert (SUCC x EQ SUCC y) H ⊢ x EQ y"
by (metis Equality_I EQ_imp_SUBS SUCC_SUBS Sym_L cut1)
lemma SUCC_inject_E [intro!]: "insert (x EQ y) H ⊢ A ⟹ insert (SUCC x EQ SUCC y) H ⊢ A"
by (metis SUCC_inject cut_same insert_commute thin1)
declare SUCC_inject_E [THEN rotate2, intro!]
declare SUCC_inject_E [THEN rotate3, intro!]
declare SUCC_inject_E [THEN rotate4, intro!]
declare SUCC_inject_E [THEN rotate5, intro!]
declare SUCC_inject_E [THEN rotate6, intro!]
declare SUCC_inject_E [THEN rotate7, intro!]
declare SUCC_inject_E [THEN rotate8, intro!]
lemma OrdP_IN_SUCC_lemma: "{OrdP x, y IN x} ⊢ SUCC y IN SUCC x"
apply (rule OrdP_linear [of _ "SUCC x" "SUCC y"])
apply (auto intro!: Mem_SUCC_EH intro: OrdP_SUCC_I Ord_IN_Ord0)
apply (metis Hyp Mem_SUCC_I1 Mem_not_sym cut_same insertCI)
apply (metis Assume EQ_imp_SUBS Mem_SUCC_I1 Mem_non_refl Subset_D thin1)
apply (blast intro: cut_same [OF Mem_cong [THEN Iff_MP2_same]])
done
lemma OrdP_IN_SUCC: "H ⊢ OrdP x ⟹ H ⊢ y IN x ⟹ H ⊢ SUCC y IN SUCC x"
by (rule cut2 [OF OrdP_IN_SUCC_lemma])
lemma OrdP_IN_SUCC_D_lemma: "{OrdP x, SUCC y IN SUCC x} ⊢ y IN x"
apply (rule OrdP_linear [of _ "x" "y"], auto)
apply (metis Assume AssumeH(2) Mem_SUCC_Refl OrdP_SUCC_I Ord_IN_Ord)
apply (rule Mem_SUCC_E [THEN rotate3])
apply (blast intro: Mem_SUCC_Refl OrdP_Trans)
apply (metis AssumeH(2) EQ_imp_SUBS Mem_SUCC_I1 Mem_non_refl Subset_D)
apply (metis EQ_imp_SUBS Mem_SUCC_I2 Mem_SUCC_EH(2) Mem_SUCC_I1 Refl SUCC_Subset_Ord_lemma Subset_D thin1)
done
lemma OrdP_IN_SUCC_D: "H ⊢ OrdP x ⟹ H ⊢ SUCC y IN SUCC x ⟹ H ⊢ y IN x"
by (rule cut2 [OF OrdP_IN_SUCC_D_lemma])
lemma OrdP_IN_SUCC_Iff: "H ⊢ OrdP y ⟹ H ⊢ SUCC x IN SUCC y IFF x IN y"
by (metis Assume Iff_I OrdP_IN_SUCC OrdP_IN_SUCC_D thin1)
section ‹The predicate ‹LstSeqP››
lemma hfun_sigma_ord_iff: "hfun_sigma_ord s ⟷ OrdDom s ∧ hfun_sigma s"
by (auto simp: hfun_sigma_ord_def OrdDom_def hfun_sigma_def HBall_def, metis+)
lemma hfun_sigma_iff: "hfun_sigma r ⟷ hfunction r ∧ hrelation r"
by (auto simp add: HBall_def hfun_sigma_def hfunction_def hrelation_def is_hpair_def, metis+)
lemma Seq_iff: "Seq r d ⟷ d ≤ hdomain r ∧ hfun_sigma r"
by (auto simp: Seq_def hfun_sigma_iff)
lemma LstSeq_iff: "LstSeq s k y ⟷ succ k ≤ hdomain s ∧ ⟨k,y⟩ ❙∈ s ∧ hfun_sigma_ord s"
by (auto simp: OrdDom_def LstSeq_def Seq_iff hfun_sigma_ord_iff)
nominal_function LstSeqP :: "tm ⇒ tm ⇒ tm ⇒ fm"
where
"LstSeqP s k y = OrdP k AND HDomain_Incl s (SUCC k) AND HFun_Sigma s AND HPair k y IN s"
by (auto simp: eqvt_def LstSeqP_graph_aux_def)
nominal_termination (eqvt)
by lexicographic_order
lemma
shows LstSeqP_fresh_iff [simp]:
"a ♯ LstSeqP s k y ⟷ a ♯ s ∧ a ♯ k ∧ a ♯ y" (is ?thesis1)
proof -
show ?thesis1
by (auto simp: LstSeq_iff OrdDom_def hfun_sigma_ord_iff)
qed
lemma LstSeqP_subst [simp]:
"(LstSeqP s k y)(i::=t) = LstSeqP (subst i t s) (subst i t k) (subst i t y)"
by (auto simp: fresh_Pair fresh_at_base)
lemma LstSeqP_E:
assumes "insert (HDomain_Incl s (SUCC k))
(insert (OrdP k) (insert (HFun_Sigma s)
(insert (HPair k y IN s) H))) ⊢ B"
shows "insert (LstSeqP s k y) H ⊢ B"
using assms by (auto simp: insert_commute)
declare LstSeqP.simps [simp del]
lemma LstSeqP_cong:
assumes "H ⊢ s EQ s'" "H ⊢ k EQ k'" "H ⊢ y EQ y'"
shows "H ⊢ LstSeqP s k y IFF LstSeqP s' k' y'"
by (rule P3_cong [OF _ assms], auto)
lemma LstSeqP_OrdP: "H ⊢ LstSeqP r k y ⟹ H ⊢ OrdP k"
by (metis Conj_E1 LstSeqP.simps)
lemma LstSeqP_Mem_lemma: "{ LstSeqP r k y, HPair k' z IN r, k' IN k } ⊢ LstSeqP r k' z"
by (auto simp: LstSeqP.simps intro: Ord_IN_Ord OrdP_SUCC_I OrdP_IN_SUCC HDomain_Incl_Mem_Ord)
lemma LstSeqP_Mem: "H ⊢ LstSeqP r k y ⟹ H ⊢ HPair k' z IN r ⟹ H ⊢ k' IN k ⟹ H ⊢ LstSeqP r k' z"
by (rule cut3 [OF LstSeqP_Mem_lemma])
lemma LstSeqP_imp_Mem: "H ⊢ LstSeqP s k y ⟹ H ⊢ HPair k y IN s"
by (auto simp: LstSeqP.simps) (metis Conj_E2)
lemma LstSeqP_SUCC: "H ⊢ LstSeqP r (SUCC d) y ⟹ H ⊢ HPair d z IN r ⟹ H ⊢ LstSeqP r d z"
by (metis LstSeqP_Mem Mem_SUCC_I2 Refl)
lemma LstSeqP_EQ: "⟦H ⊢ LstSeqP s k y; H ⊢ HPair k y' IN s⟧ ⟹ H ⊢ y EQ y'"
by (metis AssumeH(2) HFun_Sigma_E LstSeqP_E cut1 insert_commute)
end