theory Foo1
imports "../Nominal2" 
begin

(* 
  Contrived example that has more than one
  binding function for a datatype
*)

atom_decl name

nominal_datatype foo: trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"  bind x in t
| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
and assg =
  As "name" "name" "trm"
binder
  bn1::"assg \<Rightarrow> atom list" and
  bn2::"assg \<Rightarrow> atom list" and
  bn3::"assg \<Rightarrow> atom list"
where
  "bn1 (As x y t) = [atom x]"
| "bn2 (As x y t) = [atom y]"
| "bn3 (As x y t) = [atom x, atom y]"

thm foo.distinct
thm foo.induct
thm foo.inducts
thm foo.exhaust
thm foo.fv_defs
thm foo.bn_defs
thm foo.perm_simps
thm foo.eq_iff
thm foo.fv_bn_eqvt
thm foo.size_eqvt
thm foo.supports
thm foo.fsupp
thm foo.supp
thm foo.fresh

primrec
  permute_bn1_raw
where
  "permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"

primrec
  permute_bn2_raw
where
  "permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t"

primrec
  permute_bn3_raw
where
  "permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t"

quotient_definition
  "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
is
  "permute_bn1_raw"

quotient_definition
  "permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg"
is
  "permute_bn2_raw"

quotient_definition
  "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg"
is
  "permute_bn3_raw"

lemma [quot_respect]: 
  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn1_raw permute_bn1_raw"
  apply simp
  apply clarify
  apply (erule alpha_assg_raw.cases)
  apply simp_all
  apply (rule foo.raw_alpha)
  apply simp_all
  done

lemma [quot_respect]: 
  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn2_raw permute_bn2_raw"
  apply simp
  apply clarify
  apply (erule alpha_assg_raw.cases)
  apply simp_all
  apply (rule foo.raw_alpha)
  apply simp_all
  done

lemma [quot_respect]: 
  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn3_raw permute_bn3_raw"
  apply simp
  apply clarify
  apply (erule alpha_assg_raw.cases)
  apply simp_all
  apply (rule foo.raw_alpha)
  apply simp_all
  done

lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]
lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted]

lemma uu1:
  shows "alpha_bn1 as (permute_bn1 p as)"
apply(induct as rule: foo.inducts(2))
apply(auto)[6]
apply(simp add: permute_bn1)
apply(simp add: foo.eq_iff)
done

lemma uu2:
  shows "alpha_bn2 as (permute_bn2 p as)"
apply(induct as rule: foo.inducts(2))
apply(auto)[6]
apply(simp add: permute_bn2)
apply(simp add: foo.eq_iff)
done

lemma uu3:
  shows "alpha_bn3 as (permute_bn3 p as)"
apply(induct as rule: foo.inducts(2))
apply(auto)[6]
apply(simp add: permute_bn3)
apply(simp add: foo.eq_iff)
done

lemma tt1:
  shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)"
apply(induct as rule: foo.inducts(2))
apply(auto)[6]
apply(simp add: permute_bn1 foo.bn_defs)
apply(simp add: atom_eqvt)
done

lemma tt2:
  shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)"
apply(induct as rule: foo.inducts(2))
apply(auto)[6]
apply(simp add: permute_bn2 foo.bn_defs)
apply(simp add: atom_eqvt)
done

lemma tt3:
  shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)"
apply(induct as rule: foo.inducts(2))
apply(auto)[6]
apply(simp add: permute_bn3 foo.bn_defs)
apply(simp add: atom_eqvt)
done


lemma strong_exhaust1:
  fixes c::"'a::fs"
  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
  and     "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
  and     "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P"
  and     "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P"
  and     "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P"
  shows "P"
apply(rule_tac y="y" in foo.exhaust(1))
apply(rule assms(1))
apply(assumption)
apply(rule assms(2))
apply(assumption)
apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
apply(erule exE)
apply(erule conjE)
apply(rule assms(3))
apply(perm_simp)
apply(assumption)
apply(drule supp_perm_eq[symmetric])
apply(perm_simp)
apply(simp)
apply(rule at_set_avoiding2)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: foo.fresh fresh_star_def)
apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q")
apply(erule exE)
apply(erule conjE)
apply(rule assms(4))
apply(perm_simp add: tt1)
apply(assumption)
apply(drule supp_perm_eq[symmetric])
apply(simp add: foo.eq_iff)
apply(simp add: tt1 uu1)
apply(rule at_set_avoiding2)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: Abs_fresh_star)
apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
apply(erule exE)
apply(erule conjE)
apply(rule assms(5))
apply(simp add: set_eqvt)
apply(simp add: tt2)
apply(simp add: foo.eq_iff)
apply(drule supp_perm_eq[symmetric])
apply(simp)
apply(simp add: tt2 uu2)
apply(rule at_set_avoiding2)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: Abs_fresh_star)
apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn3 assg))) \<sharp>* c \<and> supp ([bn3 assg]lst.trm) \<sharp>* q")
apply(erule exE)
apply(erule conjE)
apply(rule assms(6))
apply(simp add: set_eqvt)
apply(simp add: tt3)
apply(simp add: foo.eq_iff)
apply(drule supp_perm_eq[symmetric])
apply(simp)
apply(simp add: tt3 uu3)
apply(rule at_set_avoiding2)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: finite_supp)
apply(simp add: Abs_fresh_star)
done

lemma strong_exhaust2:
  assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" 
  shows "P"
apply(rule_tac y="as" in foo.exhaust(2))
apply(rule assms(1))
apply(assumption)
done


lemma 
  fixes t::trm
  and   as::assg
  and   c::"'a::fs"
  assumes a1: "\<And>x c. P1 c (Var x)"
  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
  and     a4: "\<And>as t c. \<lbrakk>set (bn1 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let1 as t)"
  and     a5: "\<And>as t c. \<lbrakk>set (bn2 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let2 as t)"
  and     a6: "\<And>as t c. \<lbrakk>set (bn3 as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let3 as t)"
  and     a7: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)"
  shows "P1 c t" "P2 c as"
using assms
apply(induction_schema)
apply(rule_tac y="t" and c="c" in strong_exhaust1)
apply(simp_all)[6]
apply(rule_tac as="as" in strong_exhaust2)
apply(simp)
apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))")
apply(simp_all add: foo.size)
done

end