Refactor proof code (#7)

Author: jvanbruegge

BetaEquivalence.thy

@@ -0,0 +1,85 @@
+theory BetaEquivalence
+  imports Semantics
+begin
+
+lemma beta_same[simp]: "\<lbrakk> e1 \<longrightarrow>* e1' ; beta_nf e1 \<rbrakk> \<Longrightarrow> e1 = e1'"
+  by (induction e1 e1' rule: Steps.induct) (auto simp: beta_nf_def)
+
+fun path :: "term \<Rightarrow> term list \<Rightarrow> term \<Rightarrow> bool" where
+  "path a [] b \<longleftrightarrow> a = b \<or> Step a b"
+| "path a (x#xs) b \<longleftrightarrow> Step a x \<and> path x xs b"
+
+lemma path_snoc: "\<lbrakk> path a xs b ; Step b c \<rbrakk> \<Longrightarrow> path a (xs@[b]) c \<or> path a xs c"
+  by (induction a xs b arbitrary: c rule: path.induct) auto
+
+lemma Steps_concat: "\<lbrakk> e2 \<longrightarrow>* e3 ; e1 \<longrightarrow>* e2 \<rbrakk> \<Longrightarrow> e1 \<longrightarrow>* e3"
+  apply (induction e2 e3 arbitrary: e1 rule: Steps.induct)
+  using Steps.simps by blast+
+
+lemma Steps_path: "a \<longrightarrow>* b \<longleftrightarrow> (\<exists>p. path a p b)"
+proof
+  assume "a \<longrightarrow>* b"
+  then show "\<exists>p. path a p b"
+  proof (induction a b rule: Steps.induct)
+    case (refl e)
+    then have "path e [] e" by simp
+    then show ?case by blast
+  next
+    case (trans e1 e2 e3)
+    then obtain xs where "path e1 xs e2" by blast
+    then have "path e1 (xs@[e2]) e3 \<or> path e1 xs e3" using trans(2) path_snoc by simp
+    then show ?case by blast
+  qed
+next
+  assume "\<exists>p. path a p b"
+  then obtain p where "path a p b" by blast
+  then show "a \<longrightarrow>* b"
+  proof (induction a p b rule: path.induct)
+    case (1 a b)
+    then show ?case using Steps.intros by auto
+  next
+    case (2 a x xs b)
+    then have a: "a \<longrightarrow>* x" using Steps.intros by auto
+    from 2 have b: "x \<longrightarrow>* b" by simp
+    show ?case using Steps_concat[OF b a] .
+  qed
+qed
+
+lemma Steps_fwd_induct[consumes 1, case_names refl trans]:
+  assumes "a \<longrightarrow>* b"
+    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"
+  shows "P a b"
+proof -
+  from assms(1) obtain p where P: "path a p b" using Steps_path by blast
+  then show ?thesis
+  proof (induction a p b rule: path.induct)
+    case (1 a b)
+    then show ?case
+    proof (cases "a = b")
+      case True
+      then show ?thesis using assms(2) by simp
+    next
+      case False
+      then have 1: "Step a b" using 1 by simp
+      have 2: "b \<longrightarrow>* b" using Steps.refl by simp
+      show ?thesis using assms(3)[OF 2 assms(2) 1] .
+    qed
+  next
+    case (2 a x xs b)
+    then have 1: "P x b" by simp
+    from 2 have 3: "x \<longrightarrow>* b" using Steps_path by auto
+    from 2 have 4: "Step a x" by simp
+    show ?case using assms(3)[OF 3 1 4] .
+  qed
+qed
+
+lemma beta_equivalence: "\<lbrakk> e1 \<longrightarrow>* e1' ; e2 \<longrightarrow>* e2' ; e1 = e2 ; beta_nf e1' ; beta_nf e2' \<rbrakk> \<Longrightarrow> e1' = e2'"
+proof (induction e1 e1' arbitrary: e2 e2' rule: Steps_fwd_induct)
+  case (refl x)
+  then show ?case by simp
+next
+  case (trans x y z)
+  then show ?case by (metis Steps.simps Steps_path beta_same path.elims(2) Step_deterministic)
+qed
+
+end

Defs.thy

@@ -12,4 +12,4 @@ RUN for t in Nominal2 FinFun; do \
 
 RUN ./Isabelle/bin/isabelle build -o system_heaps -b Nominal2
 
-COPY ROOT Defs.thy Soundness.thy ./
+COPY ROOT *.thy ./

Dockerfile

@@ -0,0 +1,86 @@
+theory Lemmas
+  imports Syntax Defs
+begin
+
+(* atom x \<sharp> t' \<Longrightarrow> atom x \<sharp> subst t' x t *)
+lemma fresh_subst_term: "atom x \<sharp> e' \<Longrightarrow> atom x \<sharp> subst_term e' x e"
+  by (nominal_induct e avoiding: x e' rule: term.strong_induct) auto
+lemma fresh_subst_type: "atom a \<sharp> \<tau> \<Longrightarrow> atom a \<sharp> subst_type \<tau> a \<sigma>"
+  by (nominal_induct \<sigma> avoiding: a \<tau> rule: \<tau>.strong_induct) auto
+lemma fresh_subst_term_type: "atom a \<sharp> \<tau> \<Longrightarrow> atom a \<sharp> subst_term_type \<tau> a e"
+  by (nominal_induct e avoiding: a \<tau> rule: term.strong_induct) (auto simp: fresh_subst_type)
+
+(* atom c \<sharp> t \<Longrightarrow> subst t' x t = subst t' c ((x \<leftrightarrow> c) \<bullet> t) *)
+lemma subst_term_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term e' x e = subst_term e' c ((x \<leftrightarrow> c) \<bullet> e)"
+proof (nominal_induct e avoiding: c x e' rule: term.strong_induct)
+  case (Let y \<tau> e1 e2)
+  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))
+qed (auto simp: flip_fresh_fresh fresh_at_base)
+lemma subst_type_var_name: "atom c \<sharp> \<sigma> \<Longrightarrow> subst_type \<tau> a \<sigma> = subst_type \<tau> c ((a \<leftrightarrow> c) \<bullet> \<sigma>)"
+  by (nominal_induct \<sigma> avoiding: c a \<tau> rule: \<tau>.strong_induct) (auto simp: fresh_at_base)
+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)"
+proof (nominal_induct e avoiding: c a \<tau> rule: term.strong_induct)
+  case (Lam x \<tau>1 e)
+  then show ?case
+    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))
+next
+  case (Let x \<tau>1 e1 e2)
+  then show ?case
+    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))
+qed (auto simp: flip_fresh_fresh fresh_at_base subst_type_var_name)
+
+(* [[atom a]]lst. t = [[atom a2]]lst. t2 \<Longrightarrow> subst t' a t = subst t' a2 t2 *)
+lemma subst_term_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term t a e = subst_term t a' e'"
+  by (metis Abs1_eq_iff(3) flip_commute subst_term_var_name)
+lemma subst_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_type \<tau> a e = subst_type \<tau> a' e'"
+  by (metis Abs1_eq_iff(3) flip_commute subst_type_var_name)
+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'"
+  by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name)
+
+(* atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (B x _) \<Gamma> *)
+lemma fresh_not_isin_tyvar: "atom a \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BTyVar a) \<Gamma>"
+  apply (induction \<Gamma>) apply simp
+  by (metis binder.fresh(2) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(4) isin.simps(5))
+lemma fresh_not_isin_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (BVar x \<tau>) \<Gamma>"
+  apply (induction \<Gamma>) apply simp
+  by (metis (mono_tags, lifting) binder.fresh(1) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(2) isin.simps(3))
+
+(* atom x \<sharp> t \<Longrightarrow> subst t' x t = t *)
+lemma fresh_subst_term_same: "atom x \<sharp> e \<Longrightarrow> subst_term e' x e = e"
+proof (induction e' x e rule: subst_term.induct)
+  case (2 y e x \<tau> e2)
+  then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
+next
+  case (7 y e x \<tau> e1 e2)
+  then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
+qed auto
+
+lemma fresh_subst_type_same: "atom a \<sharp> \<sigma> \<Longrightarrow> subst_type \<tau> a \<sigma> = \<sigma>"
+proof (induction \<tau> a \<sigma> rule: subst_type.induct)
+  case (4 b \<tau> a \<sigma>)
+  then show ?case
+    using fresh_Pair fresh_at_base(2) fresh_def list.set(1) list.set(2) subst_type.simps(4) by fastforce
+qed auto
+
+lemma fresh_subst_term_type_same: "atom a \<sharp> e \<Longrightarrow> subst_term_type \<tau> a e = e"
+proof (induction \<tau> a e rule: subst_term_type.induct)
+  case (4 b \<tau> a e2)
+  then show ?case
+    by (simp add: "4.hyps" fresh_Pair fresh_at_base(2))
+qed (auto simp: fresh_subst_type_same)
+
+(* misc *)
+lemma fv_supp_subset: "fv_\<tau> \<tau> \<subseteq> supp \<tau>"
+  by (induction \<tau> rule: \<tau>.induct) (auto simp: \<tau>.supp \<tau>.fv_defs)
+
+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>')"
+proof (nominal_induct \<sigma>' avoiding: a b \<tau> \<tau>' rule: \<tau>.strong_induct)
+case (TyVar x)
+  then show ?case using fresh_at_base(2) fresh_subst_type_same by auto
+next
+  case (TyForall x1 x2a)
+  then show ?case
+    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)
+qed (auto simp: fresh_subst_type)
+
+end

Lemmas.thy

@@ -0,0 +1,65 @@
+theory Nominal2_Lemmas
+  imports Main "Nominal2.Nominal2"
+begin
+
+lemma Abs_lst_rename:
+  fixes a c::"'a::at" and e::"'e::fs"
+  assumes "atom c \<sharp> e"
+  shows "[[atom a]]lst. e = [[atom c]]lst. (a \<leftrightarrow> c) \<bullet> e"
+proof -
+  from assms have 1: "atom c \<notin> supp e - set [atom a]" by (simp add: fresh_def)
+  have 2: "atom a \<notin> supp e - set [atom a]" by simp
+  show ?thesis using Abs_swap2[OF 2 1] by (simp add: flip_def)
+qed
+
+lemma eqvt_at_deep:
+  assumes fresh: "atom a \<sharp> (x, e)" "atom c \<sharp> (x, e)"
+  and eqvt_at: "eqvt_at f (x, e, e2)"
+shows "(a \<leftrightarrow> c) \<bullet> f (x, e, e2) = f (x, e, (a \<leftrightarrow> c) \<bullet> e2)"
+proof -
+  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
+  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
+
+  show ?thesis using 1 2 by argo
+qed
+
+lemma Abs_lst_rename_deep:
+  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"
+  assumes fresh: "atom c \<sharp> f (x, e, e2)" "atom c \<sharp> (x, e)" "atom a \<sharp> (x, e)"
+  and eqvt_at: "eqvt_at f (x, e, e2)"
+shows "[[atom a]]lst. f (x, e, e2) = [[atom c]]lst. f (x, e, (a \<leftrightarrow> c) \<bullet> e2)"
+proof -
+  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)])
+  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])
+  show ?thesis using 1 2 by argo
+qed
+
+lemma Abs_lst_rename_both:
+  fixes a c::"'a::at" and e e'::"'b::fs"
+  assumes fresh: "atom c \<sharp> (y, e, y', e')"
+  and equal: "[[atom y]]lst. e = [[atom y']]lst. e'"
+shows "(y \<leftrightarrow> c) \<bullet> e = (y' \<leftrightarrow> c) \<bullet> e'"
+proof -
+  from assms have "(y \<leftrightarrow> c) \<bullet> ([[atom y]]lst. e) = (y' \<leftrightarrow> c) \<bullet> ([[atom y']]lst. e')" by auto
+  then have "[[atom c]]lst. (y \<leftrightarrow> c) \<bullet> e = [[atom c]]lst. (y' \<leftrightarrow> c) \<bullet> e'" by auto
+  then show ?thesis using Abs1_eq(3) by blast
+qed
+
+lemma Abs_sumC:
+  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"
+  assumes fresh: "atom y \<sharp> (x, e)" "atom y' \<sharp> (x', e')"
+  and eqvt_at: "eqvt_at f (x, e, e2)" "eqvt_at f (x', e', e2')"
+  and equal: "[[atom y]]lst. e2 = [[atom y']]lst. e2'" "x = x'" "e = e'"
+  shows "[[atom y]]lst. f (x, e, e2) = [[atom y']]lst. f (x', e', e2')"
+proof -
+  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
+  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
+
+  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)])
+  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)])
+  have 3: "(y \<leftrightarrow> c) \<bullet> e2 = (y' \<leftrightarrow> c) \<bullet> e2'" by (rule Abs_lst_rename_both[OF c(5) equal(1)])
+
+  show ?thesis using 1 2 3 equal by argo
+qed
+
+end

