Skip to content

Commit 96a3924

Browse files
jvanbrueggejvanbruegge
committed
Refactor and split Defs.thy
1 parent f42a973 commit 96a3924

File tree

6 files changed

+289
-418
lines changed

6 files changed

+289
-418
lines changed

‎Defs.thy‎

Lines changed: 16 additions & 418 deletions
Large diffs are not rendered by default.

‎Lemmas.thy‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
theory Lemmas
2+
imports Syntax Defs
3+
begin
4+
5+
(* atom x \<sharp> t' \<Longrightarrow> atom x \<sharp> subst t' x t *)
6+
lemma fresh_after_subst_term: "atom x \<sharp> e' \<Longrightarrow> atom x \<sharp> subst_term e' x e"
7+
by (nominal_induct e avoiding: x e' rule: term.strong_induct) auto
8+
lemma fresh_after_subst_type: "atom a \<sharp> \<tau> \<Longrightarrow> atom a \<sharp> subst_type \<tau> a \<sigma>"
9+
by (nominal_induct \<sigma> avoiding: a \<tau> rule: \<tau>.strong_induct) auto
10+
lemma fresh_after_subst_term_type: "atom a \<sharp> \<tau> \<Longrightarrow> atom a \<sharp> subst_term_type \<tau> a e"
11+
by (nominal_induct e avoiding: a \<tau> rule: term.strong_induct) (auto simp: fresh_after_subst_type)
12+
13+
(* atom c \<sharp> t \<Longrightarrow> subst t' x t = subst t' c ((x \<leftrightarrow> c) \<bullet> t) *)
14+
lemma subst_term_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term e' x e = subst_term e' c ((x \<leftrightarrow> c) \<bullet> e)"
15+
proof (nominal_induct e avoiding: c x e' rule: term.strong_induct)
16+
case (Let y \<tau> e1 e2)
17+
then show ?case by (smt flip_fresh_fresh fresh_Pair fresh_at_base(2) list.set(1) list.set(2) no_vars_in_ty singletonD subst_term.simps(7) term.fresh(7) term.perm_simps(7))
18+
qed (auto simp: flip_fresh_fresh fresh_at_base)
19+
lemma subst_type_var_name: "atom c \<sharp> \<sigma> \<Longrightarrow> subst_type \<tau> a \<sigma> = subst_type \<tau> c ((a \<leftrightarrow> c) \<bullet> \<sigma>)"
20+
by (nominal_induct \<sigma> avoiding: c a \<tau> rule: \<tau>.strong_induct) (auto simp: fresh_at_base)
21+
lemma subst_term_type_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term_type \<tau> a e = subst_term_type \<tau> c ((a \<leftrightarrow> c) \<bullet> e)"
22+
proof (nominal_induct e avoiding: c a \<tau> rule: term.strong_induct)
23+
case (Lam x \<tau>1 e)
24+
then show ?case
25+
by (smt flip_fresh_fresh fresh_Pair fresh_at_base(2) list.set(1) list.set(2) singletonD subst_term_type.simps(3) subst_type_var_name term.fresh(5) term.perm_simps(5))
26+
next
27+
case (Let x \<tau>1 e1 e2)
28+
then show ?case
29+
by (smt flip_def fresh_Pair fresh_at_base(2) list.set(1) list.set(2) singletonD subst_term_type.simps(7) subst_type_var_name swap_fresh_fresh term.fresh(7) term.perm_simps(7))
30+
qed (auto simp: flip_fresh_fresh fresh_at_base subst_type_var_name)
31+
32+
(* [[atom a]]lst. t = [[atom a2]]lst. t2 \<Longrightarrow> subst t' a t = subst t' a2 t2 *)
33+
lemma subst_term_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term t a e = subst_term t a' e'"
34+
by (metis Abs1_eq_iff(3) flip_commute subst_term_var_name)
35+
lemma subst_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_type \<tau> a e = subst_type \<tau> a' e'"
36+
by (metis Abs1_eq_iff(3) flip_commute subst_type_var_name)
37+
lemma subst_term_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term_type \<tau> a e = subst_term_type \<tau> a' e'"
38+
by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name)
39+
40+
(* atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (B x _) \<Gamma> *)
41+
lemma fresh_not_isin_tyvar: "atom a \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BTyVar a) \<Gamma>"
42+
apply (induction \<Gamma>) apply simp
43+
by (metis binder.fresh(2) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(4) isin.simps(5))
44+
lemma fresh_not_isin_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BVar x \<tau>) \<Gamma>"
45+
apply (induction \<Gamma>) apply simp
46+
by (metis (mono_tags, lifting) binder.fresh(1) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(2) isin.simps(3))
47+
48+
end

