TITLE: Rationalizing expressions
QUESTION [9 upvotes]: In my precalc book, I have the following problem:
Calculate $a+b+c$ if $a,b,c\in\mathbb{Q}$ and
$$\sqrt[3]{\sqrt[3]{2}-1}=\sqrt[3]{a}+\sqrt[3]{b}+\sqrt[3]{c}$$
I think that the RHS can stay untouched, while operating the LHS, but I can't find a way to factor $\sqrt[3]{2}-1$ as the third power of something. Any help is greatly appreciated.
With the help of Olegg,  i got the solution
$$\sqrt[3]{\sqrt[3]{2}-1}=\sqrt[3]{\frac{(\sqrt[3]{2}-1)(\sqrt[3]{4}+\sqrt[3]{2}+1)}{\sqrt[3]{4}+\sqrt[3]{2}+1}}$$
$$\sqrt[3]{\frac{1}{\sqrt[3]{4}+\sqrt[3]{2}+1}}$$
$$\sqrt[3]{\frac{1}{(\sqrt[3]{\frac{1}{3}}+\sqrt[3]{\frac{2}{3}})^3}}$$
$$\frac{1}{\sqrt[3]{\frac{1}{3}}+\sqrt[3]{\frac{2}{3}}}$$
$${\sqrt[3]{\frac{1}{9}}-\sqrt[3]{\frac{2}{9}}+\sqrt[3]{\frac{4}{9}}}$$
$$a+b+c=\frac{1}{3}$$

REPLY [2 votes]: Hint.
$(a,b,c) = \Bigl(\dfrac{1}{9},-\dfrac{2}{9},\dfrac{4}{9}\Bigr)$ $-$  one of rational solutions (ignoring permutations).
So, $a+b+c=\dfrac{1}{3}$.


text:
(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2020

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

(*  Title:      Intruder_Deduction.thy
    Author:     Andreas Viktor Hess, DTU
*)

section \<open>Dolev-Yao Intruder Model\<close>
theory Intruder_Deduction
imports Messages More_Unification
begin

subsection \<open>Syntax for the Intruder Deduction Relations\<close>
consts INTRUDER_SYNTH::"('f,'v) terms \<Rightarrow> ('f,'v) term \<Rightarrow> bool" (infix "\<turnstile>\<^sub>c" 50)
consts INTRUDER_DEDUCT::"('f,'v) terms \<Rightarrow> ('f,'v) term \<Rightarrow> bool" (infix "\<turnstile>" 50)

subsection \<open>Intruder Model Locale\<close>
text \<open>
  The intruder model is parameterized over arbitrary function symbols (e.g, cryptographic operators)
  and variables. It requires three functions:
  - \<open>arity\<close> that assigns an arity to each function symbol.
  - \<open>public\<close> that partitions the function symbols into those that will be available to the intruder
    and those that will not.
  - \<open>Ana\<close>, the analysis interface, that defines how messages can be decomposed (e.g., decryption).
\<close>
locale intruder_model =
  fixes arity :: "'fun \<Rightarrow> nat"
    and public :: "'fun \<Rightarrow> bool"
    and Ana :: "('fun,'var) term \<Rightarrow> (('fun,'var) term list \<times> ('fun,'var) term list)"
  assumes Ana_keys_fv: "\<And>t K R. Ana t = (K,R) \<Longrightarrow> fv\<^sub>s\<^sub>e\<^sub>t (set K) \<subseteq> fv t"
    and Ana_keys_wf: "\<And>t k K R f T.
      Ana t = (K,R) \<Longrightarrow> (\<And>g S. Fun g S \<sqsubseteq> t \<Longrightarrow> length S = arity g)
                    \<Longrightarrow> k \<in> set K \<Longrightarrow> Fun f T \<sqsubseteq> k \<Longrightarrow> length T = arity f"
    and Ana_var[simp]: "\<And>x. Ana (Var x) = ([],[])"
    and Ana_fun_subterm: "\<And>f T K R. Ana (Fun f T) = (K,R) \<Longrightarrow> set R \<subseteq> set T"
    and Ana_subst: "\<And>t \<delta> K R. \<lbrakk>Ana t = (K,R); K \<noteq> [] \<or> R \<noteq> []\<rbrakk> \<Longrightarrow> Ana (t \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>,R \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
begin

lemma Ana_subterm: assumes "Ana t = (K,T)" shows "set T \<subset> subterms t"
using assms
by (cases t)
   (simp add: psubsetI,
    metis Ana_fun_subterm Fun_gt_params UN_I term.order_refl
          params_subterms psubsetI subset_antisym subset_trans)

lemma Ana_subterm': "s \<in> set (snd (Ana t)) \<Longrightarrow> s \<sqsubseteq> t"
using Ana_subterm by (cases "Ana t") auto

lemma Ana_vars: assumes "Ana t = (K,M)" shows "fv\<^sub>s\<^sub>e\<^sub>t (set K) \<subseteq> fv t" "fv\<^sub>s\<^sub>e\<^sub>t (set M) \<subseteq> fv t"
by (rule Ana_keys_fv[OF assms]) (use Ana_subterm[OF assms] subtermeq_vars_subset in auto)

abbreviation \<V> where "\<V> \<equiv> UNIV::'var set"
abbreviation \<Sigma>n ("\<Sigma>\<^sup>_") where "\<Sigma>\<^sup>n \<equiv> {f::'fun. arity f = n}"
abbreviation \<Sigma>npub ("\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>_") where "\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n \<equiv> {f. public f} \<inter> \<Sigma>\<^sup>n"
abbreviation \<Sigma>npriv ("\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>_") where "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n \<equiv> {f. \<not>public f} \<inter> \<Sigma>\<^sup>n"
abbreviation \<Sigma>\<^sub>p\<^sub>u\<^sub>b where "\<Sigma>\<^sub>p\<^sub>u\<^sub>b \<equiv> (\<Union>n. \<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n)"
abbreviation \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> (\<Union>n. \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n)"
abbreviation \<Sigma> where "\<Sigma> \<equiv> (\<Union>n. \<Sigma>\<^sup>n)"
abbreviation \<C> where "\<C> \<equiv> \<Sigma>\<^sup>0"
abbreviation \<C>\<^sub>p\<^sub>u\<^sub>b where "\<C>\<^sub>p\<^sub>u\<^sub>b \<equiv> {f. public f} \<inter> \<C>"
abbreviation \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> {f. \<not>public f} \<inter> \<C>"
abbreviation \<Sigma>\<^sub>f where "\<Sigma>\<^sub>f \<equiv> \<Sigma> - \<C>"
abbreviation \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b where "\<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<equiv> \<Sigma>\<^sub>f \<inter> \<Sigma>\<^sub>p\<^sub>u\<^sub>b"
abbreviation \<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v where "\<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<equiv> \<Sigma>\<^sub>f \<inter> \<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v"

lemma disjoint_fun_syms: "\<Sigma>\<^sub>f \<inter> \<C> = {}" by auto
lemma id_union_univ: "\<Sigma>\<^sub>f \<union> \<C> = UNIV" "\<Sigma> = UNIV" by auto
lemma const_arity_eq_zero[dest]: "c \<in> \<C> \<Longrightarrow> arity c = 0" by simp
lemma const_pub_arity_eq_zero[dest]: "c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> arity c = 0 \<and> public c" by simp
lemma const_priv_arity_eq_zero[dest]: "c \<in> \<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v \<Longrightarrow> arity c = 0 \<and> \<not>public c" by simp
lemma fun_arity_gt_zero[dest]: "f \<in> \<Sigma>\<^sub>f \<Longrightarrow> arity f > 0" by fastforce
lemma pub_fun_public[dest]: "f \<in> \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> public f" by fastforce
lemma pub_fun_arity_gt_zero[dest]: "f \<in> \<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b \<Longrightarrow> arity f > 0" by fastforce

lemma \<Sigma>\<^sub>f_unfold: "\<Sigma>\<^sub>f = {f::'fun. arity f > 0}" by auto
lemma \<C>_unfold: "\<C> = {f::'fun. arity f = 0}" by auto
lemma \<C>pub_unfold: "\<C>\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f = 0 \<and> public f}" by auto
lemma \<C>priv_unfold: "\<C>\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f = 0 \<and> \<not>public f}" by auto
lemma \<Sigma>npub_unfold: "(\<Sigma>\<^sub>p\<^sub>u\<^sub>b\<^sup>n) = {f::'fun. arity f = n \<and> public f}" by auto
lemma \<Sigma>npriv_unfold: "(\<Sigma>\<^sub>p\<^sub>r\<^sub>i\<^sub>v\<^sup>n) = {f::'fun. arity f = n \<and> \<not>public f}" by auto
lemma \<Sigma>fpub_unfold: "\<Sigma>\<^sub>f\<^sub>p\<^sub>u\<^sub>b = {f::'fun. arity f > 0 \<and> public f}" by auto
lemma \<Sigma>fpriv_unfold: "\<Sigma>\<^sub>f\<^sub>p\<^sub>r\<^sub>i\<^sub>v = {f::'fun. arity f > 0 \<and> \<not>public f}" by auto
lemma \<Sigma>n_m_eq: "\<lbrakk>(\<Sigma>\<^sup>n) \<noteq> {}; (\<Sigma>\<^sup>n) = (\<Sigma>\<^sup>m)\<rbrakk> \<Longrightarrow> n = m" by auto

subsection \<open>Term Well-formedness\<close>
definition "wf\<^sub>t\<^sub>r\<^sub>m t \<equiv> \<forall>f T. Fun f T \<sqsubseteq> t \<longrightarrow> length T = arity f"

abbreviation "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s T \<equiv> \<forall>t \<in> T. wf\<^sub>t\<^sub>r\<^sub>m t"

lemma Ana_keys_wf': "Ana t = (K,T) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> k \<in> set K \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m k"
using Ana_keys_wf unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by metis

lemma wf_trm_Var[simp]: "wf\<^sub>t\<^sub>r\<^sub>m (Var x)" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp

lemma wf_trm_subst_range_Var[simp]: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range Var)" by simp

lemma wf_trm_subst_range_iff: "(\<forall>x. wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)) \<longleftrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
by force

lemma wf_trm_subst_rangeD: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)"
by (metis wf_trm_subst_range_iff)

lemma wf_trm_subst_rangeI[intro]:
  "(\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
by (metis wf_trm_subst_range_iff)

lemma wf_trmI[intro]:
  assumes "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t" "length T = arity f"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
using assms unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto

lemma wf_trm_subterm: "\<lbrakk>wf\<^sub>t\<^sub>r\<^sub>m t; s \<sqsubset> t\<rbrakk> \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m s"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (induct t) auto

lemma wf_trm_subtermeq:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "s \<sqsubseteq> t"
  shows "wf\<^sub>t\<^sub>r\<^sub>m s"
proof (cases "s = t")
  case False thus "wf\<^sub>t\<^sub>r\<^sub>m s" using assms(2) wf_trm_subterm[OF assms(1)] by simp
qed (metis assms(1))

lemma wf_trm_param:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" "t \<in> set T"
  shows "wf\<^sub>t\<^sub>r\<^sub>m t"
by (meson assms subtermeqI'' wf_trm_subtermeq)

lemma wf_trm_param_idx:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
    and "i < length T"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (T ! i)"
using wf_trm_param[OF assms(1), of "T ! i"] assms(2)
by fastforce

lemma wf_trm_subst:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
  shows "wf\<^sub>t\<^sub>r\<^sub>m t = wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
proof
  show "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
  proof (induction t)
    case (Fun f T)
    hence "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
      by (meson wf\<^sub>t\<^sub>r\<^sub>m_def Fun_param_is_subterm term.order_trans)
    hence "\<And>t. t \<in> set T \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)" using Fun.IH by auto
    moreover have "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f"
      using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
    ultimately show ?case by fastforce
  qed (simp add: wf_trm_subst_rangeD[OF assms])

  show "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
  proof (induction t)
    case (Fun f T)
    hence "wf\<^sub>t\<^sub>r\<^sub>m t" when "t \<in> set (map (\<lambda>s. s \<cdot> \<delta>) T)" for t
      by (metis that wf\<^sub>t\<^sub>r\<^sub>m_def Fun_param_is_subterm term.order_trans subst_apply_term.simps(2))
    hence "wf\<^sub>t\<^sub>r\<^sub>m t" when "t \<in> set T" for t using that Fun.IH by auto
    moreover have "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f"
      using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
    ultimately show ?case by fastforce
  qed (simp add: assms)
qed

lemma wf_trm_subst_singleton:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" shows "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> Var(v := t'))"
proof -
  have "wf\<^sub>t\<^sub>r\<^sub>m ((Var(v := t')) w)" for w using assms(2) unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by simp
  thus ?thesis using assms(1) wf_trm_subst[of "Var(v := t')" t, OF wf_trm_subst_rangeI] by simp
qed

lemma wf_trm_subst_rm_vars:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> rm_vars X \<delta>)"
using assms
proof (induction t)
  case (Fun f T)
  have "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>)" when "t \<in> set T" for t
    using that wf_trm_param[of f "map (\<lambda>t. t \<cdot> \<delta>) T"] Fun.prems
    by auto
  hence "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> rm_vars X \<delta>)" when "t \<in> set T" for t using that Fun.IH by simp
  moreover have "length T = arity f" using Fun.prems unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
  ultimately show ?case unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
qed simp

