Skip to content

Commit 84d7851

Browse files
jvanbrueggejvanbruegge
committed
Refactor and split Soundness.thy
1 parent 96a3924 commit 84d7851

File tree

9 files changed

+275
-280
lines changed

9 files changed

+275
-280
lines changed

‎BetaEquivalence.thy‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
theory BetaEquivalence
2+
imports Semantics
3+
begin
4+
5+
lemma beta_same[simp]: "\<lbrakk> e1 \<longrightarrow>* e1' ; beta_nf e1 \<rbrakk> \<Longrightarrow> e1 = e1'"
6+
by (induction e1 e1' rule: Steps.induct) (auto simp: beta_nf_def)
7+
8+
fun path :: "term \<Rightarrow> term list \<Rightarrow> term \<Rightarrow> bool" where
9+
"path a [] b \<longleftrightarrow> a = b \<or> Step a b"
10+
| "path a (x#xs) b \<longleftrightarrow> Step a x \<and> path x xs b"
11+
12+
lemma path_snoc: "\<lbrakk> path a xs b ; Step b c \<rbrakk> \<Longrightarrow> path a (xs@[b]) c \<or> path a xs c"
13+
by (induction a xs b arbitrary: c rule: path.induct) auto
14+
15+
lemma Steps_concat: "\<lbrakk> e2 \<longrightarrow>* e3 ; e1 \<longrightarrow>* e2 \<rbrakk> \<Longrightarrow> e1 \<longrightarrow>* e3"
16+
apply (induction e2 e3 arbitrary: e1 rule: Steps.induct)
17+
using Steps.simps by blast+
18+
19+
lemma Steps_path: "a \<longrightarrow>* b \<longleftrightarrow> (\<exists>p. path a p b)"
20+
proof
21+
assume "a \<longrightarrow>* b"
22+
then show "\<exists>p. path a p b"
23+
proof (induction a b rule: Steps.induct)
24+
case (refl e)
25+
then have "path e [] e" by simp
26+
then show ?case by blast
27+
next
28+
case (trans e1 e2 e3)
29+
then obtain xs where "path e1 xs e2" by blast
30+
then have "path e1 (xs@[e2]) e3 \<or> path e1 xs e3" using trans(2) path_snoc by simp
31+
then show ?case by blast
32+
qed
33+
next
34+
assume "\<exists>p. path a p b"
35+
then obtain p where "path a p b" by blast
36+
then show "a \<longrightarrow>* b"
37+
proof (induction a p b rule: path.induct)
38+
case (1 a b)
39+
then show ?case using Steps.intros by auto
40+
next
41+
case (2 a x xs b)
42+
then have a: "a \<longrightarrow>* x" using Steps.intros by auto
43+
from 2 have b: "x \<longrightarrow>* b" by simp
44+
show ?case using Steps_concat[OF b a] .
45+
qed
46+
qed
47+
48+
lemma Steps_fwd_induct[consumes 1, case_names refl trans]:
49+
assumes "a \<longrightarrow>* b"
50+
and "\<And>x. P x x" "\<And>x y z. y \<longrightarrow>* z \<Longrightarrow> P y z \<Longrightarrow> Step x y \<Longrightarrow> P x z"
51+
shows "P a b"
52+
proof -
53+
from assms(1) obtain p where P: "path a p b" using Steps_path by blast
54+
then show ?thesis
55+
proof (induction a p b rule: path.induct)
56+
case (1 a b)
57+
then show ?case
58+
proof (cases "a = b")
59+
case True
60+
then show ?thesis using assms(2) by simp
61+
next
62+
case False
63+
then have 1: "Step a b" using 1 by simp
64+
have 2: "b \<longrightarrow>* b" using Steps.refl by simp
65+
show ?thesis using assms(3)[OF 2 assms(2) 1] .
66+
qed
67+
next
68+
case (2 a x xs b)
69+
then have 1: "P x b" by simp
70+
from 2 have 3: "x \<longrightarrow>* b" using Steps_path by auto
71+
from 2 have 4: "Step a x" by simp
72+
show ?case using assms(3)[OF 3 1 4] .
73+
qed
74+
qed
75+
76+
lemma beta_equivalence: "\<lbrakk> e1 \<longrightarrow>* e1' ; e2 \<longrightarrow>* e2' ; e1 = e2 ; beta_nf e1' ; beta_nf e2' \<rbrakk> \<Longrightarrow> e1' = e2'"
77+
proof (induction e1 e1' arbitrary: e2 e2' rule: Steps_fwd_induct)
78+
case (refl x)
79+
then show ?case by simp
80+
next
81+
case (trans x y z)
82+
then show ?case by (metis Steps.simps Steps_path beta_same path.elims(2) Step_deterministic)
83+
qed
84+
85+
end

‎Defs.thy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -114,4 +114,4 @@ next
114114
qed (auto simp: eqvt_def subst_term_type_graph_aux_def)
115115
nominal_termination (eqvt) by lexicographic_order
116116

117-
end
117+
end

‎Lemmas.thy‎

Lines changed: 44 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ theory Lemmas
33
begin
44

55
(* 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"
6+
lemma fresh_subst_term: "atom x \<sharp> e' \<Longrightarrow> atom x \<sharp> subst_term e' x e"
77
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>"
8+
lemma fresh_subst_type: "atom a \<sharp> \<tau> \<Longrightarrow> atom a \<sharp> subst_type \<tau> a \<sigma>"
99
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)
10+
lemma fresh_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_subst_type)
1212

