Enhancements to proof automation and further unrestriction and substi…

…tution laws

Expressions.thy

@@ -297,4 +297,7 @@ lemma expr_if_reach [simp]: "P \<triangleleft> b \<triangleright> (Q \<trianglel
 lemma expr_if_disj [simp]: "P \<triangleleft> b \<triangleright> (P \<triangleleft> c \<triangleright> Q) = P \<triangleleft> b \<or> c \<triangleright> Q"
   by expr_auto
 
+lemma SEXP_expr_if [simp]: "[expr_if P b Q]\<^sub>e = expr_if P b Q"
+  by (simp add: SEXP_def)
+
 end

Extension.thy

@@ -46,6 +46,18 @@ lemma expr_post [simp]: "e\<^sup>> (s\<^sub>1, s\<^sub>2) = (@e)\<^sub>e s\<^sub
 lemma unrest_aext_expr_lens [unrest]: "\<lbrakk> mwb_lens x; x \<bowtie> a \<rbrakk> \<Longrightarrow> $x \<sharp> (P \<up> a)"
   by (expr_simp add: lens_indep.lens_put_irr2)
 
+lemma unrest_init_pre [unrest]: "\<lbrakk> mwb_lens x; $x \<sharp> e \<rbrakk> \<Longrightarrow> $x\<^sup>< \<sharp> e\<^sup><"
+  by expr_auto
+
+lemma unrest_init_post [unrest]: "mwb_lens x \<Longrightarrow> $x\<^sup>< \<sharp> e\<^sup>>"
+  by expr_auto
+
+lemma unrest_fin_pre [unrest]: "mwb_lens x \<Longrightarrow> $x\<^sup>> \<sharp> e\<^sup><"
+  by expr_auto
+
+lemma unrest_fin_post [unrest]: "\<lbrakk> mwb_lens x; $x \<sharp> e \<rbrakk> \<Longrightarrow> $x\<^sup>> \<sharp> e\<^sup>>"
+  by expr_auto
+
 subsection \<open> Substitutions \<close>
 
 definition subst_aext :: "'a subst \<Rightarrow> ('a \<Longrightarrow> 'b) \<Rightarrow> 'b subst"

Quantifiers.thy

@@ -30,6 +30,16 @@ translations
 lemma ex_is_liberation: "mwb_lens x \<Longrightarrow> (\<exists> x \<Zspot> P) = (P \\ $x)"
   by (expr_auto, metis mwb_lens_weak weak_lens.put_get)
 
+lemma ex_unrest_iff: "\<lbrakk> mwb_lens x \<rbrakk> \<Longrightarrow> ($x \<sharp> P) \<longleftrightarrow> (\<exists> x \<Zspot> P) = P"
+  by (simp add: ex_is_liberation unrest_liberate_iff)
+
+lemma ex_unrest: "\<lbrakk> mwb_lens x; $x \<sharp> P \<rbrakk> \<Longrightarrow> (\<exists> x \<Zspot> P) = P"
+  using ex_unrest_iff by blast
+
+lemma unrest_ex_in [unrest]:
+  "\<lbrakk> mwb_lens y; x \<subseteq>\<^sub>L y \<rbrakk> \<Longrightarrow> $x \<sharp> (\<exists> y \<Zspot> P)"
+  by (simp add: ex_expr_def sublens_pres_mwb sublens_put_put unrest_lens)
+
 lemma ex_as_subst: "vwb_lens x \<Longrightarrow> (\<exists> x \<Zspot> e) = (\<exists> v. e\<lbrakk>\<guillemotleft>v\<guillemotright>/x\<rbrakk>)\<^sub>e"
   by expr_auto
 
@@ -48,6 +58,10 @@ lemma ex_false [simp]: "(\<exists> x \<Zspot> (False)\<^sub>e) = (False)\<^sub>e
 lemma ex_disj [simp]: "(\<exists> x \<Zspot> (P \<or> Q)\<^sub>e) = ((\<exists> x \<Zspot> P) \<or> (\<exists> x \<Zspot> Q))\<^sub>e"
   by (expr_auto)
 
+lemma ex_plus:
+  "(\<exists> (y,x) \<Zspot> P) = (\<exists> x \<Zspot> \<exists> y \<Zspot> P)"
+  by (expr_auto)
+
 lemma all_as_ex: "(\<forall> x \<Zspot> P) = (\<not> (\<exists> x \<Zspot> \<not> P))\<^sub>e"
   by (expr_auto)
 

Shallow_Expressions.thy

@@ -2,4 +2,5 @@ theory Shallow_Expressions
   imports 
     Variables Expressions Unrestriction Substitutions Extension Liberation Quantifiers Collections
     EDefinitions Schemas
-begin end
+begin end
+

Substitutions.thy

@@ -354,10 +354,17 @@ qed
 
 text \<open> A tactic for proving unrestrictions by evaluating a special kind of substitution. \<close>
 
-method unrest = (simp add: unrest_ssubst var_alpha_combine usubst_eval)
+method unrest uses add = (simp add: add unrest_ssubst var_alpha_combine usubst_eval)
 
 text \<open> A tactic for evaluating substitutions. \<close>
 
-method subst_eval = (simp add: usubst_eval usubst unrest)
+method subst_eval uses add = (simp add: add usubst_eval usubst unrest)
+
+text \<open> We can exercise finer grained control over substitutions with the following method. \<close>
+
+declare vwb_lens_mwb [lens]
+declare mwb_lens_weak [lens]
+
+method subst_eval' = (simp only: lens usubst_eval usubst unrest SEXP_apply)
 
 end

Unrestriction.thy

@@ -69,6 +69,9 @@ lemma unrest_var_single [unrest]:
   "\<lbrakk> mwb_lens x; x \<bowtie> y \<rbrakk> \<Longrightarrow> $x \<sharp> ($y)\<^sub>e"
   by (simp add: expr_defs lens_indep.lens_put_irr2 lens_indep_sym lens_override_def var_alpha_def)
 
+lemma unrest_get [unrest]: "\<lbrakk> mwb_lens x; x \<bowtie> y \<rbrakk> \<Longrightarrow> $x \<sharp> get\<^bsub>y\<^esub>"
+  by (expr_simp, simp add: lens_indep.lens_put_irr2)
+
 lemma unrest_conj [unrest]:
   "\<lbrakk> x \<sharp> P; x \<sharp> Q \<rbrakk> \<Longrightarrow> x \<sharp> (P \<and> Q)\<^sub>e"
   by (auto simp add: expr_defs)