lemma wf_trm_subst_rm_vars': "wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (rm_vars X \<delta> v)"
by auto

lemma wf_trms_subst:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
by (metis (no_types, lifting) assms imageE wf_trm_subst)

lemma wf_trms_subst_rm_vars:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>)"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t rm_vars X \<delta>)"
using assms wf_trm_subst_rm_vars by blast

lemma wf_trms_subst_rm_vars':
  assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (rm_vars X \<delta>))"
using assms by force

lemma wf_trms_subst_compose:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)" "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<theta> \<circ>\<^sub>s \<delta>))"
using assms subst_img_comp_subset' wf_trm_subst by blast

lemma wf_trm_subst_compose:
  fixes \<delta>::"('fun, 'v) subst"
  assumes "wf\<^sub>t\<^sub>r\<^sub>m (\<theta> x)" "\<And>x. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> x)"
  shows "wf\<^sub>t\<^sub>r\<^sub>m ((\<theta> \<circ>\<^sub>s \<delta>) x)"
using wf_trm_subst[of \<delta> "\<theta> x", OF wf_trm_subst_rangeI[OF assms(2)]] assms(1)
      subst_subst_compose[of "Var x" \<theta> \<delta>]
      subst_apply_term.simps(1)[of x \<theta>]
      subst_apply_term.simps(1)[of x "\<theta> \<circ>\<^sub>s \<delta>"]
by argo

lemma wf_trms_Var_range:
  assumes "subst_range \<delta> \<subseteq> range Var"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<delta>)"
using assms by fastforce

lemma wf_trms_subst_compose_Var_range:
  assumes "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<theta>)"
    and "subst_range \<delta> \<subseteq> range Var"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<delta> \<circ>\<^sub>s \<theta>))"
    and "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range (\<theta> \<circ>\<^sub>s \<delta>))"
using assms wf_trms_subst_compose wf_trms_Var_range by metis+

lemma wf_trm_subst_inv: "wf\<^sub>t\<^sub>r\<^sub>m (t \<cdot> \<delta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by (induct t) auto

lemma wf_trms_subst_inv: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta>) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M"
using wf_trm_subst_inv by fast

lemma wf_trm_subterms: "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subterms t)"
using wf_trm_subterm by blast

lemma wf_trms_subterms: "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subterms\<^sub>s\<^sub>e\<^sub>t M)"
using wf_trm_subterms by blast

lemma wf_trm_arity: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T) \<Longrightarrow> length T = arity f"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by blast

lemma wf_trm_subterm_arity: "wf\<^sub>t\<^sub>r\<^sub>m t \<Longrightarrow> Fun f T \<sqsubseteq> t \<Longrightarrow> length T = arity f"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by blast

lemma unify_list_wf_trm:
  assumes "Unification.unify E B = Some U" "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
  and "\<forall>(v,t) \<in> set B. wf\<^sub>t\<^sub>r\<^sub>m t"
  shows "\<forall>(v,t) \<in> set U. wf\<^sub>t\<^sub>r\<^sub>m t"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case (1 B U) thus ?case by auto
next
  case (2 f T g S E B U)
  have wf_fun: "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun g S)" using "2.prems"(2) by auto
  from "2.prems"(1) obtain E' where *: "decompose (Fun f T) (Fun g S) = Some E'"
    and [simp]: "f = g" "length T = length S" "E' = zip T S"
    and **: "Unification.unify (E'@E) B = Some U"
    by (auto split: option.splits)
  hence "t \<sqsubset> Fun f T" "t' \<sqsubset> Fun g S" when "(t,t') \<in> set E'" for t t'
    using that by (metis zip_arg_subterm(1), metis zip_arg_subterm(2))
  hence "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" when "(t,t') \<in> set E'" for t t'
    using wf_trm_subterm wf_fun \<open>f = g\<close> that by blast+
  thus ?case using "2.IH"[OF * ** _ "2.prems"(3)] "2.prems"(2) by fastforce
next
  case (3 v t E B)
  hence *: "\<forall>(w,x) \<in> set ((v, t) # B). wf\<^sub>t\<^sub>r\<^sub>m x"
      and **: "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t"
    by auto

  show ?case
  proof (cases "t = Var v")
    case True thus ?thesis using "3.prems" "3.IH"(1) by auto
  next
    case False
    hence "v \<notin> fv t" using "3.prems"(1) by auto
    hence "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using \<open>t \<noteq> Var v\<close> "3.prems"(1) by auto
    moreover have "\<forall>(s, t) \<in> set (subst_list (subst v t) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
      using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m t\<close>] "3.prems"(2)
      unfolding subst_list_def subst_def by auto
    ultimately show ?thesis using "3.IH"(2)[OF \<open>t \<noteq> Var v\<close> \<open>v \<notin> fv t\<close> _ _ *] by metis
  qed
next
  case (4 f T v E B U)
  hence *: "\<forall>(w,x) \<in> set ((v, Fun f T) # B). wf\<^sub>t\<^sub>r\<^sub>m x"
      and **: "\<forall>(s,t) \<in> set E. wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)"
    by auto

  have "v \<notin> fv (Fun f T)" using "4.prems"(1) by force
  hence "Unification.unify (subst_list (subst v (Fun f T)) E) ((v, Fun f T)#B) = Some U"
    using "4.prems"(1) by auto
  moreover have "\<forall>(s, t) \<in> set (subst_list (subst v (Fun f T)) E). wf\<^sub>t\<^sub>r\<^sub>m s \<and> wf\<^sub>t\<^sub>r\<^sub>m t"
    using wf_trm_subst_singleton[OF _ \<open>wf\<^sub>t\<^sub>r\<^sub>m (Fun f T)\<close>] "4.prems"(2)
    unfolding subst_list_def subst_def by auto
  ultimately show ?case using "4.IH"[OF \<open>v \<notin> fv (Fun f T)\<close> _ _ *] by metis
qed

lemma mgu_wf_trm:
  assumes "mgu s t = Some \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t"
  shows "wf\<^sub>t\<^sub>r\<^sub>m (\<sigma> v)"
