Skip to content

Commit b5dfc41

Browse files
jvanbrueggejvanbruegge
committed
Define and prove normal substitution
1 parent 4c38220 commit b5dfc41

File tree

2 files changed

+134
-49
lines changed

2 files changed

+134
-49
lines changed

‎Defs.thy‎

Lines changed: 131 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -2,78 +2,162 @@ theory Defs
22
imports Main "Nominal2.Nominal2" "HOL-Eisbach.Eisbach"
33
begin
44

5-
atom_decl "name"
5+
atom_decl "var"
6+
atom_decl "tyvar"
7+
68
nominal_datatype "\<tau>" =
79
TyUnit
8-
| TyArrow "\<tau>" "\<tau>" ("_ \<rightarrow> _" 50)
10+
| TyVar "tyvar"
11+
| TyArrow "\<tau>" "\<tau>" ("_ \<rightarrow> _" 50)
12+
| TyForall a::"tyvar" t::"\<tau>" binds a in t ("\<forall> _ . _" 50)
913

1014
nominal_datatype "term" =
11-
Var "name"
12-
| Lam x::"name" "\<tau>" e::"term" binds x in e ("\<lambda> _ : _ . _" 50)
15+
Var "var"
16+
| Lam x::"var" "\<tau>" e::"term" binds x in e ("\<lambda> _ : _ . _" 50)
17+
| TyLam a::"tyvar" e::"term" binds a in e ("\<Lambda> _ . _" 50)
1318
| App "term" "term"
1419
| Unit
15-
| Let x::"name" "term" e2::"term" binds x in e2
20+
| Let x::"var" "term" e2::"term" binds x in e2
1621

17-
type_synonym "\<Gamma>" = "(name * \<tau>) list"
22+
type_synonym "\<Gamma>" = "(var * \<tau>) list"
1823

1924
declare term.fv_defs[simp]
2025

21-
lemma no_vars_in_ty[simp]: "atom x \<sharp> (ty :: \<tau>)"
26+
lemma no_vars_in_ty[simp]: "atom (x :: var) \<sharp> (ty :: \<tau>)"
2227
by (induction ty rule: \<tau>.induct) auto
2328

24-
nominal_function isin :: "name * \<tau> \<Rightarrow> \<Gamma> \<Rightarrow> bool" (infixr "\<in>" 80) where
29+
(*nominal_function isin :: "var * \<tau> \<Rightarrow> \<Gamma> \<Rightarrow> bool" (infixr "\<in>" 80) where
2530
"isin _ [] = False"
2631
| "isin (x, t) ((y, t')#xs) = (if x = y then t = t' else isin (x, t) xs)"
2732
apply (all_trivials)
2833
apply (simp add: eqvt_def isin_graph_aux_def)
2934
apply (metis list.exhaust old.prod.exhaust)
3035
apply simp
3136
done
32-
nominal_termination (eqvt) by lexicographic_order
37+
nominal_termination (eqvt) by lexicographic_order*)
3338