1313
(* atom c \<sharp> t \<Longrightarrow> subst t' x t = subst t' c ((x \<leftrightarrow> c) \<bullet> t) *)
1414
lemma subst_term_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term e' x e = subst_term e' c ((x \<leftrightarrow> c) \<bullet> e)"
@@ -26,7 +26,7 @@ proof (nominal_induct e avoiding: c a \<tau> rule: term.strong_induct)
2626
next
2727
case (Let x \<tau>1 e1 e2)
2828
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))
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))
3030
qed (auto simp: flip_fresh_fresh fresh_at_base subst_type_var_name)
3131

3232
(* [[atom a]]lst. t = [[atom a2]]lst. t2 \<Longrightarrow> subst t' a t = subst t' a2 t2 *)
@@ -45,4 +45,42 @@ lemma fresh_not_isin_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin
4545
apply (induction \<Gamma>) apply simp
4646
by (metis (mono_tags, lifting) binder.fresh(1) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(2) isin.simps(3))
4747

48-
end
48+
(* atom x \<sharp> t \<Longrightarrow> subst t' x t = t *)
49+
lemma fresh_subst_term_same: "atom x \<sharp> e \<Longrightarrow> subst_term e' x e = e"
50+
proof (induction e' x e rule: subst_term.induct)
51+
case (2 y e x \<tau> e2)
52+
then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
53+
next
54+
case (7 y e x \<tau> e1 e2)
55+
then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
56+
qed auto
57+
58+
lemma fresh_subst_type_same: "atom a \<sharp> \<sigma> \<Longrightarrow> subst_type \<tau> a \<sigma> = \<sigma>"
59+
proof (induction \<tau> a \<sigma> rule: subst_type.induct)
60+
case (4 b \<tau> a \<sigma>)
61+
then show ?case
62+
using fresh_Pair fresh_at_base(2) fresh_def list.set(1) list.set(2) subst_type.simps(4) by fastforce
63+
qed auto
64+
65+
lemma fresh_subst_term_type_same: "atom a \<sharp> e \<Longrightarrow> subst_term_type \<tau> a e = e"
66+
proof (induction \<tau> a e rule: subst_term_type.induct)
67+
case (4 b \<tau> a e2)
68+
then show ?case
69+
by (simp add: "4.hyps" fresh_Pair fresh_at_base(2))
70+
qed (auto simp: fresh_subst_type_same)
71+
72+
(* misc *)
73+
lemma fv_supp_subset: "fv_\<tau> \<tau> \<subseteq> supp \<tau>"
74+
by (induction \<tau> rule: \<tau>.induct) (auto simp: \<tau>.supp \<tau>.fv_defs)
75+
76+
lemma subst_type_order: "\<lbrakk> atom b \<sharp> \<tau>' ; atom b \<sharp> a \<rbrakk> \<Longrightarrow> subst_type \<tau>' a (subst_type \<tau> b \<sigma>') = subst_type (subst_type \<tau>' a \<tau>) b (subst_type \<tau>' a \<sigma>')"
77+
proof (nominal_induct \<sigma>' avoiding: a b \<tau> \<tau>' rule: \<tau>.strong_induct)
78+
case (TyVar x)
79+
then show ?case using fresh_at_base(2) fresh_subst_type_same by auto
80+
next
81+
case (TyForall x1 x2a)
82+
then show ?case
83+
by (smt flip_at_simps(1) flip_at_simps(2) flip_commute fresh_Pair fresh_subst_type fresh_subst_type_same subst_type.eqvt subst_type.simps(4) subst_type_var_name)
84+
qed (auto simp: fresh_subst_type)
85+
86+
end

‎Nominal2_Lemmas.thy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,4 +62,4 @@ proof -
6262
show ?thesis using 1 2 3 equal by argo
6363
qed
6464

65-
end
65+
end

‎Semantics.thy‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,9 +21,16 @@ inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightar
2121
equivariance Step
2222
nominal_inductive Step .
2323

24+
inductive Steps :: "term \<Rightarrow> term \<Rightarrow> bool" (infix "\<longrightarrow>*" 70) where
25+
refl: "e \<longrightarrow>* e"
26+
| trans: "\<lbrakk> e1 \<longrightarrow>* e2 ; e2 \<longrightarrow> e3 \<rbrakk> \<Longrightarrow> Steps e1 e3"
27+
2428
definition beta_nf :: "term \<Rightarrow> bool" where
2529
"beta_nf e \<equiv> \<nexists>e'. e \<longrightarrow> e'"
2630

31+
definition stuck :: "term \<Rightarrow> bool" where
32+
"stuck e \<equiv> \<not>is_value e \<and> beta_nf e"
33+
2734
lemma value_beta_nf: "is_value v \<Longrightarrow> beta_nf v"
2835
apply (cases v rule: term.exhaust)
2936
using Step.cases beta_nf_def by fastforce+
@@ -86,4 +93,4 @@ next
8693
using ST_AppTI value_beta_nf beta_nf_def by auto
8794
qed
8895

89-
end
96+
end

0 commit comments

Comments
 (0)