Nominal2_Lemmas.thy

@@ -1,4 +1,4 @@
 session Lambda = HOL + sessions "HOL-Eisbach" Nominal2
 theories
-    Defs
+    BetaEquivalence
     Soundness

ROOT

@@ -0,0 +1,96 @@
+theory Semantics
+  imports Syntax Defs Lemmas
+begin
+
+no_notation HOL.implies (infixr "\<longrightarrow>" 25)
+
+inductive Step :: "term \<Rightarrow> term \<Rightarrow> bool" ("_ \<longrightarrow> _" 25) where
+  ST_BetaI: "\<lbrakk> is_value v \<rbrakk> \<Longrightarrow> App (\<lambda> x : \<tau> . e) v \<longrightarrow> subst_term v x e"
+
+| ST_AppI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> App e1 e \<longrightarrow> App e2 e"
+
+| ST_App2I: "\<lbrakk> is_value v ; e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> App v e1 \<longrightarrow> App v e2"
+
+| ST_SubstI: "\<lbrakk> is_value v \<rbrakk> \<Longrightarrow> Let x \<tau> v e \<longrightarrow> subst_term v x e"
+
+| ST_LetI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> Let x \<tau> e1 e \<longrightarrow> Let x \<tau> e2 e"
+
+| ST_BetaTI: "TyApp (\<Lambda> a . e) \<tau> \<longrightarrow> subst_term_type \<tau> a e"
+
+| ST_AppTI: "\<lbrakk> e1 \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> TyApp e1 \<tau> \<longrightarrow> TyApp e2 \<tau>"
+equivariance Step
+nominal_inductive Step .
+
+inductive Steps :: "term \<Rightarrow> term \<Rightarrow> bool" (infix "\<longrightarrow>*" 70) where
+  refl: "e \<longrightarrow>* e"
+| trans: "\<lbrakk> e1 \<longrightarrow>* e2 ; e2 \<longrightarrow> e3 \<rbrakk> \<Longrightarrow> Steps e1 e3"
+
+definition beta_nf :: "term \<Rightarrow> bool" where
+  "beta_nf e \<equiv> \<nexists>e'. e \<longrightarrow> e'"
+
+definition stuck :: "term \<Rightarrow> bool" where
+  "stuck e \<equiv> \<not>is_value e \<and> beta_nf e"
+
+lemma value_beta_nf: "is_value v \<Longrightarrow> beta_nf v"
+  apply (cases v rule: term.exhaust)
+  using Step.cases beta_nf_def by fastforce+
+
+lemma Step_deterministic: "\<lbrakk> e \<longrightarrow> e1 ; e \<longrightarrow> e2 \<rbrakk> \<Longrightarrow> e1 = e2"
+proof (induction e e1 arbitrary: e2 rule: Step.induct)
+  case (ST_BetaI v x \<tau> e)
+  from ST_BetaI(2) show ?case
+  proof cases
+    case (ST_BetaI y e')
+    then show ?thesis using subst_term_same by blast
+  next
+    case (ST_AppI e')
+    then show ?thesis using Step.cases by fastforce
+  next
+    case (ST_App2I e')
+    then show ?thesis using ST_BetaI value_beta_nf beta_nf_def by blast
+  qed
+next
+  case (ST_AppI e1 e2 e)
+  from ST_AppI(3) show ?case
+    apply cases
+    using ST_AppI Step.cases value_beta_nf beta_nf_def by fastforce+
+next
+  case (ST_App2I v e1 e2)
+  from ST_App2I(4) show ?case
+    apply cases
+    using ST_App2I.hyps(2) value_beta_nf beta_nf_def apply blast
+    using ST_App2I.hyps(1) value_beta_nf beta_nf_def apply blast
+    using ST_App2I value_beta_nf beta_nf_def by auto
+next
+  case (ST_SubstI v x e)
+  from ST_SubstI(2) show ?case
+  proof cases
+    case (ST_SubstI x e)
+    then show ?thesis using subst_term_same by blast
+  next
+    case (ST_LetI e2 x e)
+    then show ?thesis using ST_SubstI.hyps value_beta_nf beta_nf_def by blast
+  qed
+next
+  case (ST_LetI t1 t2 x \<tau> e)
+  from ST_LetI(3) show ?case
+    apply cases
+    using ST_LetI value_beta_nf beta_nf_def by auto
+next
+  case (ST_BetaTI a e \<tau>)
+  then show ?case
+  proof cases
+    case (ST_BetaTI b e')
+    then show ?thesis using subst_term_type_same by blast
+  next
+    case (ST_AppTI e2)
+    then show ?thesis using is_value.simps(3) value_beta_nf beta_nf_def by blast
+  qed
+next
+  case (ST_AppTI e1 e2 \<tau>)
+  from ST_AppTI(3) show ?case
+    apply cases
+    using ST_AppTI value_beta_nf beta_nf_def by auto
+qed
+
+end