‎Nominal2_Lemmas.thy‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
theory Nominal2_Lemmas
2+
imports Main "Nominal2.Nominal2"
3+
begin
4+
5+
lemma Abs_lst_rename:
6+
fixes a c::"'a::at" and e::"'e::fs"
7+
assumes "atom c \<sharp> e"
8+
shows "[[atom a]]lst. e = [[atom c]]lst. (a \<leftrightarrow> c) \<bullet> e"
9+
proof -
10+
from assms have 1: "atom c \<notin> supp e - set [atom a]" by (simp add: fresh_def)
11+
have 2: "atom a \<notin> supp e - set [atom a]" by simp
12+
show ?thesis using Abs_swap2[OF 2 1] by (simp add: flip_def)
13+
qed
14+
15+
lemma eqvt_at_deep:
16+
assumes fresh: "atom a \<sharp> (x, e)" "atom c \<sharp> (x, e)"
17+
and eqvt_at: "eqvt_at f (x, e, e2)"
18+
shows "(a \<leftrightarrow> c) \<bullet> f (x, e, e2) = f (x, e, (a \<leftrightarrow> c) \<bullet> e2)"
19+
proof -
20+
have 1: "(a \<leftrightarrow> c) \<bullet> f (x, e, e2) = f ((a \<leftrightarrow> c) \<bullet> (x, e, e2))" using eqvt_at eqvt_at_def by blast
21+
have 2: "(a \<leftrightarrow> c) \<bullet> (x, e, e2) = (x, e, (a \<leftrightarrow> c) \<bullet> e2)" using fresh fresh_Pair flip_fresh_fresh by fastforce
22+
23+
show ?thesis using 1 2 by argo
24+
qed
25+
26+
lemma Abs_lst_rename_deep:
27+
fixes a c::"'a::at" and x::"'b::fs" and e::"'c::fs" and e2::"'d::fs" and f::"'b * 'c * 'd \<Rightarrow> 'e::fs"
28+
assumes fresh: "atom c \<sharp> f (x, e, e2)" "atom c \<sharp> (x, e)" "atom a \<sharp> (x, e)"
29+
and eqvt_at: "eqvt_at f (x, e, e2)"
30+
shows "[[atom a]]lst. f (x, e, e2) = [[atom c]]lst. f (x, e, (a \<leftrightarrow> c) \<bullet> e2)"
31+
proof -
32+
have 1: "[[atom a]]lst. f (x, e, e2) = [[atom c]]lst. (a \<leftrightarrow> c) \<bullet> f (x, e, e2)" by (rule Abs_lst_rename[OF fresh(1)])
33+
have 2: "(a \<leftrightarrow> c) \<bullet> f (x, e, e2) = f (x, e, (a \<leftrightarrow> c) \<bullet> e2)" by (rule eqvt_at_deep[OF fresh(3) fresh(2) eqvt_at])
34+
show ?thesis using 1 2 by argo
35+
qed
36+
37+
lemma Abs_lst_rename_both:
38+
fixes a c::"'a::at" and e e'::"'b::fs"
39+
assumes fresh: "atom c \<sharp> (y, e, y', e')"
40+
and equal: "[[atom y]]lst. e = [[atom y']]lst. e'"
41+
shows "(y \<leftrightarrow> c) \<bullet> e = (y' \<leftrightarrow> c) \<bullet> e'"
42+
proof -
43+
from assms have "(y \<leftrightarrow> c) \<bullet> ([[atom y]]lst. e) = (y' \<leftrightarrow> c) \<bullet> ([[atom y']]lst. e')" by auto
44+
then have "[[atom c]]lst. (y \<leftrightarrow> c) \<bullet> e = [[atom c]]lst. (y' \<leftrightarrow> c) \<bullet> e'" by auto
45+
then show ?thesis using Abs1_eq(3) by blast
46+
qed
47+
48+
lemma Abs_sumC:
49+
fixes y y'::"'a::at" and x x'::"'b::fs" and e e'::"'c::fs" and e2 e2'::"'d::fs" and f::"'b * 'c * 'd \<Rightarrow> 'e::fs"
50+
assumes fresh: "atom y \<sharp> (x, e)" "atom y' \<sharp> (x', e')"
51+
and eqvt_at: "eqvt_at f (x, e, e2)" "eqvt_at f (x', e', e2')"
52+
and equal: "[[atom y]]lst. e2 = [[atom y']]lst. e2'" "x = x'" "e = e'"
53+
shows "[[atom y]]lst. f (x, e, e2) = [[atom y']]lst. f (x', e', e2')"
54+
proof -
55+
obtain c::"'a" where "atom c \<sharp> (y, y', e, e', x, x', e2, e2', f (x, e, e2), f (x', e', e2'))" using obtain_fresh by blast
56+
then have c: "atom c \<sharp> f (x, e, e2)" "atom c \<sharp> (x, e)" "atom c \<sharp> f (x', e', e2')" "atom c \<sharp> (x', e')" "atom c \<sharp> (y, e2, y', e2')" using fresh_Pair by auto
57+
58+
have 1: "[[atom y]]lst. f (x, e, e2) = [[atom c]]lst. f (x, e, (y \<leftrightarrow> c) \<bullet> e2)" by (rule Abs_lst_rename_deep[OF c(1) c(2) fresh(1) eqvt_at(1)])
59+
have 2: "[[atom y']]lst. f (x', e', e2') = [[atom c]]lst. f (x', e', (y' \<leftrightarrow> c) \<bullet> e2')" by (rule Abs_lst_rename_deep[OF c(3) c(4) fresh(2) eqvt_at(2)])
60+
have 3: "(y \<leftrightarrow> c) \<bullet> e2 = (y' \<leftrightarrow> c) \<bullet> e2'" by (rule Abs_lst_rename_both[OF c(5) equal(1)])
61+
62+
show ?thesis using 1 2 3 equal by argo
63+
qed
64+
65+
end