proof -
  from assms obtain \<sigma>' where "subst_of \<sigma>' = \<sigma>" "\<forall>(v,t) \<in> set \<sigma>'. wf\<^sub>t\<^sub>r\<^sub>m t"
    using unify_list_wf_trm[of "[(s,t)]" "[]"] by (auto split: option.splits)
  thus ?thesis
  proof (induction \<sigma>' arbitrary: \<sigma> v rule: List.rev_induct)
    case (snoc x \<sigma>' \<sigma> v)
    define \<theta> where "\<theta> = subst_of \<sigma>'"
    hence "wf\<^sub>t\<^sub>r\<^sub>m (\<theta> v)" for v using snoc.prems(2) snoc.IH[of \<theta>] by fastforce
    moreover obtain w t where x: "x = (w,t)" by (metis surj_pair)
    hence \<sigma>: "\<sigma> = Var(w := t) \<circ>\<^sub>s \<theta>" using snoc.prems(1) by (simp add: subst_def \<theta>_def)
    moreover have "wf\<^sub>t\<^sub>r\<^sub>m t" using snoc.prems(2) x by auto
    ultimately show ?case using wf_trm_subst[of _ t] unfolding subst_compose_def by auto
  qed (simp add: wf\<^sub>t\<^sub>r\<^sub>m_def)
qed

lemma mgu_wf_trms:
  assumes "mgu s t = Some \<sigma>" "wf\<^sub>t\<^sub>r\<^sub>m s" "wf\<^sub>t\<^sub>r\<^sub>m t"
  shows "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s (subst_range \<sigma>)"
using mgu_wf_trm[OF assms] by simp

subsection \<open>Definitions: Intruder Deduction Relations\<close>
text \<open>
  A standard Dolev-Yao intruder.
\<close>
inductive intruder_deduct::"('fun,'var) terms \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
where
  Axiom[simp]:   "t \<in> M \<Longrightarrow> intruder_deduct M t"
| Compose[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> intruder_deduct M t\<rbrakk>
                  \<Longrightarrow> intruder_deduct M (Fun f T)"
| Decompose:     "\<lbrakk>intruder_deduct M t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> intruder_deduct M k;
                   t\<^sub>i \<in> set T\<rbrakk>
                  \<Longrightarrow> intruder_deduct M t\<^sub>i"

text \<open>
  A variant of the intruder relation which limits the intruder to composition only.
\<close>
inductive intruder_synth::"('fun,'var) terms \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
where
  AxiomC[simp]:   "t \<in> M \<Longrightarrow> intruder_synth M t"
| ComposeC[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> intruder_synth M t\<rbrakk>
                    \<Longrightarrow> intruder_synth M (Fun f T)"

adhoc_overloading INTRUDER_DEDUCT intruder_deduct
adhoc_overloading INTRUDER_SYNTH intruder_synth

lemma intruder_deduct_induct[consumes 1, case_names Axiom Compose Decompose]:
  assumes "M \<turnstile> t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
          "\<And>T f. \<lbrakk>length T = arity f; public f;
                  \<And>t. t \<in> set T \<Longrightarrow> M \<turnstile> t;
                  \<And>t. t \<in> set T \<Longrightarrow> P M t\<rbrakk> \<Longrightarrow> P M (Fun f T)"
          "\<And>t K T t\<^sub>i. \<lbrakk>M \<turnstile> t; P M t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> M \<turnstile> k;
                       \<And>k. k \<in> set K \<Longrightarrow> P M k; t\<^sub>i \<in> set T\<rbrakk> \<Longrightarrow> P M t\<^sub>i"
  shows "P M t"
using assms by (induct rule: intruder_deduct.induct) blast+

lemma intruder_synth_induct[consumes 1, case_names AxiomC ComposeC]:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M \<turnstile>\<^sub>c t" "\<And>t. t \<in> M \<Longrightarrow> P M t"
          "\<And>T f. \<lbrakk>length T = arity f; public f;
                  \<And>t. t \<in> set T \<Longrightarrow> M \<turnstile>\<^sub>c t;
                  \<And>t. t \<in> set T \<Longrightarrow> P M t\<rbrakk> \<Longrightarrow> P M (Fun f T)"
  shows "P M t"
using assms by (induct rule: intruder_synth.induct) auto

subsection \<open>Definitions: Analyzed Knowledge and Public Ground Well-formed Terms (PGWTs)\<close>
definition analyzed::"('fun,'var) terms \<Rightarrow> bool" where
  "analyzed M \<equiv> \<forall>t. M \<turnstile> t \<longleftrightarrow> M \<turnstile>\<^sub>c t"

definition analyzed_in where
  "analyzed_in t M \<equiv> \<forall>K R. (Ana t = (K,R) \<and> (\<forall>k \<in> set K. M \<turnstile>\<^sub>c k)) \<longrightarrow> (\<forall>r \<in> set R. M \<turnstile>\<^sub>c r)"

definition decomp_closure::"('fun,'var) terms \<Rightarrow> ('fun,'var) terms \<Rightarrow> bool" where
  "decomp_closure M M' \<equiv> \<forall>t. M \<turnstile> t \<and> (\<exists>t' \<in> M. t \<sqsubseteq> t') \<longleftrightarrow> t \<in> M'"

inductive public_ground_wf_term::"('fun,'var) term \<Rightarrow> bool" where
  PGWT[simp]: "\<lbrakk>public f; arity f = length T;
                \<And>t. t \<in> set T \<Longrightarrow> public_ground_wf_term t\<rbrakk>
                  \<Longrightarrow> public_ground_wf_term (Fun f T)"

abbreviation "public_ground_wf_terms \<equiv> {t. public_ground_wf_term t}"

lemma public_const_deduct:
  assumes "c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b"
  shows "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
proof -
  have "arity c = 0" "public c" using const_arity_eq_zero \<open>c \<in> \<C>\<^sub>p\<^sub>u\<^sub>b\<close> by auto
  thus "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
    using intruder_synth.ComposeC[OF _ \<open>public c\<close>, of "[]"]
          intruder_deduct.Compose[OF _ \<open>public c\<close>, of "[]"]
    by auto
qed

lemma public_const_deduct'[simp]:
  assumes "arity c = 0" "public c"
  shows "M \<turnstile> Fun c []" "M \<turnstile>\<^sub>c Fun c []"
using intruder_deduct.Compose[of "[]" c] intruder_synth.ComposeC[of "[]" c] assms by simp_all

lemma private_fun_deduct_in_ik:
  assumes t: "M \<turnstile> t" "Fun f T \<in> subterms t"
    and f: "\<not>public f"
  shows "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t M"
using t
proof (induction t rule: intruder_deduct.induct)
  case Decompose thus ?case by (meson Ana_subterm psubsetD term.order_trans)
qed (auto simp add: f in_subterms_Union)

lemma private_fun_deduct_in_ik':
  assumes t: "M \<turnstile> Fun f T"
    and f: "\<not>public f"
    and M: "Fun f T \<in> subterms\<^sub>s\<^sub>e\<^sub>t M \<Longrightarrow> Fun f T \<in> M"
  shows "Fun f T \<in> M"
by (rule M[OF private_fun_deduct_in_ik[OF t term.order_refl f]])

lemma pgwt_public: "\<lbrakk>public_ground_wf_term t; Fun f T \<sqsubseteq> t\<rbrakk> \<Longrightarrow> public f"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_ground: "public_ground_wf_term t \<Longrightarrow> fv t = {}"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_fun: "public_ground_wf_term t \<Longrightarrow> \<exists>f T. t = Fun f T"
using pgwt_ground[of t] by (cases t) auto

lemma pgwt_arity: "\<lbrakk>public_ground_wf_term t; Fun f T \<sqsubseteq> t\<rbrakk> \<Longrightarrow> arity f = length T"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_wellformed: "public_ground_wf_term t \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m t"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_deducible: "public_ground_wf_term t \<Longrightarrow> M \<turnstile>\<^sub>c t"
by (induct t rule: public_ground_wf_term.induct) auto

lemma pgwt_is_empty_synth: "public_ground_wf_term t \<longleftrightarrow> {} \<turnstile>\<^sub>c t"
proof -
  { fix M::"('fun,'var) term set" assume "M \<turnstile>\<^sub>c t" "M = {}" hence "public_ground_wf_term t"
      by (induct t rule: intruder_synth.induct) auto
  }
  thus ?thesis using pgwt_deducible by auto
qed

lemma ideduct_synth_subst_apply:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "{} \<turnstile>\<^sub>c t" "\<And>v. M \<turnstile>\<^sub>c \<theta> v"
  shows "M \<turnstile>\<^sub>c t \<cdot> \<theta>"
proof -
  { fix M'::"('fun,'var) term set" assume "M' \<turnstile>\<^sub>c t" "M' = {}" hence "M \<turnstile>\<^sub>c t \<cdot> \<theta>"
    proof (induction t rule: intruder_synth.induct)
      case (ComposeC T f M')
      hence "length (map (\<lambda>t. t \<cdot> \<theta>) T) = arity f" "\<And>x. x \<in> set (map (\<lambda>t. t \<cdot> \<theta>) T) \<Longrightarrow> M \<turnstile>\<^sub>c x"
        by auto
      thus ?case using intruder_synth.ComposeC[of "map (\<lambda>t. t \<cdot> \<theta>) T" f M] \<open>public f\<close> by fastforce
    qed simp
  }
  thus ?thesis using assms by metis
qed

subsection \<open>Lemmata: Monotonicity, deduction private constants, etc.\<close>
context
begin
lemma ideduct_mono:
  "\<lbrakk>M \<turnstile> t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> M' \<turnstile> t"
proof (induction rule: intruder_deduct.induct)
  case (Decompose M t K T t\<^sub>i)
  have "\<forall>k. k \<in> set K \<longrightarrow> M' \<turnstile> k" using Decompose.IH \<open>M \<subseteq> M'\<close> by simp
  moreover have "M' \<turnstile> t" using Decompose.IH \<open>M \<subseteq> M'\<close> by simp
  ultimately show ?case using Decompose.hyps intruder_deduct.Decompose by blast
qed auto

lemma ideduct_synth_mono:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  shows "\<lbrakk>M \<turnstile>\<^sub>c t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> M' \<turnstile>\<^sub>c t"
by (induct rule: intruder_synth.induct) auto

lemma ideduct_reduce:
  "\<lbrakk>M \<union> M' \<turnstile> t; \<And>t'. t' \<in> M' \<Longrightarrow> M \<turnstile> t'\<rbrakk> \<Longrightarrow> M \<turnstile> t"
proof (induction rule: intruder_deduct_induct)
  case Decompose thus ?case using intruder_deduct.Decompose by blast
qed auto

lemma ideduct_synth_reduce:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  shows "\<lbrakk>M \<union> M' \<turnstile>\<^sub>c t; \<And>t'. t' \<in> M' \<Longrightarrow> M \<turnstile>\<^sub>c t'\<rbrakk> \<Longrightarrow> M \<turnstile>\<^sub>c t"
by (induct rule: intruder_synth_induct) auto

lemma ideduct_mono_eq:
  assumes "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile> t" shows "M \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<turnstile> t"
proof
  show "M \<union> N \<turnstile> t \<Longrightarrow> M' \<union> N \<turnstile> t"
  proof (induction t rule: intruder_deduct_induct)
    case (Axiom t) thus ?case
    proof (cases "t \<in> M")
      case True
      hence "M \<turnstile> t" using intruder_deduct.Axiom by metis
      thus ?thesis using assms ideduct_mono[of M' t "M' \<union> N"] by simp
    qed auto
  next
    case (Compose T f) thus ?case using intruder_deduct.Compose by auto
  next
    case (Decompose t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M' \<union> N" t K T] by auto
  qed

  show "M' \<union> N \<turnstile> t \<Longrightarrow> M \<union> N \<turnstile> t"
  proof (induction t rule: intruder_deduct_induct)
    case (Axiom t) thus ?case
    proof (cases "t \<in> M'")
      case True
      hence "M' \<turnstile> t" using intruder_deduct.Axiom by metis
      thus ?thesis using assms ideduct_mono[of M t "M \<union> N"] by simp
    qed auto
  next
    case (Compose T f) thus ?case using intruder_deduct.Compose by auto
  next
    case (Decompose t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose[of "M \<union> N" t K T] by auto
  qed
qed

lemma deduct_synth_subterm:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M \<turnstile>\<^sub>c t" "s \<in> subterms t" "\<forall>m \<in> M. \<forall>s \<in> subterms m. M \<turnstile>\<^sub>c s"
  shows "M \<turnstile>\<^sub>c s"
using assms by (induct t rule: intruder_synth.induct) auto

lemma deduct_if_synth[intro, dest]: "M \<turnstile>\<^sub>c t \<Longrightarrow> M \<turnstile> t"
by (induct rule: intruder_synth.induct) auto

private lemma ideduct_ik_eq: assumes "\<forall>t \<in> M. M' \<turnstile> t" shows "M' \<turnstile> t \<longleftrightarrow> M' \<union> M \<turnstile> t"
by (meson assms ideduct_mono ideduct_reduce sup_ge1)

private lemma synth_if_deduct_empty: "{} \<turnstile> t \<Longrightarrow> {} \<turnstile>\<^sub>c t"
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K M m)
  then obtain f T where "t = Fun f T" "m \<in> set T"
    using Ana_fun_subterm Ana_var by (cases t) fastforce+
  with Decompose.IH(1) show ?case by (induction rule: intruder_synth_induct) auto
qed auto

private lemma ideduct_deduct_synth_mono_eq:
  assumes "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile>\<^sub>c t" "M \<subseteq> M'"
  and "\<forall>t. M' \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<union> D \<turnstile>\<^sub>c t"
  shows "M \<union> N \<turnstile> t \<longleftrightarrow> M' \<union> N \<union> D \<turnstile>\<^sub>c t"
proof -
  have "\<forall>m \<in> M'. M \<turnstile> m" using assms(1) by auto
  hence "\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile> t" by (metis assms(1,2) deduct_if_synth ideduct_reduce sup.absorb2)
  hence "\<forall>t. M' \<union> N \<turnstile> t \<longleftrightarrow> M \<union> N \<turnstile> t" by (meson ideduct_mono_eq)
  thus ?thesis by (meson assms(3))
qed

lemma ideduct_subst: "M \<turnstile> t \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile> t \<cdot> \<delta>"
proof (induction t rule: intruder_deduct_induct)
  case (Compose T f)
  hence "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f" "\<And>t. t \<in> set T \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile> t \<cdot> \<delta>" by auto
  thus ?case using intruder_deduct.Compose[OF _ Compose.hyps(2), of "map (\<lambda>t. t \<cdot> \<delta>) T"] by auto
next
  case (Decompose t K M' m')
  hence "Ana (t \<cdot> \<delta>) = (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>, M' \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
        "\<And>k. k \<in> set (K \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>) \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile> k"
        "m' \<cdot> \<delta> \<in> set (M' \<cdot>\<^sub>l\<^sub>i\<^sub>s\<^sub>t \<delta>)"
    using Ana_subst[OF Decompose.hyps(2)] by fastforce+
  thus ?case using intruder_deduct.Decompose[OF Decompose.IH(1)] by metis
qed simp

lemma ideduct_synth_subst:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term" and \<delta>::"('fun,'var) subst"
  shows "M \<turnstile>\<^sub>c t \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile>\<^sub>c t \<cdot> \<delta>"
proof (induction t rule: intruder_synth_induct)
  case (ComposeC T f)
  hence "length (map (\<lambda>t. t \<cdot> \<delta>) T) = arity f" "\<And>t. t \<in> set T \<Longrightarrow> M \<cdot>\<^sub>s\<^sub>e\<^sub>t \<delta> \<turnstile>\<^sub>c t \<cdot> \<delta>" by auto
  thus ?case using intruder_synth.ComposeC[OF _ ComposeC.hyps(2), of "map (\<lambda>t. t \<cdot> \<delta>) T"] by auto
qed simp

lemma ideduct_vars:
  assumes "M \<turnstile> t"
  shows "fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
using assms
proof (induction t rule: intruder_deduct_induct)
  case (Decompose t K T t\<^sub>i) thus ?case
    using Ana_vars(2) fv_subset by blast
qed auto

lemma ideduct_synth_vars:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M \<turnstile>\<^sub>c t"
  shows "fv t \<subseteq> fv\<^sub>s\<^sub>e\<^sub>t M"
using assms by (induct t rule: intruder_synth_induct) auto

lemma ideduct_synth_priv_fun_in_ik:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M \<turnstile>\<^sub>c t" "f \<in> funs_term t" "\<not>public f"
  shows "f \<in> \<Union>(funs_term ` M)"
using assms by (induct t rule: intruder_synth_induct) auto

lemma ideduct_synth_priv_const_in_ik:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "M \<turnstile>\<^sub>c Fun c []" "\<not>public c"
  shows "Fun c [] \<in> M"
using intruder_synth.cases[OF assms(1)] assms(2) by fast

lemma ideduct_synth_ik_replace:
  fixes M::"('fun,'var) terms" and t::"('fun,'var) term"
  assumes "\<forall>t \<in> M. N \<turnstile>\<^sub>c t"
    and "M \<turnstile>\<^sub>c t"
  shows "N \<turnstile>\<^sub>c t"
using assms(2,1) by (induct t rule: intruder_synth.induct) auto
end

subsection \<open>Lemmata: Analyzed Intruder Knowledge Closure\<close>
lemma deducts_eq_if_analyzed: "analyzed M \<Longrightarrow> M \<turnstile> t \<longleftrightarrow> M \<turnstile>\<^sub>c t"
unfolding analyzed_def by auto

lemma closure_is_superset: "decomp_closure M M' \<Longrightarrow> M \<subseteq> M'"
unfolding decomp_closure_def by force

lemma deduct_if_closure_deduct: "\<lbrakk>M' \<turnstile> t; decomp_closure M M'\<rbrakk> \<Longrightarrow> M \<turnstile> t"
proof (induction t rule: intruder_deduct.induct)
  case (Decompose M' t K T t\<^sub>i)
  thus ?case using intruder_deduct.Decompose[OF _ \<open>Ana t = (K,T)\<close> _ \<open>t\<^sub>i \<in> set T\<close>] by simp
qed (auto simp add: decomp_closure_def)

lemma deduct_if_closure_synth: "\<lbrakk>decomp_closure M M'; M' \<turnstile>\<^sub>c t\<rbrakk> \<Longrightarrow> M \<turnstile> t"
using deduct_if_closure_deduct by blast

lemma decomp_closure_subterms_composable:
  assumes "decomp_closure M M'"
  and "M' \<turnstile>\<^sub>c t'" "M' \<turnstile> t" "t \<sqsubseteq> t'"
  shows "M' \<turnstile>\<^sub>c t"
using \<open>M' \<turnstile>\<^sub>c t'\<close> assms
proof (induction t' rule: intruder_synth.induct)
  case (AxiomC t' M')
  have "M \<turnstile> t" using \<open>M' \<turnstile> t\<close> deduct_if_closure_deduct AxiomC.prems(1) by blast
  moreover
  { have "\<exists>s \<in> M. t' \<sqsubseteq> s" using \<open>t' \<in> M'\<close> AxiomC.prems(1) unfolding decomp_closure_def by blast
    hence "\<exists>s \<in> M. t \<sqsubseteq> s" using \<open>t \<sqsubseteq> t'\<close> term.order_trans by auto
  }
  ultimately have "t \<in> M'" using AxiomC.prems(1) unfolding decomp_closure_def by blast
  thus ?case by simp
next
  case (ComposeC T f M')
  let ?t' = "Fun f T"
  { assume "t = ?t'" have "M' \<turnstile>\<^sub>c t" using \<open>M' \<turnstile>\<^sub>c ?t'\<close> \<open>t = ?t'\<close> by simp }
  moreover
  { assume "t \<noteq> ?t'"
    have "\<exists>x \<in> set T. t \<sqsubseteq> x" using \<open>t \<sqsubseteq> ?t'\<close> \<open>t \<noteq> ?t'\<close> by simp
    hence "M' \<turnstile>\<^sub>c t" using ComposeC.IH ComposeC.prems(1,3) ComposeC.hyps(3) by blast
  }
  ultimately show ?case using cases_simp[of "t = ?t'" "M' \<turnstile>\<^sub>c t"] by simp
qed

lemma decomp_closure_analyzed:
  assumes "decomp_closure M M'"
  shows "analyzed M'"
proof -
  { fix t assume "M' \<turnstile> t" have "M' \<turnstile>\<^sub>c t" using \<open>M' \<turnstile> t\<close> assms
    proof (induction t rule: intruder_deduct.induct)
      case (Decompose M' t K T t\<^sub>i)
      hence "M' \<turnstile> t\<^sub>i" using Decompose.hyps intruder_deduct.Decompose by blast
      moreover have "t\<^sub>i \<sqsubseteq> t"
        using Decompose.hyps(4) Ana_subterm[OF Decompose.hyps(2)] by blast
      moreover have "M' \<turnstile>\<^sub>c t" using Decompose.IH(1) Decompose.prems by blast
      ultimately show "M' \<turnstile>\<^sub>c t\<^sub>i" using decomp_closure_subterms_composable Decompose.prems by blast
    qed auto
  }
  moreover have "\<forall>t. M \<turnstile>\<^sub>c t \<longrightarrow> M \<turnstile> t" by auto
  ultimately show ?thesis by (auto simp add: decomp_closure_def analyzed_def)
qed

lemma analyzed_if_all_analyzed_in:
  assumes M: "\<forall>t \<in> M. analyzed_in t M"
  shows "analyzed M"
proof (unfold analyzed_def, intro allI iffI)
  fix t
  assume t: "M \<turnstile> t"
  thus "M \<turnstile>\<^sub>c t"
  proof (induction t rule: intruder_deduct_induct)
    case (Decompose t K T t\<^sub>i)
    { assume "t \<in> M"
      hence ?case
        using M Decompose.IH(2) Decompose.hyps(2,4)
        unfolding analyzed_in_def by fastforce
    } moreover {
      fix f S assume "t = Fun f S" "\<And>s. s \<in> set S \<Longrightarrow> M \<turnstile>\<^sub>c s"
      hence ?case using Ana_fun_subterm[of f S] Decompose.hyps(2,4) by blast
    } ultimately show ?case using intruder_synth.cases[OF Decompose.IH(1), of ?case] by blast
  qed simp_all
qed auto

lemma analyzed_is_all_analyzed_in:
  "(\<forall>t \<in> M. analyzed_in t M) \<longleftrightarrow> analyzed M"
proof
  show "analyzed M \<Longrightarrow> \<forall>t \<in> M. analyzed_in t M"
    unfolding analyzed_in_def analyzed_def
    by (auto intro: intruder_deduct.Decompose[OF intruder_deduct.Axiom])
qed (rule analyzed_if_all_analyzed_in)

lemma ik_has_synth_ik_closure:
  fixes M :: "('fun,'var) terms"
  shows "\<exists>M'. (\<forall>t. M \<turnstile> t \<longleftrightarrow> M' \<turnstile>\<^sub>c t) \<and> decomp_closure M M' \<and> (finite M \<longrightarrow> finite M')"
proof -
  let ?M' = "{t. M \<turnstile> t \<and> (\<exists>t' \<in> M. t \<sqsubseteq> t')}"

  have M'_closes: "decomp_closure M ?M'" unfolding decomp_closure_def by simp
  hence "M \<subseteq> ?M'" using closure_is_superset by simp

  have "\<forall>t. ?M' \<turnstile>\<^sub>c t \<longrightarrow> M \<turnstile> t" using deduct_if_closure_synth[OF M'_closes] by blast
  moreover have "\<forall>t. M \<turnstile> t \<longrightarrow> ?M' \<turnstile> t" using ideduct_mono[OF _ \<open>M \<subseteq> ?M'\<close>] by simp
  moreover have "analyzed ?M'" using decomp_closure_analyzed[OF M'_closes] .
  ultimately have "\<forall>t. M \<turnstile> t \<longleftrightarrow> ?M' \<turnstile>\<^sub>c t" unfolding analyzed_def by blast
  moreover have "finite M \<longrightarrow> finite ?M'" by auto
  ultimately show ?thesis using M'_closes by blast
qed

subsection \<open>Intruder Variants: Numbered and Composition-Restricted Intruder Deduction Relations\<close>
text \<open>
  A variant of the intruder relation which restricts composition to only those terms that satisfy
  a given predicate Q.
\<close>
inductive intruder_deduct_restricted::
  "('fun,'var) terms \<Rightarrow> (('fun,'var) term \<Rightarrow> bool) \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
  ("\<langle>_;_\<rangle> \<turnstile>\<^sub>r _" 50)
where
  AxiomR[simp]:   "t \<in> M \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t"
| ComposeR[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t; Q (Fun f T)\<rbrakk>
                    \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r Fun f T"
| DecomposeR:     "\<lbrakk>\<langle>M; Q\<rangle> \<turnstile>\<^sub>r t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r k; t\<^sub>i \<in> set T\<rbrakk>
                    \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t\<^sub>i"

text \<open>
  A variant of the intruder relation equipped with a number representing the heigth of the
  derivation tree (i.e., \<open>\<langle>M; k\<rangle> \<turnstile>\<^sub>n t\<close> iff k is the maximum number of applications of the compose
  an decompose rules in any path of the derivation tree for \<open>M \<turnstile> t\<close>).
\<close>
inductive intruder_deduct_num::
  "('fun,'var) terms \<Rightarrow> nat \<Rightarrow> ('fun,'var) term \<Rightarrow> bool"
  ("\<langle>_; _\<rangle> \<turnstile>\<^sub>n _" 50)
where
  AxiomN[simp]:   "t \<in> M \<Longrightarrow> \<langle>M; 0\<rangle> \<turnstile>\<^sub>n t"
| ComposeN[simp]: "\<lbrakk>length T = arity f; public f; \<And>t. t \<in> set T \<Longrightarrow> \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t\<rbrakk>
                    \<Longrightarrow> \<langle>M; Suc (Max (insert 0 (steps ` set T)))\<rangle> \<turnstile>\<^sub>n Fun f T"
| DecomposeN:     "\<lbrakk>\<langle>M; n\<rangle> \<turnstile>\<^sub>n t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; steps k\<rangle> \<turnstile>\<^sub>n k; t\<^sub>i \<in> set T\<rbrakk>
                    \<Longrightarrow> \<langle>M; Suc (Max (insert n (steps ` set K)))\<rangle> \<turnstile>\<^sub>n t\<^sub>i"

lemma intruder_deduct_restricted_induct[consumes 1, case_names AxiomR ComposeR DecomposeR]:
  assumes "\<langle>M; Q\<rangle> \<turnstile>\<^sub>r t" "\<And>t. t \<in> M \<Longrightarrow> P M Q t"
          "\<And>T f. \<lbrakk>length T = arity f; public f;
                  \<And>t. t \<in> set T \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r t;
                  \<And>t. t \<in> set T \<Longrightarrow> P M Q t; Q (Fun f T)
                  \<rbrakk> \<Longrightarrow> P M Q (Fun f T)"
          "\<And>t K T t\<^sub>i. \<lbrakk>\<langle>M; Q\<rangle> \<turnstile>\<^sub>r t; P M Q t; Ana t = (K, T); \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; Q\<rangle> \<turnstile>\<^sub>r k;
                       \<And>k. k \<in> set K \<Longrightarrow> P M Q k; t\<^sub>i \<in> set T\<rbrakk> \<Longrightarrow> P M Q t\<^sub>i"
  shows "P M Q t"
using assms by (induct t rule: intruder_deduct_restricted.induct) blast+

lemma intruder_deduct_num_induct[consumes 1, case_names AxiomN ComposeN DecomposeN]:
  assumes "\<langle>M; n\<rangle> \<turnstile>\<^sub>n t" "\<And>t. t \<in> M \<Longrightarrow> P M 0 t"
          "\<And>T f steps.
              \<lbrakk>length T = arity f; public f;
               \<And>t. t \<in> set T \<Longrightarrow> \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t;
               \<And>t. t \<in> set T \<Longrightarrow> P M (steps t) t\<rbrakk>
              \<Longrightarrow> P M (Suc (Max (insert 0 (steps ` set T)))) (Fun f T)"
          "\<And>t K T t\<^sub>i steps n.
              \<lbrakk>\<langle>M; n\<rangle> \<turnstile>\<^sub>n t; P M n t; Ana t = (K, T);
               \<And>k. k \<in> set K \<Longrightarrow> \<langle>M; steps k\<rangle> \<turnstile>\<^sub>n k;
               t\<^sub>i \<in> set T; \<And>k. k \<in> set K \<Longrightarrow> P M (steps k) k\<rbrakk>
              \<Longrightarrow> P M (Suc (Max (insert n (steps ` set K)))) t\<^sub>i"
  shows "P M n t"
using assms by (induct rule: intruder_deduct_num.induct) blast+

lemma ideduct_restricted_mono:
  "\<lbrakk>\<langle>M; P\<rangle> \<turnstile>\<^sub>r t; M \<subseteq> M'\<rbrakk> \<Longrightarrow> \<langle>M'; P\<rangle> \<turnstile>\<^sub>r t"
proof (induction rule: intruder_deduct_restricted_induct)
  case (DecomposeR t K T t\<^sub>i)
  have "\<forall>k. k \<in> set K \<longrightarrow> \<langle>M'; P\<rangle> \<turnstile>\<^sub>r k" using DecomposeR.IH \<open>M \<subseteq> M'\<close> by simp
  moreover have "\<langle>M'; P\<rangle> \<turnstile>\<^sub>r t" using DecomposeR.IH \<open>M \<subseteq> M'\<close> by simp
  ultimately show ?case
    using DecomposeR
          intruder_deduct_restricted.DecomposeR[OF _ DecomposeR.hyps(2) _ DecomposeR.hyps(4)]
    by blast
qed auto

subsection \<open>Lemmata: Intruder Deduction Equivalences\<close>
lemma deduct_if_restricted_deduct: "\<langle>M;P\<rangle> \<turnstile>\<^sub>r m \<Longrightarrow> M \<turnstile> m"
proof (induction m rule: intruder_deduct_restricted_induct)
  case (DecomposeR t K T t\<^sub>i) thus ?case using intruder_deduct.Decompose by blast
qed simp_all

lemma restricted_deduct_if_restricted_ik:
  assumes "\<langle>M;P\<rangle> \<turnstile>\<^sub>r m" "\<forall>m \<in> M. P m"
  and P: "\<forall>t t'. P t \<longrightarrow> t' \<sqsubseteq> t \<longrightarrow> P t'"
  shows "P m"
using assms(1)
proof (induction m rule: intruder_deduct_restricted_induct)
  case (DecomposeR t K T t\<^sub>i)
  obtain f S where "t = Fun f S" using Ana_var \<open>t\<^sub>i \<in> set T\<close> \<open>Ana t = (K, T)\<close> by (cases t) auto
  thus ?case using DecomposeR assms(2) P Ana_subterm by blast
qed (simp_all add: assms(2))

lemma deduct_restricted_if_synth:
  assumes P: "P m" "\<forall>t t'. P t \<longrightarrow> t' \<sqsubseteq> t \<longrightarrow> P t'"
  and m: "M \<turnstile>\<^sub>c m"
  shows "\<langle>M; P\<rangle> \<turnstile>\<^sub>r m"
using m P(1)
proof (induction m rule: intruder_synth_induct)
  case (ComposeC T f)
  hence "\<langle>M; P\<rangle> \<turnstile>\<^sub>r t" when t: "t \<in> set T" for t
    using t P(2) subtermeqI''[of _ T f]
    by fastforce
  thus ?case
    using intruder_deduct_restricted.ComposeR[OF ComposeC.hyps(1,2)] ComposeC.prems(1)
    by metis
qed simp

lemma deduct_zero_in_ik:
  assumes "\<langle>M; 0\<rangle> \<turnstile>\<^sub>n t" shows "t \<in> M"
proof -
  { fix k assume "\<langle>M; k\<rangle> \<turnstile>\<^sub>n t" hence "k > 0 \<or> t \<in> M" by (induct t) auto
  } thus ?thesis using assms by auto
qed

lemma deduct_if_deduct_num: "\<langle>M; k\<rangle> \<turnstile>\<^sub>n t \<Longrightarrow> M \<turnstile> t"
by (induct t rule: intruder_deduct_num.induct)
   (metis intruder_deduct.Axiom,
    metis intruder_deduct.Compose,
    metis intruder_deduct.Decompose)

lemma deduct_num_if_deduct: "M \<turnstile> t \<Longrightarrow> \<exists>k. \<langle>M; k\<rangle> \<turnstile>\<^sub>n t"
proof (induction t rule: intruder_deduct_induct)
  case (Compose T f)
  then obtain steps where *: "\<forall>t \<in> set T. \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t" by moura
  then obtain n where "\<forall>t \<in> set T. steps t \<le> n"
    using finite_nat_set_iff_bounded_le[of "steps ` set T"]
    by auto
  thus ?case using ComposeN[OF Compose.hyps(1,2), of M steps] * by force
next
  case (Decompose t K T t\<^sub>i)
  hence "\<And>u. u \<in> insert t (set K) \<Longrightarrow> \<exists>k. \<langle>M; k\<rangle> \<turnstile>\<^sub>n u" by auto
  then obtain steps where *: "\<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t" "\<forall>t \<in> set K. \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t" by moura
  then obtain n where "steps t \<le> n" "\<forall>t \<in> set K. steps t \<le> n"
    using finite_nat_set_iff_bounded_le[of "steps ` insert t (set K)"]
    by auto
  thus ?case using DecomposeN[OF _ Decompose.hyps(2) _ Decompose.hyps(4), of M _ steps] * by force
qed (metis AxiomN)

lemma deduct_normalize:
  assumes M: "\<forall>m \<in> M. \<forall>f T. Fun f T \<sqsubseteq> m \<longrightarrow> P f T"
  and t: "\<langle>M; k\<rangle> \<turnstile>\<^sub>n t" "Fun f T \<sqsubseteq> t" "\<not>P f T"
  shows "\<exists>l \<le> k. (\<langle>M; l\<rangle> \<turnstile>\<^sub>n Fun f T) \<and> (\<forall>t \<in> set T. \<exists>j < l. \<langle>M; j\<rangle> \<turnstile>\<^sub>n t)"
using t
proof (induction t rule: intruder_deduct_num_induct)
  case (AxiomN t) thus ?case using M by auto
next
  case (ComposeN T' f' steps) thus ?case
  proof (cases "Fun f' T' = Fun f T")
    case True
    hence "\<langle>M; Suc (Max (insert 0 (steps ` set T')))\<rangle> \<turnstile>\<^sub>n Fun f T" "T = T'"
      using intruder_deduct_num.ComposeN[OF ComposeN.hyps] by auto
    moreover have "\<And>t. t \<in> set T \<Longrightarrow> \<langle>M; steps t\<rangle> \<turnstile>\<^sub>n t"
      using True ComposeN.hyps(3) by auto
    moreover have "\<And>t. t \<in> set T \<Longrightarrow> steps t < Suc (Max (insert 0 (steps ` set T)))"
      using Max_less_iff[of "insert 0 (steps ` set T)" "Suc (Max (insert 0 (steps ` set T)))"]
      by auto
    ultimately show ?thesis by auto
  next
    case False
    then obtain t' where t': "t' \<in> set T'" "Fun f T \<sqsubseteq> t'" using ComposeN by auto
    hence "\<exists>l \<le> steps t'. (\<langle>M; l\<rangle> \<turnstile>\<^sub>n Fun f T) \<and> (\<forall>t \<in> set T. \<exists>j < l. \<langle>M; j\<rangle> \<turnstile>\<^sub>n t)"
      using ComposeN.IH[OF _ _ ComposeN.prems(2)] by auto
    moreover have "steps t' < Suc (Max (insert 0 (steps ` set T')))"
      using Max_less_iff[of "insert 0 (steps ` set T')" "Suc (Max (insert 0 (steps ` set T')))"]
      using t'(1) by auto
    ultimately show ?thesis using ComposeN.hyps(3)[OF t'(1)]
      by (meson Suc_le_eq le_Suc_eq le_trans)
  qed
next
  case (DecomposeN t K T' t\<^sub>i steps n)
  hence *: "Fun f T \<sqsubseteq> t"
    using term.order_trans[of "Fun f T" t\<^sub>i t] Ana_subterm[of t K T']
    by blast
  have "\<exists>l \<le> n. (\<langle>M; l\<rangle> \<turnstile>\<^sub>n Fun f T) \<and> (\<forall>t' \<in> set T. \<exists>j < l. \<langle>M; j\<rangle> \<turnstile>\<^sub>n t')"
    using DecomposeN.IH(1)[OF * DecomposeN.prems(2)] by auto
  moreover have "n < Suc (Max (insert n (steps ` set K)))"
      using Max_less_iff[of "insert n (steps ` set K)" "Suc (Max (insert n (steps ` set K)))"]
      by auto
  ultimately show ?case using DecomposeN.hyps(4) by (meson Suc_le_eq le_Suc_eq le_trans)
qed

lemma deduct_inv:
  assumes "\<langle>M; n\<rangle> \<turnstile>\<^sub>n t"
  shows "t \<in> M \<or>
         (\<exists>f T. t = Fun f T \<and> public f \<and> length T = arity f \<and> (\<forall>t \<in> set T. \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n t)) \<or>
         (\<exists>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M.
            (\<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n m) \<and> (\<forall>k \<in> set (fst (Ana m)). \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n k) \<and>
            t \<in> set (snd (Ana m)))"
    (is "?P t n \<or> ?Q t n \<or> ?R t n")
using assms
proof (induction n arbitrary: t rule: nat_less_induct)
  case (1 n t) thus ?case
  proof (cases n)
    case 0
    hence "t \<in> M" using deduct_zero_in_ik "1.prems"(1) by metis
    thus ?thesis by auto
  next
    case (Suc n')
    hence "\<langle>M; Suc n'\<rangle> \<turnstile>\<^sub>n t"
          "\<forall>m < Suc n'. \<forall>x. (\<langle>M; m\<rangle> \<turnstile>\<^sub>n x) \<longrightarrow> ?P x m \<or> ?Q x m \<or> ?R x m"
      using "1.prems" "1.IH" by blast+
    hence "?P t (Suc n') \<or> ?Q t (Suc n') \<or> ?R t (Suc n')"
    proof (induction t rule: intruder_deduct_num_induct)
      case (AxiomN t) thus ?case by simp
    next
      case (ComposeN T f steps)
      have "\<And>t. t \<in> set T \<Longrightarrow> steps t < Suc (Max (insert 0 (steps ` set T)))"
          using Max_less_iff[of "insert 0 (steps ` set T)" "Suc (Max (insert 0 (steps ` set T)))"]
          by auto
      thus ?case using ComposeN.hyps by metis
    next
      case (DecomposeN t K T t\<^sub>i steps n)
      have 0: "n < Suc (Max (insert n (steps ` set K)))"
              "\<And>k. k \<in> set K \<Longrightarrow> steps k < Suc (Max (insert n (steps ` set K)))"
        using Max_less_iff[of "insert n (steps ` set K)" "Suc (Max (insert n (steps ` set K)))"]
        by auto

      have IH1: "?P t j \<or> ?Q t j \<or> ?R t j" when jt: "j < n" "\<langle>M; j\<rangle> \<turnstile>\<^sub>n t" for j t
        using jt DecomposeN.prems(1) 0(1)
        by simp

      have IH2: "?P t n \<or> ?Q t n \<or> ?R t n"
        using DecomposeN.IH(1) IH1
        by simp

      have 1: "\<forall>k \<in> set (fst (Ana t)). \<exists>l < Suc (Max (insert n (steps ` set K))). \<langle>M; l\<rangle> \<turnstile>\<^sub>n k"
        using DecomposeN.hyps(1,2,3) 0(2)
        by auto

      have 2: "t\<^sub>i \<in> set (snd (Ana t))"
        using DecomposeN.hyps(2,4)
        by fastforce

      have 3: "t \<in> subterms\<^sub>s\<^sub>e\<^sub>t M" when "t \<in> set (snd (Ana m))" "m \<sqsubseteq>\<^sub>s\<^sub>e\<^sub>t M" for m
        using that(1) Ana_subterm[of m _ "snd (Ana m)"] in_subterms_subset_Union[OF that(2)]
        by (metis (no_types, lifting) prod.collapse psubsetD subsetCE subsetD)

      have 4: "?R t\<^sub>i (Suc (Max (insert n (steps ` set K))))" when "?R t n"
        using that 0(1) 1 2 3 DecomposeN.hyps(1)
        by (metis (no_types, lifting))

      have 5: "?R t\<^sub>i (Suc (Max (insert n (steps ` set K))))" when "?P t n"
        using that 0(1) 1 2 DecomposeN.hyps(1)
        by blast

      have 6: ?case when *: "?Q t n"
      proof -
        obtain g S where g:
            "t = Fun g S" "public g" "length S = arity g" "\<forall>t \<in> set S. \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n t"
          using * by moura
        then obtain l where l: "l < n" "\<langle>M; l\<rangle> \<turnstile>\<^sub>n t\<^sub>i"
          using 0(1) DecomposeN.hyps(2,4) Ana_fun_subterm[of g S K T] by blast

        have **: "l < Suc (Max (insert n (steps ` set K)))" using l(1) 0(1) by simp

        show ?thesis using IH1[OF l] less_trans[OF _ **] by fastforce
      qed

      show ?case using IH2 4 5 6 by argo
    qed
    thus ?thesis using Suc by fast
  qed
qed

lemma restricted_deduct_if_deduct:
  assumes M: "\<forall>m \<in> M. \<forall>f T. Fun f T \<sqsubseteq> m \<longrightarrow> P (Fun f T)"
  and P_subterm: "\<forall>f T t. M \<turnstile> Fun f T \<longrightarrow> P (Fun f T) \<longrightarrow> t \<in> set T \<longrightarrow> P t"
  and P_Ana_key: "\<forall>t K T k. M \<turnstile> t \<longrightarrow> P t \<longrightarrow> Ana t = (K, T) \<longrightarrow> M \<turnstile> k \<longrightarrow> k \<in> set K \<longrightarrow> P k"
  and m: "M \<turnstile> m" "P m"
  shows "\<langle>M; P\<rangle> \<turnstile>\<^sub>r m"
proof -
  { fix k assume "\<langle>M; k\<rangle> \<turnstile>\<^sub>n m"
    hence ?thesis using m(2)
    proof (induction k arbitrary: m rule: nat_less_induct)
      case (1 n m) thus ?case
      proof (cases n)
        case 0
        hence "m \<in> M" using deduct_zero_in_ik "1.prems"(1) by metis
        thus ?thesis by auto
      next
        case (Suc n')
        hence "\<langle>M; Suc n'\<rangle> \<turnstile>\<^sub>n m"
              "\<forall>m < Suc n'. \<forall>x. (\<langle>M; m\<rangle> \<turnstile>\<^sub>n x) \<longrightarrow> P x \<longrightarrow> \<langle>M;P\<rangle> \<turnstile>\<^sub>r x"
          using "1.prems" "1.IH" by blast+
        thus ?thesis using "1.prems"(2)
        proof (induction m rule: intruder_deduct_num_induct)
          case (ComposeN T f steps)
          have *: "steps t < Suc (Max (insert 0 (steps ` set T)))" when "t \<in> set T" for t
            using Max_less_iff[of "insert 0 (steps ` set T)"] that
            by blast

          have **: "P t" when "t \<in> set T" for t
            using P_subterm ComposeN.prems(2) that
                  Fun_param_is_subterm[OF that]
                  intruder_deduct.Compose[OF ComposeN.hyps(1,2)]
                  deduct_if_deduct_num[OF ComposeN.hyps(3)]
            by blast

          have "\<langle>M; P\<rangle> \<turnstile>\<^sub>r t" when "t \<in> set T" for t
            using ComposeN.prems(1) ComposeN.hyps(3)[OF that] *[OF that] **[OF that]
            by blast
          thus ?case
            by (metis intruder_deduct_restricted.ComposeR[OF ComposeN.hyps(1,2)] ComposeN.prems(2))
        next
          case (DecomposeN t K T t\<^sub>i steps l)
          show ?case
          proof (cases "P t")
            case True
            hence "\<And>k. k \<in> set K \<Longrightarrow> P k"
              using P_Ana_key DecomposeN.hyps(1,2,3) deduct_if_deduct_num
              by blast
            moreover have
                "\<And>k m x. k \<in> set K \<Longrightarrow> m < steps k \<Longrightarrow> \<langle>M; m\<rangle> \<turnstile>\<^sub>n x \<Longrightarrow> P x \<Longrightarrow> \<langle>M;P\<rangle> \<turnstile>\<^sub>r x"
            proof -
              fix k m x assume *: "k \<in> set K" "m < steps k" "\<langle>M; m\<rangle> \<turnstile>\<^sub>n x" "P x"
              have "steps k \<in> insert l (steps ` set K)" using *(1) by simp
              hence "m < Suc (Max (insert l (steps ` set K)))"
                using less_trans[OF *(2), of "Suc (Max (insert l (steps ` set K)))"]
                      Max_less_iff[of "insert l (steps ` set K)"
                                      "Suc (Max (insert l (steps ` set K)))"]
                by auto
              thus "\<langle>M;P\<rangle> \<turnstile>\<^sub>r x" using DecomposeN.prems(1) *(3,4) by simp
            qed
            ultimately have "\<And>k. k \<in> set K \<Longrightarrow> \<langle>M; P\<rangle> \<turnstile>\<^sub>r k"
              using DecomposeN.IH(2) by auto
            moreover have "\<langle>M; P\<rangle> \<turnstile>\<^sub>r t"
              using True DecomposeN.prems(1) DecomposeN.hyps(1) le_imp_less_Suc
                    Max_less_iff[of "insert l (steps ` set K)" "Suc (Max (insert l (steps ` set K)))"]
              by blast
            ultimately show ?thesis
              using intruder_deduct_restricted.DecomposeR[OF _ DecomposeN.hyps(2)
                                                             _ DecomposeN.hyps(4)]
              by metis
          next
            case False
            obtain g S where gS: "t = Fun g S" using DecomposeN.hyps(2,4) by (cases t) moura+
            hence *: "Fun g S \<sqsubseteq> t" "\<not>P (Fun g S)" using False by force+
            have "\<exists>j<l. \<langle>M; j\<rangle> \<turnstile>\<^sub>n t\<^sub>i"
              using gS DecomposeN.hyps(2,4) Ana_fun_subterm[of g S K T]
                    deduct_normalize[of M "\<lambda>f T. P (Fun f T)", OF M DecomposeN.hyps(1) *]
              by force
            hence "\<exists>j<Suc (Max (insert l (steps ` set K))). \<langle>M; j\<rangle> \<turnstile>\<^sub>n t\<^sub>i"
              using Max_less_iff[of "insert l (steps ` set K)"
                                    "Suc (Max (insert l (steps ` set K)))"]
                    less_trans[of _ l "Suc (Max (insert l (steps ` set K)))"]
              by blast
            thus ?thesis using DecomposeN.prems(1,2) by meson
          qed
        qed auto
      qed
    qed
  } thus ?thesis using deduct_num_if_deduct m(1) by metis
qed

lemma restricted_deduct_if_deduct':
  assumes "\<forall>m \<in> M. P m"
    and "\<forall>t t'. P t \<longrightarrow> t' \<sqsubseteq> t \<longrightarrow> P t'"
    and "\<forall>t K T k. P t \<longrightarrow> Ana t = (K, T) \<longrightarrow> k \<in> set K \<longrightarrow> P k"
    and "M \<turnstile> m" "P m"
  shows "\<langle>M; P\<rangle> \<turnstile>\<^sub>r m"
using restricted_deduct_if_deduct[of M P m] assms
by blast

lemma private_const_deduct:
  assumes c: "\<not>public c" "M \<turnstile> (Fun c []::('fun,'var) term)"
  shows "Fun c [] \<in> M \<or>
         (\<exists>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. M \<turnstile> m \<and> (\<forall>k \<in> set (fst (Ana m)). M \<turnstile> m) \<and>
                             Fun c [] \<in> set (snd (Ana m)))"
proof -
  obtain n where "\<langle>M; n\<rangle> \<turnstile>\<^sub>n Fun c []"
    using c(2) deduct_num_if_deduct by moura
  hence "Fun c [] \<in> M \<or>
         (\<exists>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M.
            (\<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n m) \<and>
            (\<forall>k \<in> set (fst (Ana m)). \<exists>l < n. \<langle>M; l\<rangle> \<turnstile>\<^sub>n k) \<and> Fun c [] \<in> set (snd (Ana m)))"
    using deduct_inv[of M n "Fun c []"] c(1) by fast
  thus ?thesis using deduct_if_deduct_num[of M] by blast
qed

lemma private_fun_deduct_in_ik'':
  assumes t: "M \<turnstile> Fun f T" "Fun c [] \<in> set T" "\<forall>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. Fun f T \<notin> set (snd (Ana m))"
    and c: "\<not>public c" "Fun c [] \<notin> M" "\<forall>m \<in> subterms\<^sub>s\<^sub>e\<^sub>t M. Fun c [] \<notin> set (snd (Ana m))"
  shows "Fun f T \<in> M"
proof -
  have *: "\<nexists>n. \<langle>M; n\<rangle> \<turnstile>\<^sub>n Fun c []"
    using private_const_deduct[OF c(1)] c(2,3) deduct_if_deduct_num
    by blast

  obtain n where n: "\<langle>M; n\<rangle> \<turnstile>\<^sub>n Fun f T"
    using t(1) deduct_num_if_deduct
    by blast

  show ?thesis
    using deduct_inv[OF n] t(2,3) *
    by blast
qed

end

subsection \<open>Executable Definitions for Code Generation\<close>
fun intruder_synth' where
  "intruder_synth' pu ar M (Var x) = (Var x \<in> M)"
| "intruder_synth' pu ar M (Fun f T) = (
    Fun f T \<in> M \<or> (pu f \<and> length T = ar f \<and> list_all (intruder_synth' pu ar M) T))"

definition "wf\<^sub>t\<^sub>r\<^sub>m' ar t \<equiv> (\<forall>s \<in> subterms t. is_Fun s \<longrightarrow> ar (the_Fun s) = length (args s))"

definition "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s' ar M \<equiv> (\<forall>t \<in> M. wf\<^sub>t\<^sub>r\<^sub>m' ar t)"

definition "analyzed_in' An pu ar t M \<equiv> (case An t of
    (K,T) \<Rightarrow> (\<forall>k \<in> set K. intruder_synth' pu ar M k) \<longrightarrow> (\<forall>s \<in> set T. intruder_synth' pu ar M s))"

lemma (in intruder_model) intruder_synth'_induct[consumes 1, case_names Var Fun]:
  assumes "intruder_synth' public arity M t"
          "\<And>x. intruder_synth' public arity M (Var x) \<Longrightarrow> P (Var x)"
          "\<And>f T. (\<And>z. z \<in> set T \<Longrightarrow> intruder_synth' public arity M z \<Longrightarrow> P z) \<Longrightarrow>
                  intruder_synth' public arity M (Fun f T) \<Longrightarrow> P (Fun f T) "
  shows "P t"
using assms by (induct public arity M t rule: intruder_synth'.induct) auto

lemma (in intruder_model) wf\<^sub>t\<^sub>r\<^sub>m_code[code_unfold]:
  "wf\<^sub>t\<^sub>r\<^sub>m t = wf\<^sub>t\<^sub>r\<^sub>m' arity t"
unfolding wf\<^sub>t\<^sub>r\<^sub>m_def wf\<^sub>t\<^sub>r\<^sub>m'_def
by auto

lemma (in intruder_model) wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s_code[code_unfold]:
  "wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s M = wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s' arity M"
using wf\<^sub>t\<^sub>r\<^sub>m_code
unfolding wf\<^sub>t\<^sub>r\<^sub>m\<^sub>s'_def
by auto

lemma (in intruder_model) intruder_synth_code[code_unfold]:
  "intruder_synth M t = intruder_synth' public arity M t"
  (is "?A \<longleftrightarrow> ?B")
proof
  show "?A \<Longrightarrow> ?B"
  proof (induction t rule: intruder_synth_induct)
    case (AxiomC t) thus ?case by (cases t) auto
  qed (fastforce simp add: list_all_iff)

  show "?B \<Longrightarrow> ?A"
  proof (induction t rule: intruder_synth'_induct)
    case (Fun f T) thus ?case
    proof (cases "Fun f T \<in> M")
      case False
      hence "public f" "length T = arity f" "list_all (intruder_synth' public arity M) T"
        using Fun.hyps by fastforce+
      thus ?thesis
        using Fun.IH intruder_synth.ComposeC[of T f M] Ball_set[of T]
        by blast
    qed simp
  qed simp
qed

lemma (in intruder_model) analyzed_in_code[code_unfold]:
  "analyzed_in t M = analyzed_in' Ana public arity t M"
using intruder_synth_code[of M]
unfolding analyzed_in_def analyzed_in'_def
by fastforce

end

subset_name: curated


TITLE: From Tilings To Groups
QUESTION [2 upvotes]: I am studying (on my own) some random group theory, and using this primer. The book focuses on finitely presented groups, and the main definition of a hyperbolic group there is "word-hyperbolic", meaning: given a word $w$ representing the trivial element in the group, the minimal number of relators needed to write $w$ is bounded by some constant times its length $|w|$ (see page 18).
In page 20 the author explains the connection between tilings and groups, but he does so very informally. Specifically, he says that the hyperbolic group $\langle a,b,c,d \mid aba^{-1}b^{-1} cdc^{-1}d^{-1} \rangle$ corresponds to octagon tiling of the hyperbolic plane (tiles correspond to the relation), and that because there's a tiling of the Euclidean plane with hexagons, there's a group which satisfies the $C'(1/6+\varepsilon)$ condition without being hyperbolic.
I understand the intuition - the area of hexagon tiling grows linearly while the perimeter quadratically, and in hyperbolic octagon they both grow at the same rate. Still, the correspondence lacks "explicitation" for me.
My questions are:

Can we generally construct hyperbolic (resp. non-hyperbolic) groups from tiling of hyperbolic (resp. non-hyperbolic) space?
My first guess would be to take the symmetry group of a tiling, but will it Cayley graph be really similar to the tiling? Will it be hyperbolic if we started with hyperbolic space?
Suppose I take the group $\langle S \mid R \rangle$ where $R$ is a set of one relation of length 6. When will it necessarily be non-hyperbolic (in the sense of word-hyperbolic)? For example consider $S=\{ abcabc \}$, $S= \{ aba^{-1} cdc^{-1}\}$ or $S= \{abc a^{-1} b^{-1} c^{-1} \}$. (EDIT: I'm pretty confident that the last example is indeed non-hyperbolic, since I chose the generator to give a valid tiling)

REPLY [2 votes]: Hyperbolicity, as I understand it, is a property of a finitely presented group that only depends on its Cayley graph as a metric space up to quasi-isometry. Consequently, you can study it by studying any metric space quasi-isometric to the Cayley graph. An important theorem is that if $M$ is a closed Riemannian manifold, then $\pi_1(M)$ is quasi-isometric to the universal cover $\widetilde{M}$. In particular, if $M$ is a closed hyperbolic surface, then $\pi_1(M)$ is quasi-isometric to the hyperbolic plane. $\widetilde{M}$ is tiled by copies of $M$ so that's where the tiling comes into play.


TITLE: probability distribution of communities in Stochastic Block Model
QUESTION [0 upvotes]: Consider a simple case of Stochastic Block Model: all nodes in the graph are equally divided into two communities, the probability of edge connection for nodes in the same community is $p$, nodes in different communities $q$. Given a node $v$, consider the random variable $\Delta(v)$: the difference of numbers of neighbors in the two communities. I am wondering how to calculate the probability distribution of $\Delta(v)$.

REPLY [1 votes]: Let $C_1$ and $C_2$ denote those communities. Also let $N_j(v):=\{w\in C_j:w\leftrightarrow v\}$. Assume that $v\in C_1$. Then for $0\le x< |C_1|$ and $0\le y\le |C_2|$,
$$
\mathsf{P}(N_1(v)=x)=\binom{|C_1|-1}{x}p^x(1-p)^{|C_1|-x-1}
$$
and
$$
\mathsf{P}(N_2(v)=y)=\binom{|C_2|}{y}q^y(1-q)^{|C_2|-y}.
$$
Consequently, the distribution of $\Delta(v):=N_1(v)-N_2(v)$ is determined by
$$
\mathsf{P}(\Delta(v)=z)=\sum_{y}\mathsf{P}(N_1(v)=z+y)\mathsf{P}(N_2(v)=y).
$$


TITLE: Are there three variable generalizations of Ramanujans theta function?
QUESTION [1 upvotes]: The Ramanujan theta function $$f(a,b) = \sum_{n \in \mathbb Z} a^{n(n+1)/2} b^{n(n-1)/2}$$ satisfies the following Jacobi triple product identity $f(a,b) = (-a;ab)\_\infty (-b;ab)\_\infty (ab;ab)\_\infty$.
Are there any three variable generalizations which also satisfy identities like that?

REPLY [3 votes]: I do not know what it is for, as any basic hypergeometric summation can be interpretted as a certain multi-variate "Jacobi-like" identity. Probably, the easiest 4-variate example, known in the theory of basic hypergeometric functions as Ramanujan's summation (see, for example, Section 5.2 in the $q$-Bible of Gasper and Rahman), is
$$
\sum_{n\in\mathbb Z}\frac{(a;q) _ n}{(b;q) _ n}\biggl(\frac ca\biggr)^n
=\frac{(q,b/a,c,q/c;q) _ \infty}{(b,q/a,c/a,b/c;q) _ \infty},
$$
where the standard notation $(a;q) _ n=\prod_{k=1}^n(1-aq^{k-1})$ is used (and extending this symbol to the negative $n$ as well). The formula is valid for $|q|<1$ and $|b|<|c|<|a|$. The Jacobi triple product identity can be realised as a limiting case of this summation.


TITLE: Work done against gravity in climbing and partially descending a wall
QUESTION [0 upvotes]: A question I found in a book recently concerned two worms climbing up one side of a wall and back down the other side, such that the worms were each half across the wall (I.e. the lengths on either side of the wall were equal for each worm). To calculate the amount of work done against gravity, it is suggested that this can be done by using the change in height of the worm's centre of gravity, in the equation W = mgh.
My question is: does this imply that negative work can be done against gravity?
My initial instinct would be yes, since the worm starts with a height of the centre of gravity of 0m, which is raised (implying +ve work against gravity) and then lowered again (implying -ve work against gravity).
The second question is: how come the snail doesn't do total work of: the work done to raise half of its mass by the height of the wall + the work done to raise half of its mass to mean height of the trailing half above the wall?
More generally, if I (70kg) climb a ladder of height 1m and then climb back down again, have I done 70g N work against gravity? Or have I done 0N work?

REPLY [0 votes]: does this imply that negative work can be done against gravity?

This isn't a very well-worded questions. Forces do work. This work is independent of what other forces may be acting on the object$^*$. So you should just ask "can this force do negative work?" Whether or not gravity is also acting on the object and whether or not these forces oppose each other is irrelevant. There is no "work against gravity".

More generally, if I (70kg) climb a ladder of height 1m and then climb back down again, have I done 70g N work against gravity? Or have I done 0N work?

Assuming a constant force each time, if you apply $700\ \rm N$ over $1\ \rm m$ in the same direction as your displacement then you do $700\ \rm J$ of work, and if you apply $700\ \rm N$ over $1\ \rm m$ in the opposite direction as your displacement then you do $-700\ \rm J$ of work. Notice how this doesn't depend on what gravity is doing.

$^*$ Of course the other forces as well as the one in question determines the trajectory of the object, but if you know the trajectory then you only need to focus on the force in question to determine the work done by it over the path the object takes.


text:
\begin{definition}[Definition:Subdivision (Graph Theory)/Graph]
A [[Definition:Graph (Graph Theory)|graph]] which has been derived from $G$ by a [[Definition:Sequence|sequence]] of [[Definition:Edge Subdivision|edge subdivision operations]] is called a '''subdivision of $G$'''.
\end{definition}

config: wiki


TITLE: Do intergalactic magnetic fields imply an Open Universe?
QUESTION [26 upvotes]: According to a paper on the arXiv (now published in Phys Rev D), they do. How credible is this result?  The abstract says:

The detection of magnetic fields at high redshifts, and in empty
  intergalactic space, support the idea that cosmic magnetism has a
  primordial origin. Assuming that Maxwellian electromagnetism and
  general relativity hold, and without introducing any `new' physics, we
  show how the observed magnetic fields can easily survive cosmological
  evolution from the inflationary era in a marginally open Friedmann
  universe but fail to do so, by a very wide margin, in a flat or a
  marginally closed universe. Magnetic fields evolve very differently in
  open and closed Friedmann models. The existence of significant
  magnetic fields in the Universe today, that require primordial
  seeding, may therefore provide strong evidence that the Universe is
  marginally open and not marginally closed.

REPLY [1 votes]: A 2013 paper by Shtanov and Sahni (already mentioned by Ben Crowell in the comments) says that the modes grow exponentially in conformal coordinates, and Barrow et al overlooked the fact that the conformal time changes very little during and after inflation.
A 2014 preprint by Tsagas, one of the authors of the original paper, cites Shtanov and Sahni and seems to agree with them and disagree with the original paper. So I think the original paper is wrong.


TITLE: Solve for $x$ in $x\cdot 2^x -8x = 0$
QUESTION [0 upvotes]: $x\cdot 2^x -8x = 0$
I tried:
$$x\cdot 2^x -8x = 0 \Leftrightarrow x\cdot 2^x = 8x \Leftrightarrow 2^x = 8 \Leftrightarrow x = 3$$
But my book says the solution is $x = 0 \lor x = 3$
How do I get the right solution? What did I do wrong?

REPLY [0 votes]: Basically, you are dividing by zero, because x can be zero. Therefore, what you can do is factor out the x to get:
$x(2^x - 8) = 0$
Therefore, either x must equal 0 or $2^x - 8$ must equal 0.
From there, it's pretty simple.


TITLE: interpretation of $\{H,L^2\}$
QUESTION [1 upvotes]: In Hamiltonian mechanics, we show $\{H,L_z\}=0$, which can be interpreted as the conservation of angular momentum around $Oz$. Following the same idea, how can we interprete $\{H,L^2\}$?
Is the interpretation the same (or only similar) as in quantum mechanics for $[H,L_z]$ and $[H,L^2]$?

REPLY [3 votes]: Dear Isaac, yes, $\{H,L^2\}=0$ holds for spherically symmetric Hamiltonians and it means that the magnitude of the angular momentum will be conserved in time. More precisely, the squared magnitude of the angular momentum is conserved but classically, it's the same thing. The time derivative of any observable, whether it's composite or not, is given by its Poisson bracket with the Hamiltonian - all these things are just a classical limit of "commutators" (Poisson bracket) with the corresponding "operators" (observables).
If $\{H,L_x\}=\{H,L_y\}=\{H,L_z\}=0$, then one may also prove $\{H,L^2\}=0$. This is simplest to prove in the quantum mechanical language. If $H$ commutes with $L_z$, it also commutes with $L_z^2$, and similarly it may commute with $L_x^2$ and $L_y^2$ - and with the sum of these three terms which is $L^2$.
The interpretation of classical physics and quantum mechanics is always different but the maths of the Poisson brackets directly reflects the quantum commutators. In quantum mechanics, all these things can only be measured probabilistically and so on; this portion of quantum mechanics is universal.
In the case of the angular momentum, it's useful to talk about $L^2$ and $L_z$ in quantum mechanics - and we usually no longer add $L_x$ or $L_y$. The pair $L^2$ and $L_z$ commutes with each other, $[L^2,L_z]=0$, but commutators such as $[L_x,L_z]$ are not zero but rather $-i\hbar L_y$, and so on.
Also, $L^2$ has eigenvalues which are always a bit greater than the maximum eigenvalue of $L_z^2$: you can't ever rotate a nonzero angular momentum exactly in the $z$-direction. Equivalently, the uncertainty principle always guarantees that $L_x$ and $L_y$ can't be simultaneously zero when $L_z$ is nonzero.
The eigenvalues of $L^2$ are $l(l+1)\hbar^2$ for integer values of $l$ while the eigenvalues of $L_z$ are integers between $-l$ and $+l$, where the latter $l$ is the same $l$ used in the formula for the eigenvalue of $L^2$.


TITLE: Density argument that some large numbers can't be the sum of two squares
QUESTION [0 upvotes]: I have encountered a question stating that density arguments can sometimes be employed to prove certain problems have no solutions. It then asks me to use a density argument to prove that there are not enough perfect squares to write any large number as a sum of two squares.
Now I (as far as I am aware) have not had to work with density arguments before. A search on here showed that we can start by proving something in a dense subset, but since I am working with the natural numbers this doesn't seem to be a possibility.
From intuition we know that as we go through the natural numbers the squares get more and more spaced out, and so up to some number n, the proportion of numbers less than or equal to n that are squares decreases. Am I supposed to try and use something like this?
Any suggestion about where to start, what to try, or even a full explanation would be very helpful.

REPLY [1 votes]: The argument could go roughly as follows:
There are $n^2$ integers between $1$ and $n^2$. For any number in that interval to be the sum of two squares, each square must be one of the $n+1$ sqares $0^2, 1^2, 2^2,\ldots n^2.$
But selecting $2$ of those $n+1$ numbers with possible repetition but not counting order (addition is commutative) yields
$${n+1 \choose 2}+(n+1) = \frac{(n+1)(n+2)}2$$
possible choices, which is less than $n^2$ for big $n$, it's even just "a bit" more than half of $n^2$.
So even if you add all the squares you have, you do not get enough sums that they could be all numbers from $1$ to $n^2$, just a bit more than half of that. That proves that some of those $n^2$ numbers cannot be the sum of $2$ squares.
Since the deficit (numbers that can't be sums of 2 squares) is $n^2-\frac{(n+1)(n+2)}2=\frac12n^2-\frac32n -1$ and thus increasing with $n$, it can't be that only small numbers
are not of this form.
Density arguments are often "coarse", they do not often lead to the best possible bounds (in this case every non-negative integer can be the sum of 4 squares, but some are not the sum of 3 squares). But they can be effective to get some kind of result without going deep into intricacies of a problem.


TITLE: Test the convergence of the series $\sum\limits_nn^p(\sqrt{n+1}-2\sqrt n + \sqrt{n-1})$
QUESTION [4 upvotes]: I am trying to test the convergence of the series
$$\sum_{n=1}^\infty n^p(\sqrt{n+1}-2\sqrt n + \sqrt{n-1})$$
$p$ is a fixed real number.
I tried the ratio test and the integral test without success. Now, I am stuck with the quantity between the round brackets. I have no idea on how to treat it in order to obtain something useful to work with.

REPLY [1 votes]: In essence the problem is to determine the order of
$$\sqrt{n+1}+\sqrt{n-1}-2\sqrt{n}$$
Tring the ususal trick of multiplying by the conjuguate we get
$$\sqrt{n+1}+\sqrt{n-1}-2\sqrt{n}
=\frac{2\sqrt{n^2-1}-2n}{\sqrt{n+1}+\sqrt{n-1}+2\sqrt{n}}$$ then doing the same again we get
$$\sqrt{n+1}+\sqrt{n-1}-2\sqrt{n}
=\frac{-2}{(\sqrt{n+1}+\sqrt{n-1}+2\sqrt{n})(\sqrt{n^2-1}+n)}$$
Now the order of $(\sqrt{n+1}+\sqrt{n-1}+2\sqrt{n})(\sqrt{n^2-1}+n)$ is $n^{\frac{3}{2}}$ as can be easily verified, since
$$\frac{\sqrt{n+1}+\sqrt{n-1}+2\sqrt{n}}{\sqrt{n}}\rightarrow 4$$  and
$$\frac{\sqrt{n^2-1}+n}{n}\rightarrow 2$$
So if we compare our series with the series $\sum n^{p-\frac{3}{2}}$
 we see that we get a finite ratio. Thus the criteria for convergence is
$$p-\frac{3}{2}<-1$$
or $$p<\frac{1}{2}$$


TITLE: Algebraic Proof: Sum of Squares of 3 consecutive odd numbers = 12n+11
QUESTION [0 upvotes]: I was doing a maths mock exam just today, and I found one question of a type I would normally not find difficult - well difficult. I came here due to it being a GCSE level question that I assume most would find ridiculously easy....
The question being: 'Prove that the sum of the squares of any three consecutive odd numbers is always 11 more than a multiple of 12'
So, I write out - being a non-calculator test:
$$
(2n+1)^2+(2n+3)^2+(2n+5)^2
$$
I expand the brackets and expect something nice... I get
$$
(2n+1)^2+(2n+3)^2+(2n+5)^2 = 12n^2+36n+35
$$
Now, I think I know that

11 more than a multiple of 12

Means:
$$
12n+11
$$
But
$$
12n^2+36n+35 \neq 12n+11
$$
I don't know if I'm missing something fundemental here, whether I'm not seeing it, I mean the output does look similar in that 35 is 1 less than 36 in '36n' and there's a 12 there, but they're just not equal? How do? Thanks.

REPLY [0 votes]: $$12n^2+36n+35$$
if you do $35-11$, you get $24$ which is a factor of $12$, allowing everything to be factorised. so $$12n^2+36n+35= 12n^2+36n+24+11
= 12(n^2+36n+2)+11$$
So the number would always have a remainder of $11$ afterwards, because we have already multiplied it by $12$ to make it a multiple of $12$.


TITLE: Intuitive explanation of conditional density function
QUESTION [0 upvotes]: So conditional density is defined this way $f_{X|Y}\left(x,y\right)=\frac{f_{  X,Y }\left(x,y\right)}{f_Y(y)} $.
I was wondering why it was not simply thus $f_{X|Y}\left(x,y\right)= f_{  X,Y }\left(x,Y=y\right)$. In this function we are taking the slice of the function of two variables along the line Y=y,so what we get looks like a pdf for X when Y =y.

REPLY [0 votes]: Heuristically, the conditional density function can be viewed as
\begin{align*}
f_{X|Y}(x\mid y)&=
\frac{d}{dx}\left(\lim_{\delta\rightarrow 0}P(X\le x \mid y \le Y \le y+\delta) \right)\\
&=\frac{d}{dx}\left(\lim_{\delta\rightarrow 0}\frac{P(X\le x,y \le Y \le y+\delta)}{P(y \le Y \le y+\delta)} \right)\\
&=\frac{d}{dx}\left(\lim_{\delta\rightarrow 0}\frac{\int_{-\infty}^x\int_y^{y+\delta} f_{X, Y}(u, v)dudv}{\int_{-\infty}^{\infty}\int_y^{y+\delta} f_{X, Y}(u, v)dudv} \right)\\
&=\lim_{\delta\rightarrow 0}\frac{\int_y^{y+\delta} f_{X, Y}(x, v)dv}{\int_y^{y+\delta} f_Y(v)dv}\\
&=\frac{f_{X, Y}(x, y)}{f_Y(y)}.
\end{align*}
Noe that this intepretaion is still ad-hoc, as it is possible that $P(y \le Y \le y+\delta)=0$, for certain $\delta>0$.
Formally, note that, the condition density is the function $f_{X|Y}(x\mid y)$ such that, for any Borel set $C$,
\begin{align*}
E(1_{X\in C}\mid Y=y) = \int_C f_{X|Y}(x\mid y) dx.
\end{align*}
In addition, note that the conditional expectation $$E(1_{X\in C}\mid Y=y)$$ is also a Borel measurable function such that for any Borel set $B$
\begin{align*}
\int_{Y\in B} 1_{X\in C} dP &= \int_{B}E(1_{X\in C}\mid Y=y) P_Y(dy) \\
&= \int_{B}E(1_{X\in C}\mid Y=y) f_Y(y)dy\\
&= \int_{B}\int_C f_{X|Y}(x\mid y)  f_Y(y) dx dy,\tag{1}
\end{align*}
where $P_Y(dy)$ is the measure generated by the distribution function of $Y$. On the other hand,
\begin{align*}
\int_{Y\in B} 1_{X\in C} dP = \int_{B}\int_C f_{X, Y}(x, y) dx dy.\tag{2}
\end{align*}
Comparing $(1)$ and $(2)$, we see that
\begin{align*}
f_{X|Y}(x\mid y) = \frac{f_{X, Y}(x, y)}{f_Y(y)}.
\end{align*}


TITLE: Representing the $2$-homology classes of a $4$ manifold. Last passage of a Proof
QUESTION [4 upvotes]: I found a few occurrences of the same proof about representability of elements of $H_2(M,\mathbb{Z})$ for $M$ a closed orientable smooth $4$-manifold. All of them stop at the very end claiming that the conclusion is clear. I found an analogue question on MO but even there it's not explained the last passage of the proof.

(from Kirby's Topology of $4$-Manifolds Theorem 1.1 page $20$) There is an isomorphism $$ H^2(M, \mathbb{Z})\cong [M,\mathbb{C}P^{\infty}]$$ so letting $\hat{\alpha}$ being the Poincaré dual of a chosen $\alpha \in H_2(M, \mathbb{Z})$, there is an homotopy class of maps $[f]\colon M \to \mathbb{C}P^{\infty}$ corresponding to $\hat{\alpha}$. By cellular approximation, we can homotopy (a representative of) $f$ in roder to obtain a map $f\colon M \to \mathbb{C}P^2$. Make $f$ smoothly transverse to $\mathbb{C}P^1\subset \mathbb{C}P^2$. Consider $f^{-1}(\mathbb{C}P^1)$, this will be an oriented surface representing $\alpha$.

I'm not able to prove this last statement, everything is pretty much clear. Looking around I didn't find any explanation for this, so I'm wondering if it is a trivial result. The only indication I found is in the linked question where one suggests to sue Pontrjagin-Thom construction for the group $SO(2)$. Needless to say I'm unable to make use of this hint.
Can someone give me an explanation for this last sentence?

REPLY [3 votes]: The reason for this is the following fact:
Theorem: Let $N\to M$ be a submanifold and $[N]$ the homology class it defines in $M$. Then in $M$ the Thom class of the normal bundle is dual to $[N]$. (see e.g. this exercise in Milnor Stasheff)
Use this together with the map $[M,K(G,i)] \to H^i(M;G)$ which is precisely given by pulling back the unique $i$-cohomology class $k$.
Third thing we use is that normal bundles pull back and naturality of characteristic classes.
Now in your notation (let additionally $\tau_\alpha \in H^2M$ and $\tau_k\in H^2\mathbb CP^2$ be the Thom classes of the normal bundles of $f^{-1}(\mathbb CP^1) $ and $\mathbb CP^1$ resp.):
$$
\hat \alpha  =f^*k = f^*(PD(\mathbb CP1)) = f^*(\tau _k) = \tau_\alpha.
$$
Apply PD to this equality and obtain $$\alpha = PD(\hat \alpha)=PD(\tau_\alpha)=[f^{-1}(\mathbb CP^1)]$$.
Sorry for the very confusing notation which already kind of assumes the result.


TITLE: There is no isometry between a sphere and a plane.
QUESTION [4 upvotes]: How can I show that there is no isometry between a sphere and a plane?
Wikipedia defines an isometry as follows:

Let $(M,g)$ and $(M',g')$ be two Riemannian manifolds, and let $f:M\to M'$ be a diffeomorphism. Then $f$ is called an isometry if $g'=f^*g'$, where $f^*g'$ denotes the pullback of the rank $(0,2)$ metric tensor $g'$ by $f$.

However, I have no clue how to apply this definition to solve this problem. Any hint would be greatly appreciated!

REPLY [5 votes]: Imagine you are holding a sheet of paper. This is your plane. Try and fold the sheet if paper into a sphere without creasing or bending the edges. Can you do this? No, isometries preserve curvature. If you try and make a sphere out of a sheet of paper you will have to bend or tear the paper. But we know that a plane and a cylinder are isometric. You can easily wrap the paper around to form a cylinder. There is no bending needed.


TITLE: Showing a free abelian group is generated by its basis
QUESTION [3 upvotes]: I'm following Massey's "Basic Course in Algebraic Topology" and I'm stuck on his section explaining free abelian groups. He seems to be using a definition of free abelian groups that differs from most others' definitions, and then he leaves it to the reader to show that they're the same, but I can't figure out the proof. More specifically:
He defines a free abelian group on an arbitrary set $S$ as an abelian group $F$ together with a function $\phi:S\to F$ such that for any abelian group $A$ and any function $\psi:S\to A$, there exists a unique homomorphism $f:F\to A$ such that $f\circ\phi=\psi$. He shows that free abelian groups over a given set are unique up to isomorphism, and then leaves the following as an exercise:

"Prove directly from the definition that $\phi(S)$ generates $F$.
  [Hint: Assume not; consider the subgroup $F'$ generated by
  $\phi(S)$.]"

I can't figure out this exercise, but it seems really important to understanding this particular definition of free abelian groups. My guess is to let $\langle\phi(S)\rangle$ be $A$ and let $\psi$ be $\phi$ in the above definition, but I can't produce a contradiction.
Thank you for your help.
Edit: I just realized this question is very related to this other question, but I'm not convinced by the responses. The responses show that $\langle\phi(S)\rangle$ is isomorphic to $F$, but that doesn't seem (to me...) to show that they are equal, since $2\mathbb{Z}$ is isomorphic to $\mathbb{Z}$ without being equal.

REPLY [0 votes]: Your goal is to show the inclusion map $i:F'\to F$ is an isomorphism.  As you suggest, take $A=F'$ and $\psi=\phi$. to get a homomorphism $f:F\to F'$ which restricts to the identity on $\phi(S)$.  Since $\phi(S)$ generates $F'$, this implies $f$ is the identity on all of $F'\subseteq F$, i.e. that the composition $fi:F'\to F'$ is the identity.  To conclude that $i$ is an isomorphism, it suffices to show that $if:F\to F$ is the identity.  For this, you want to use the uniqueness part of the universal property of $F$, in the case where $A=F$ and $\psi=\phi$.
(This argument is actually equivalent to Nitrogen's answer--this is just an explicit implementation of the proof that any two groups satisfying the universal property are canonically isomorphic.)


TITLE: Does the speed of sound wave change when the source velocity change?
QUESTION [2 upvotes]: The speed of sound in air is about $740$ miles per hour. Suppose that a police car is sounding its siren and is driving towards you at $60$ miles per hour. At what speed is the sound of the siren approaching you?

My teacher says the answer is $720 \text{ mph}$ - is this correct? Or is the correct answer $800 \text{ mph}$?

REPLY [4 votes]: My teacher says the answer is $720 \text{ mph}$ - is this correct? Or is the correct answer $800 \text{ mph}$?

Neither is correct. The speed of sound in air remains at $740 \text{ mph}$.

The speed of sound in medium is constant and depends only on the type of medium. However, the sound wave frequency will change if the source and listener are moving relative to each other. This is known as the Doppler effect (see figure below)
$$f_L = \frac{v + v_L}{v + v_S} f_S$$
where $f_S$ and $f_L$ are source (emitted) and listener (observed) frequency, $v_S$ and $v_L$ are source and listener speed relative to the medium, and $v$ is sound propagation speed in the medium. You have to be careful with the signs for $v_S$ and $v_L$:

$v_S$ is positive if the source is moving away from the listener, and
$v_L$ is positive if the listener is moving towards the source.

Source: H. D. Young, R. A. Freedman, "University Physics with Modern Physics in SI Units", 15th ed., 2019.

Even if the police car is approaching you at $60 \text{ mph}$ the speed of sound in air remains at $740 \text{ mph}$. However, you will hear the siren at the following frequency
$$f_L = \frac{740 + 0}{740 - 60} f_S \approx 1.1 f_S$$
Since $f_L > f_S$ it means that you hear higher frequency than emitted, i.e. you hear peaks of the police-car siren spaced closer in time than they are emitted. When source is moving away from a stationary listener, the listener hears lower frequency than emitted.


TITLE: How does voltage drop in series connection happen?
QUESTION [1 upvotes]: The fact that the voltage is the same for two elements connected in parallel seems very clear and intuitive.
But when switching to the other related idea, of voltage drop in series connection, I do not quite get it.
It’s clear to me that the voltage will be lower the closer we get to the low potential end of the voltage source.
But it’s not clear that the voltage will drop depending on the resistance (and not on the distance to the source).
Suppose this simple circuit:

The fact is that each resistance will cause a 50 V drop, but I do not understand how this happens. I see the maths coming from the Ohm’s law, but I do not get the idea.
Voltage is caused by a difference in charges (it’s actually called potential difference) and I don’t see a potential difference happening there in the resistances. They are just there making it difficult for the electrons to traverse them.
Also, when everything starts running, does the first resistance on the path (resistor A) get all 100 V until the current reaches the second resistance? Or will it instantaneously get its 50 V without the electrons even knowing/feeling that there is a second resistance?

REPLY [3 votes]: Part 0 - resistors
Yes, resistors make the voltage drop by "locally" slowing down electrons, so that they have to "waste" some energy to overcome the obstacle - that causes the voltage drop. You can think of them as "stairs" in the voltage.
Part one - drop of voltage - resistivity - ideal circuits
The reason is that we idealize the "connections" as being with zero resistance, i.e. two points in the circuit without a resistance in between will have the same voltage. In addition, we assume there is a steady state so that the "initial" flowing of electrons inside the circuit is neglected and we focus on when the system is flowing without changing over time.
It is an idealization.
If you think about it, the fact that the cables have no resistance has to be false, because otherwise short-cutting a circuit (i.e. connecting the two poles of a battery of voltage $V$ without any resistance in between) would lead to a current $I=V/R$ where the resistance $R=0$ so that would result in an infinite current $I=\infty$.
In reality, cables have some resistance $r$. We can model that as a fragment of length $dx$ of a cable of having a resistance $$r=\rho dx$$ that is, $\rho$ is a resistance per unit length. We assume it to be constant.
In this case, if you measure the voltage between two points of the circuit at a distance $L$ without any resistance between it you would measure a distance-dependent voltage drop $$\Delta V = -\rho L I$$ where $I$ is the testing current.
This drop is however in general very small compared to the voltage $V$ of the battery and is usually neglected. It is however sometimes necessary to take it into account!
So, if you have a circuit of length $L_{tot}$ with the battery at $\ell=0$ (where $\ell$ is the length along the circuit), a (point-like) "normal" resistance $R$ at $\ell=\ell_0$ and again the battery at $\ell=L_{tot}$ you would have a voltage drop $V(\ell)$
$$
 V(\ell)=
    \begin{cases}
      -I\rho\ell, & \text{if}\ \ell<\ell_0 \\
      -I\rho\ell-RI, & \ell>=\ell_0
    \end{cases}
$$
which is length-dependent.
Notice that you can always approximate this by an ideal circuit with a resistance $r=\rho L$ in series with the "normal" resistance $R$ - that is of course unless you are actually interested in the spatial value of the voltage $V(\ell)$.
With the same reasoning, you can also, instead of modelling your resistance $R$ as a point-like object, assume it has an extension $L_0$ with a resistance per unit length $r_0=R/L_0$, so that now the voltage depends on where you measure along the resistance with $\Delta V= -r_0 x I$ with $x$ the position along the resistance.
In the circuit you drew, it's like having $\rho=0$ and then two point resistors with a value $R$ which have to provide the needed voltage drop and they "share" it as they are equal. But you could also see it as one big capacitor of total resistance $2R$ and length $2L$ so that it has $\rho_0=(2R)/(2L)$ so that after a distance $L$ (equivalent to one resistor) the voltage drop is $\Delta V_1=(2R/2L)*L*I=R*I$ which is equivalent to one full resistor. Because in your case the current I is $100V/2R$ (total voltage divided by total resistance) and you get
$$\Delta V_1=R*100V/(2R) = 100V/2 = 50V$$
You can also model cables as 3D cylinders with a resistance per unit volume and so on - to learn more: resistivity
Part two - initial times  - sort of
Now we model the circuit at the initial times. To do this properly we would need a capacitor and differential equation, but I guess that would be too advanced now. I will try a different approach.
Assume we have a cable with total resistance $R$ and we split it into $N$ pieces of resistance $r=R/N$. We have a battery and the cables connects the two parts of the battery. At the initial time, everything is at a voltage $V=0$ except the point where the battery is, which has voltage $V$.
At the beginning, the electrons see a small piece of circuit with resistance $r$, the voltage difference is $V$ and emit a current $i_1=V/r$. Now they see another resistor and so emit a current $i_2=V/(2r)$. (This is because they see a resistor $r$ at a voltage $V$ and then follow Ohm's law).
If before the voltage drop across the first resistor was, before, $V_1(0)=i_2*r=V$, as the full "voltage" had to decrease through the first resistor, now the voltage is split between the two resistors, so that the voltage drop across the first one is $V_1(1)=i_2 r=V/(2r) * r= V/2$.
And so on, such that when the electrons have crossed $n$ resistors the voltage drop across the first one is
$$V_1(n)=V/n$$
If the times it take for the electrons to cross a resistor is $\tau$ we now have that $n=t/\tau$ (i.e. after a time $10\tau$ we have crossed $n=10$ resistors) so that
$$V_1(t)=V/n={V\over(t/\tau)}={V\tau\over t}$$ valid for $t<N\tau$, so that over time the voltage across the first resistor decreases. When the time is $T=N\tau$ the circuit reaches equilibrium and we get $V_1(final)=V/N$
At the same time, the current goes from 0 (when we attach the circuit there is no current) to $$i_n=V/(nr)={V\over(t/\tau)r}={V\tau\over nt}$$ which also decreases until the final value of $I=V/(Nr)=V/R$.
So, at time $t=0$ where is a spike in current across the first resistor, which then decreases to a final value as the electrons "explore" the presence of new resistors and fine their average final current. The same holds for the voltage.


TITLE: equation for an hexagon with rounded corners
QUESTION [0 upvotes]: I know a simple equation for a squircle, $x^4+y^4=a^4$

What would be the equation for an hexagon with rounded corners?
In the equation, how can I take in account for the angle of rotation of the hexagon about its center?

REPLY [1 votes]: polar
$$ r = 5 + \frac{1}{5} \cos (6 \theta)   $$
looks very good. You can solve as rectangular using $x = r \cos \theta$ and $y = r \sin \theta$
The 6 is fixed, but you may adjust the ratio of coefficients as you like, for visual effect.