3439
(** subrules *)
3540
nominal_function
36-
is_v_of_e :: "term => bool"
41+
is_value :: "term => bool"
3742
where
38-
"is_v_of_e (Var x) = (False)"
39-
| "is_v_of_e (\<lambda> x : \<tau> . e) = ((True))"
40-
| "is_v_of_e (App e1 e2) = (False)"
41-
| "is_v_of_e Unit = ((True))"
42-
| "is_v_of_e (Let x e1 e2) = (False)"
43-
apply (all_trivials)
44-
apply (simp add: eqvt_def is_v_of_e_graph_aux_def)
43+
"is_value (Var x) = False"
44+
| "is_value (\<lambda> x : \<tau> . e) = True"
45+
| "is_value (\<Lambda> a . e) = True"
46+
| "is_value (App e1 e2) = False"
47+
| "is_value Unit = True"
48+
| "is_value (Let x e1 e2) = False"
49+
apply (auto simp: eqvt_def is_value_graph_aux_def)
4550
using term.exhaust by blast
46-
nominal_termination (eqvt)
47-
by lexicographic_order
48-
49-
method pat_comp_aux =
50-
(match premises in
51-
"x = (_ :: term) \<Longrightarrow> _" for x \<Rightarrow> \<open>rule term.strong_exhaust [where y = x and c = x]\<close>
52-
\<bar> "x = (Var _, _) \<Longrightarrow> _" for x :: "_ :: fs" \<Rightarrow>
53-
\<open>rule term.strong_exhaust [where y = "fst x" and c = x]\<close>
54-
\<bar> "x = (_, Var _) \<Longrightarrow> _" for x :: "_ :: fs" \<Rightarrow>
55-
\<open>rule term.strong_exhaust [where y = "snd x" and c = x]\<close>
56-
\<bar> "x = (_, _, Var _) \<Longrightarrow> _" for x :: "_ :: fs" \<Rightarrow>
57-
\<open>rule term.strong_exhaust [where y = "snd (snd x)" and c = x]\<close>)
51+
nominal_termination (eqvt) by lexicographic_order
52+
53+
lemma Abs_lst_rename: "\<lbrakk> atom c \<sharp> e ; sort_of (atom c) = sort_of (atom a) \<rbrakk> \<Longrightarrow> [[atom a]]lst. e = [[atom c]]lst. (a \<leftrightarrow> c) \<bullet> e"
54+
proof -
55+
assume a: "atom c \<sharp> e" and a2: "sort_of (atom c) = sort_of (atom a)"
56+
then have 1: "atom c \<notin> supp e - set [atom a]" by (simp add: fresh_def)
57+
have 2: "atom a \<notin> supp e - set [atom a]" by simp
58+
show ?thesis using Abs_swap2[OF 2 1] by (simp add: a2 flip_def)
59+
qed
60+
61+
lemma Abs_lst_rename_both:
62+
"\<lbrakk> atom c \<sharp> (y, e::'e::fs, y', e'::'e::fs) ; sort_of (atom c) = sort_of (atom y) ; sort_of (atom c) = sort_of (atom y') ; ([[atom y]]lst. e) = ([[atom y']]lst. e') \<rbrakk> \<Longrightarrow>
63+
(y \<leftrightarrow> c) \<bullet> e = (y' \<leftrightarrow> c) \<bullet> e'"
64+
proof -
65+
assume a: "atom c \<sharp> (y, e, y', e')" "sort_of (atom c) = sort_of (atom y)" "sort_of (atom c) = sort_of (atom y')" "([[atom y]]lst. e) = ([[atom y']]lst. e')"
66+
then have "(y \<leftrightarrow> c) \<bullet> ([[atom y]]lst. e) = (y' \<leftrightarrow> c) \<bullet> ([[atom y']]lst. e')"
67+
by (smt Abs_lst_rename Cons_eqvt Nil_eqvt flip_def fresh_PairD(1) fresh_PairD(2) permute_Abs_lst swap_atom_simps(1))
68+
then have "([[atom c]]lst. (y \<leftrightarrow> c) \<bullet> e) = ([[atom c]]lst. (y' \<leftrightarrow> c) \<bullet> e')" using Abs_lst_rename a(2) a(3) by auto
69+
then show ?thesis using Abs1_eq(3) by blast
70+
qed
71+
72+
lemma eqvt_at_deep: "\<lbrakk> atom a \<sharp> (x, e) ; atom c \<sharp> (x, e) ; eqvt_at f (e, x, e2) \<rbrakk> \<Longrightarrow> (a \<leftrightarrow> c) \<bullet> f (e, x, e2) = f (e, x, (a \<leftrightarrow> c) \<bullet> e2)"
73+
proof -
74+
assume a: "atom a \<sharp> (x, e)" "atom c \<sharp> (x, e)" "eqvt_at f (e, x, e2)"
75+
76+
have 1: "(a \<leftrightarrow> c) \<bullet> f (e, x, e2) = f ((a \<leftrightarrow> c) \<bullet> (e, x, e2))" using a(3) eqvt_at_def by blast
77+
have 2: "(a \<leftrightarrow> c) \<bullet> (e, x, e2) = (e, x, (a \<leftrightarrow> c) \<bullet> e2)" using a(1) a(2) fresh_Pair flip_fresh_fresh by fastforce
78+
79+
show ?thesis using 1 2 by argo
80+
qed
81+
82+
lemma Abs_lst_rename_deep: "\<lbrakk> atom c \<sharp> (f (e, x, e2), x, e) ; atom a \<sharp> (x, e) ; sort_of (atom c) = sort_of (atom a) ; eqvt_at f (e, x, e2) \<rbrakk> \<Longrightarrow> [[atom a]]lst. f (e, x, e2) = [[atom c]]lst. f (e, x, (a \<leftrightarrow> c) \<bullet> e2)"
83+
proof -
84+
assume a: "atom c \<sharp> (f (e, x, e2), x, e)" "atom a \<sharp> (x, e)" "sort_of (atom c) = sort_of (atom a)" "eqvt_at f (e, x, e2)"
85+
86+
have 1: "[[atom a]]lst. f (e, x, e2) = [[atom c]]lst. (a \<leftrightarrow> c) \<bullet> f (e, x, e2)" using Abs_lst_rename[OF _ a(3)] a(1) fresh_Pair by blast
87+
have 2: "(a \<leftrightarrow> c) \<bullet> f (e, x, e2) = f (e, x, (a \<leftrightarrow> c) \<bullet> e2)" using eqvt_at_deep[OF a(2) _ a(4)] a(1) fresh_Pair by blast
88+
89+
show ?thesis using 1 2 by argo
90+
qed
5891

5992
(** substitutions *)
6093
nominal_function
61-
subst_term :: "term => name => term => term"
94+
subst_term :: "term => var => term => term"
6295
where
63-
"subst_term e_5 x5 (Var x) = ((if x=x5 then e_5 else (Var x)))"
64-
| "atom x \<sharp> (x5, e_5) \<Longrightarrow> subst_term e_5 x5 (\<lambda> x : \<tau> . e) = (Lam x \<tau> (subst_term e_5 x5 e))"
65-
| "subst_term e_5 x5 (App e1 e2) = (App (subst_term e_5 x5 e1) (subst_term e_5 x5 e2))"
66-
| "subst_term e_5 x5 Unit = (Unit )"
67-
| "atom x \<sharp> (x5, e_5) \<Longrightarrow> subst_term e_5 x5 (Let x e1 e2) = (Let x (subst_term e_5 x5 e1) (subst_term e_5 x5 e2))"
68-
apply (all_trivials)
69-
apply (simp add: eqvt_def subst_term_graph_aux_def)
70-
apply(pat_comp_aux)
71-
apply(auto simp: fresh_star_def fresh_Pair)
72-
apply blast
73-
apply blast
74-
apply (auto simp: eqvt_at_def)
75-
apply (metis flip_fresh_fresh)+
76-
done
96+
"subst_term e x (Var y) = (if x=y then e else Var y)"
97+
| "atom y \<sharp> (x, e) \<Longrightarrow> subst_term e x (\<lambda> y : \<tau> . e2) = (Lam y \<tau> (subst_term e x e2))"
98+
| "atom y \<sharp> (x, e) \<Longrightarrow> subst_term e x (\<Lambda> y . e2) = (\<Lambda> y . subst_term e x e2)"
99+
| "subst_term e x (App e1 e2) = (App (subst_term e x e1) (subst_term e x e2))"
100+
| "subst_term _ _ Unit = Unit"
101+
| "atom y \<sharp> (x, e) \<Longrightarrow> subst_term e x (Let y e1 e2) = (Let y (subst_term e x e1) (subst_term e x e2))"
102+
proof goal_cases
103+
case (3 P x)
104+
then obtain e y t where P: "x = (e, y, t)" by (metis prod.exhaust)
105+
then show ?case
106+
apply (cases t rule: term.strong_exhaust[of _ _ "(y, e)"])
107+
apply (auto simp: 3)
108+
using 3(2) 3(3) 3(6) P fresh_star_def by blast+
109+
next
110+
case (10 y x e \<tau> e2 y' x' e' \<tau>' e2')
111+
112+
obtain c::var where "atom c \<sharp> (y, y', e, x, e', x', e2, e2', subst_term_sumC (e, x, e2), subst_term_sumC (e', x', e2'))" using obtain_fresh by blast
113+
then have c: "atom c \<sharp> (subst_term_sumC (e, x, e2), x, e)" "atom c \<sharp> (subst_term_sumC (e', x', e2'), x', e')" "atom c \<sharp> (y, e2, y', e2')" using fresh_Pair by fastforce+
114+
115+
have sort_same_y: "sort_of (atom c) = sort_of (atom y)" by simp
116+
have sort_same_y': "sort_of (atom c) = sort_of (atom y')" by simp
117+
118+
have 1: "(\<lambda> y : \<tau> . subst_term_sumC (e, x, e2)) = (\<lambda> c : \<tau> . subst_term_sumC (e, x, (y \<leftrightarrow> c) \<bullet> e2))"
119+
using Abs_lst_rename_deep[OF c(1) 10(5) sort_same_y 10(1)] term.eq_iff(2) by blast
120+
have 2: "(\<lambda> y' : \<tau>' . subst_term_sumC (e', x', e2')) = (\<lambda> c : \<tau> . subst_term_sumC (e, x, (y' \<leftrightarrow> c) \<bullet> e2'))"
121+
using Abs_lst_rename_deep[OF c(2) 10(6) sort_same_y' 10(2)] term.eq_iff(2) 10(7) by auto
122+
have 3: "(y \<leftrightarrow> c) \<bullet> e2 = (y' \<leftrightarrow> c) \<bullet> e2'" using Abs_lst_rename_both[OF c(3) sort_same_y sort_same_y'] 10(7) by force
123+
124+
show ?case using 1 2 3 by argo
125+
next
126+
case (15 y x e e2 y' x' e' e2')
127+
128+
obtain c::tyvar where "atom c \<sharp> (y, y', e, x, e', x', e2, e2', subst_term_sumC (e, x, e2), subst_term_sumC (e', x', e2'))" using obtain_fresh by blast
129+
then have c: "atom c \<sharp> (subst_term_sumC (e, x, e2), x, e)" "atom c \<sharp> (subst_term_sumC (e', x', e2'), x', e')" "atom c \<sharp> (y, e2, y', e2')" using fresh_Pair by fastforce+
130+
131+
have sort_same_y: "sort_of (atom c) = sort_of (atom y)" by simp
132+
have sort_same_y': "sort_of (atom c) = sort_of (atom y')" by simp
133+
134+
have 1: "(\<Lambda> y . subst_term_sumC (e, x, e2)) = (\<Lambda> c . subst_term_sumC (e, x, (y \<leftrightarrow> c) \<bullet> e2))"
135+
using Abs_lst_rename_deep[OF c(1) 15(5) sort_same_y 15(1)] term.eq_iff(3) by presburger
136+
have 2: "(\<Lambda> y' . subst_term_sumC (e', x', e2')) = (\<Lambda> c . subst_term_sumC (e, x, (y' \<leftrightarrow> c) \<bullet> e2'))"
137+
using Abs_lst_rename_deep[OF c(2) 15(6) sort_same_y' 15(2)] term.eq_iff(3) 15(7) by auto
138+
have 3: "(y \<leftrightarrow> c) \<bullet> e2 = (y' \<leftrightarrow> c) \<bullet> e2'" using Abs_lst_rename_both[OF c(3) sort_same_y sort_same_y'] 15(7) by force
139+
140+
show ?case using 1 2 3 by argo
141+
next
142+
case (24 y x e e1 e2 y' x' e' e1' e2')
143+
144+
obtain c::var where "atom c \<sharp> (y, y', e, x, e', x', e2, e2', subst_term_sumC (e, x, e2), subst_term_sumC (e', x', e2'))" using obtain_fresh by blast
145+
then have c: "atom c \<sharp> (subst_term_sumC (e, x, e2), x, e)" "atom c \<sharp> (subst_term_sumC (e', x', e2'), x', e')" "atom c \<sharp> (y, e2, y', e2')" using fresh_Pair by fastforce+
146+
147+
have sort_same_y: "sort_of (atom c) = sort_of (atom y)" by simp
148+
have sort_same_y': "sort_of (atom c) = sort_of (atom y')" by simp
149+
150+
let ?e1 = "subst_term_sumC (e, x, e1)"
151+
let ?e1' = "subst_term_sumC (e', x', e1')"
152+
have 0: "?e1 = ?e1'" using 24 by simp
153+
have 1: "Let y ?e1 (subst_term_sumC (e, x, e2)) = Let c ?e1 (subst_term_sumC (e, x, (y \<leftrightarrow> c) \<bullet> e2))"
154+
using Abs_lst_rename_deep[OF c(1) 24(9) sort_same_y 24(2)] 0 term.eq_iff(6) by blast
155+
have 2: "Let y' ?e1' (subst_term_sumC (e', x', e2')) = Let c ?e1 (subst_term_sumC (e, x, (y' \<leftrightarrow> c) \<bullet> e2'))"
156+
using Abs_lst_rename_deep[OF c(2) 24(10) sort_same_y' 24(4)] 0 term.eq_iff(6) 24(11) by auto
157+
have 3: "(y \<leftrightarrow> c) \<bullet> e2 = (y' \<leftrightarrow> c) \<bullet> e2'" using Abs_lst_rename_both[OF c(3) sort_same_y sort_same_y'] 24(11) by force
158+
159+
show ?case using 1 2 3 by argo
160+
qed (auto simp: eqvt_def subst_term_graph_aux_def)
77161
nominal_termination (eqvt) by lexicographic_order
78162

79163
lemma fresh_subst_term: "\<lbrakk> atom z \<sharp> s ; z = y \<or> atom z \<sharp> t \<rbrakk> \<Longrightarrow> atom z \<sharp> subst_term s y t"
@@ -122,17 +206,17 @@ where
122206

123207
| (* defn Step *)
124208

125-
ST_BetaI: "\<lbrakk>is_v_of_e v\<rbrakk> \<Longrightarrow>
209+
ST_BetaI: "\<lbrakk>is_value v\<rbrakk> \<Longrightarrow>
126210
((App (\<lambda> x : \<tau> . e) v) \<longrightarrow> subst_term v x e )"
127211

128212
| ST_AppI: "\<lbrakk>(e1 \<longrightarrow> e2)\<rbrakk> \<Longrightarrow>
129213
((App e1 e) \<longrightarrow> (App e2 e))"
130214

131-
| ST_App2I: "\<lbrakk>is_v_of_e v ;
215+
| ST_App2I: "\<lbrakk>is_value v ;
132216
(e1 \<longrightarrow> e2)\<rbrakk> \<Longrightarrow>
133217
((App v e1) \<longrightarrow> (App v e2))"
134218

135-
| ST_SubstI: "\<lbrakk>is_v_of_e v\<rbrakk> \<Longrightarrow>
219+
| ST_SubstI: "\<lbrakk>is_value v\<rbrakk> \<Longrightarrow>
136220
((Let x v e) \<longrightarrow> subst_term v x e )"
137221

138222
| ST_LetI: "\<lbrakk>(e1 \<longrightarrow> e2)\<rbrakk> \<Longrightarrow>

‎Soundness.thy‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ proof (nominal_induct e avoiding: \<Gamma> \<tau> v x \<tau>' rule: term.strong_
171171
next
172172
case False
173173
then show ?thesis using Var context_invariance
174-
by (metis (no_types, lifting) Rep_name_inverse atom_name_def subst_term.simps(1) isin.simps(2) singletonD supp_at_base term.fv_defs(1))
174+
by (metis (no_types, lifting) Rep_var_inverse atom_var_def subst_term.simps(1) isin.simps(2) singletonD supp_at_base term.fv_defs(1))
175175
qed
176176
next
177177
case (Lam y \<sigma> e)
@@ -286,7 +286,8 @@ lemma beta_same[simp]: "\<lbrakk> e1 \<longrightarrow>* e1' ; beta_nf e1 \<rbrak
286286
lemma subst_term_perm: "atom x' \<sharp> (x, e) \<Longrightarrow> subst_term v x e = subst_term v x' ((x \<leftrightarrow> x') \<bullet> e)"
287287
apply (nominal_induct e avoiding: x x' v rule: term.strong_induct)
288288
apply (auto simp: fresh_Pair fresh_at_base(2) flip_fresh_fresh)
289-
by (smt flip_at_base_simps(3) flip_commute flip_eqvt flip_fresh_fresh minus_flip permute_eqvt permute_eqvt subst_term.eqvt uminus_eqvt)
289+
by (smt flip_at_base_simps(3) flip_at_simps(2) flip_eqvt flip_fresh_fresh minus_flip permute_eqvt permute_eqvt subst_term.eqvt)
290+
290291

291292
lemma step_deterministic: "\<lbrakk> Step e e1 ; Step e e2 \<rbrakk> \<Longrightarrow> e1 = e2"
292293
proof (induction e e1 arbitrary: e2 rule: Step.induct)

0 commit comments

Comments
 (0)