‎Semantics.thy‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
theory Semantics
2+
imports Syntax Defs Lemmas
3+
begin
4+
5+
no_notation HOL.implies (infixr "\<longrightarrow>" 25)
6+
7+
inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightarrow> _" 25) where
8+
ST_BetaI: "\<lbrakk> is_value v \<rbrakk> \<Longrightarrow> App (\<lambda> x : \<tau> . e) v \<longrightarrow> subst_term v x e"
9+
10+
| ST_AppI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> App e1 e \<longrightarrow> App e2 e"
11+
12+
| ST_App2I: "\<lbrakk> is_value v ; e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> App v e1 \<longrightarrow> App v e2"
13+
14+
| ST_SubstI: "\<lbrakk> is_value v \<rbrakk> \<Longrightarrow> Let x \<tau> v e \<longrightarrow> subst_term v x e"
15+
16+
| ST_LetI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> Let x \<tau> e1 e \<longrightarrow> Let x \<tau> e2 e"
17+
18+
| ST_BetaTI: "TyApp (\<Lambda> a . e) \<tau> \<longrightarrow> subst_term_type \<tau> a e"
19+
20+
| ST_AppTI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
21+
equivariance Step
22+
nominal_inductive Step .
23+
24+
definition beta_nf :: "term \<Rightarrow> bool" where
25+
"beta_nf e \<equiv> \<nexists>e'. e \<longrightarrow> e'"
26+
27+
lemma value_beta_nf: "is_value v \<Longrightarrow> beta_nf v"
28+
apply (cases v rule: term.exhaust)
29+
using Step.cases beta_nf_def by fastforce+
30+
31+
lemma Step_deterministic: "\<lbrakk> e \<longrightarrow> e1 ; e \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> e1 = e2"
32+
proof (induction e e1 arbitrary: e2 rule: Step.induct)
33+
case (ST_BetaI v x \<tau> e)
34+
from ST_BetaI(2) show ?case
35+
proof cases
36+
case (ST_BetaI y e')
37+
then show ?thesis using subst_term_same by blast
38+
next
39+
case (ST_AppI e')
40+
then show ?thesis using Step.cases by fastforce
41+
next
42+
case (ST_App2I e')
43+
then show ?thesis using ST_BetaI value_beta_nf beta_nf_def by blast
44+
qed
45+
next
46+
case (ST_AppI e1 e2 e)
47+
from ST_AppI(3) show ?case
48+
apply cases
49+
using ST_AppI Step.cases value_beta_nf beta_nf_def by fastforce+
50+
next
51+
case (ST_App2I v e1 e2)
52+
from ST_App2I(4) show ?case
53+
apply cases
54+
using ST_App2I.hyps(2) value_beta_nf beta_nf_def apply blast
55+
using ST_App2I.hyps(1) value_beta_nf beta_nf_def apply blast
56+
using ST_App2I value_beta_nf beta_nf_def by auto
57+
next
58+
case (ST_SubstI v x e)
59+
from ST_SubstI(2) show ?case
60+
proof cases
61+
case (ST_SubstI x e)
62+
then show ?thesis using subst_term_same by blast
63+
next
64+
case (ST_LetI e2 x e)
65+
then show ?thesis using ST_SubstI.hyps value_beta_nf beta_nf_def by blast
66+
qed
67+
next
68+
case (ST_LetI t1 t2 x \<tau> e)
69+
from ST_LetI(3) show ?case
70+
apply cases
71+
using ST_LetI value_beta_nf beta_nf_def by auto
72+
next
73+
case (ST_BetaTI a e \<tau>)
74+
then show ?case
75+
proof cases
76+
case (ST_BetaTI b e')
77+
then show ?thesis using subst_term_type_same by blast
78+
next
79+
case (ST_AppTI e2)
80+
then show ?thesis using is_value.simps(3) value_beta_nf beta_nf_def by blast
81+
qed
82+
next
83+
case (ST_AppTI e1 e2 \<tau>)
84+
from ST_AppTI(3) show ?case
85+
apply cases
86+
using ST_AppTI value_beta_nf beta_nf_def by auto
87+
qed
88+
89+
end

‎Syntax.thy‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
theory Syntax
2+
imports "Nominal2.Nominal2"
3+
begin
4+
5+
atom_decl "var"
6+
atom_decl "tyvar"
7+
8+
nominal_datatype "\<tau>" =
9+
TyUnit
10+
| TyVar "tyvar"
11+
| TyArrow "\<tau>" "\<tau>" ("_ \<rightarrow> _" 50)
12+
| TyForall a::"tyvar" t::"\<tau>" binds a in t ("\<forall> _ . _" 50)
13+
14+
nominal_datatype "term" =
15+
Var "var"
16+
| App "term" "term"
17+
| TyApp "term" "\<tau>"
18+
| Unit
19+
| Lam x::"var" "\<tau>" e::"term" binds x in e ("\<lambda> _ : _ . _" 50)
20+
| TyLam a::"tyvar" e::"term" binds a in e ("\<Lambda> _ . _" 50)
21+
| Let x::"var" "\<tau>" "term" e2::"term" binds x in e2
22+
23+
nominal_datatype "binder" =
24+
"BVar" "var" "\<tau>"
25+
| "BTyVar" "tyvar"
26+
27+
type_synonym "\<Gamma>" = "binder list"
28+
29+
lemma no_vars_in_ty[simp]: "atom (x :: var) \<sharp> (ty :: \<tau>)"
30+
by (induction ty rule: \<tau>.induct) auto
31+
32+
end

‎Typing.thy‎

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
theory Typing
2+
imports Syntax Defs
3+
begin
4+
5+
inductive Ty :: "\<Gamma> \<Rightarrow> \<tau> \<Rightarrow> bool" ("_ \<turnstile>\<^sub>t\<^sub>y _") where
6+
Ty_Unit: "\<Gamma> \<turnstile>\<^sub>t\<^sub>y TyUnit"
7+
8+
| Ty_Var: "\<lbrakk> BTyVar a \<in> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>t\<^sub>y TyVar a"
9+
10+
| Ty_Arrow: "\<lbrakk> \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau>1 ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>t\<^sub>y (\<tau>1 \<rightarrow> \<tau>2)"
11+
12+
| Ty_Forall: "\<lbrakk> BTyVar a # \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<sigma> ; atom a \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile>\<^sub>t\<^sub>y (\<forall>a. \<sigma>)"
13+
equivariance Ty
14+
nominal_inductive Ty avoids
15+
Ty_Forall: a
16+
by (auto simp: fresh_star_def)
17+
18+
inductive T :: "\<Gamma> \<Rightarrow> term \<Rightarrow> \<tau> \<Rightarrow> bool" ("_ \<turnstile> _ : _" 50) where
19+
T_UnitI: "(\<Gamma> \<turnstile> Unit : TyUnit)"
20+
21+
| T_VarI: "\<lbrakk> BVar x \<tau> \<in> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Var x) : \<tau>"
22+
23+
| T_AbsI: "\<lbrakk> atom x \<sharp> \<Gamma> ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau>1 ; BVar x \<tau>1 # \<Gamma> \<turnstile> e : \<tau>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda> x : \<tau>1 . e) : (\<tau>1 \<rightarrow> \<tau>2)"
24+
25+
| T_AppI: "\<lbrakk> \<Gamma> \<turnstile> e1 : (\<tau>1 \<rightarrow> \<tau>2) ; \<Gamma> \<turnstile> e2 : \<tau>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : \<tau>2"
26+
27+
| T_LetI: "\<lbrakk> atom x \<sharp> (\<Gamma>, e1) ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau>1 ; BVar x \<tau>1 # \<Gamma> \<turnstile> e2 : \<tau>2 ; \<Gamma> \<turnstile> e1 : \<tau>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Let x \<tau>1 e1 e2 : \<tau>2"
28+
29+
| T_AppTI: "\<lbrakk> \<Gamma> \<turnstile> e : (\<forall>a . \<sigma>) ; \<Gamma> \<turnstile>\<^sub>t\<^sub>y \<tau> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> TyApp e \<tau> : subst_type \<tau> a \<sigma>"
30+
31+
| T_AbsTI: "\<lbrakk> BTyVar a # \<Gamma> \<turnstile> e : \<sigma> ; atom a \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<Lambda> a . e) : (\<forall> a . \<sigma>)"
32+
equivariance T
33+
nominal_inductive T avoids
34+
T_AbsI: x
35+
| T_LetI: x
36+
| T_AbsTI: a
37+
by (auto simp: fresh_star_def fresh_Unit fresh_Pair)
38+
39+
end

0 commit comments

Comments
 (0)