theory Multi_Recs2
imports "../Nominal2"
begin

(* 
  multiple recursive binders - multiple letrecs with multiple 
  clauses for each functions

  example 8 from Peter Sewell's bestiary (originally due
  to James Cheney) 

*)

atom_decl name

nominal_datatype fun_recs: exp =
  Var name
| Unit 
| Pair exp exp
| LetRec l::lrbs e::exp bind (set) "b_lrbs l" in l e
and fnclause =
  K x::name p::pat f::exp bind (set) "b_pat p" in f
and fnclauses =
  S fnclause
| ORs fnclause fnclauses
and lrb =
  Clause fnclauses
and lrbs =
  Single lrb
| More lrb lrbs
and pat =
  PVar name
| PUnit
| PPair pat pat
binder
  b_lrbs :: "lrbs \<Rightarrow> atom set" and
  b_pat :: "pat \<Rightarrow> atom set" and
  b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
  b_fnclause :: "fnclause \<Rightarrow> atom set" and
  b_lrb :: "lrb \<Rightarrow> atom set"
where
  "b_lrbs (Single l) = b_lrb l"
| "b_lrbs (More l ls) = b_lrb l \<union> b_lrbs ls"
| "b_pat (PVar x) = {atom x}"
| "b_pat (PUnit) = {}"
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
| "b_fnclauses (S fc) = (b_fnclause fc)"
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
| "b_lrb (Clause fcs) = (b_fnclauses fcs)"
| "b_fnclause (K x pat exp) = {atom x}"



thm fun_recs.perm_bn_alpha
thm fun_recs.perm_bn_simps
thm fun_recs.bn_finite
thm fun_recs.inducts
thm fun_recs.distinct
thm fun_recs.induct
thm fun_recs.inducts
thm fun_recs.exhaust
thm fun_recs.fv_defs
thm fun_recs.bn_defs
thm fun_recs.perm_simps
thm fun_recs.eq_iff
thm fun_recs.fv_bn_eqvt
thm fun_recs.size_eqvt
thm fun_recs.supports
thm fun_recs.fsupp
thm fun_recs.supp

term alpha_b_fnclause
term alpha_b_fnclauses
term alpha_b_lrb
term alpha_b_lrbs
term alpha_b_pat

term alpha_b_fnclause_raw
term alpha_b_fnclauses_raw
term alpha_b_lrb_raw
term alpha_b_lrbs_raw
term alpha_b_pat_raw

lemma uu1:
  fixes as0::exp  and as1::fnclause
  shows "(\<lambda>x::exp. True) (as0::exp)"
  and   "alpha_b_fnclause as1 (permute_b_fnclause p as1)"
  and   "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)"
  and   "alpha_b_lrb as3 (permute_b_lrb p as3)"
  and   "alpha_b_lrbs as4 (permute_b_lrbs p as4)"
  and   "alpha_b_pat as5 (permute_b_pat p as5)"
apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts)
apply(simp_all)
apply(simp only: fun_recs.perm_bn_simps)
apply(simp only: fun_recs.eq_iff)
apply(simp)
oops


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


end