theory ExPS8
imports "../Nominal2"
begin

(* example 8 from Peter Sewell's bestiary *)

atom_decl name

declare [[STEPS = 31]]

nominal_datatype fun_pats: exp =
  EVar name
| EUnit 
| EPair exp exp
| ELetRec 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_pats.distinct
thm fun_pats.induct
thm fun_pats.inducts
thm fun_pats.exhaust
thm fun_pats.fv_defs
thm fun_pats.bn_defs
thm fun_pats.perm_simps
thm fun_pats.eq_iff
thm fun_pats.fv_bn_eqvt
thm fun_pats.size_eqvt
thm fun_pats.supports
thm fun_pats.fsupp
thm fun_pats.supp


ML {*
fun add_ss thms =
  HOL_basic_ss addsimps thms

fun symmetric thms = 
  map (fn thm => thm RS @{thm sym}) thms
*}

lemma
  "(fv_exp x = supp x) \<and>
   (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and>
   (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and>
   (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and>
   (fv_lrbs xd = supp xd \<and> fv_b_lrbs xd = supp_rel alpha_b_lrbs xd) \<and>
   (fv_pat xe = supp xe \<and> fv_b_pat xe = supp_rel alpha_b_pat xe)"
apply(rule fun_pats.induct)
apply(tactic {* ALLGOALS (TRY o rtac @{thm conjI})*})
thm fun_pats.inducts
oops


lemma
  "fv_exp x = supp x" and
  "fv_fnclause y = supp y" and
  "fv_fnclauses xb = supp xb" and
  "fv_lrb xc = supp xc" and
  "fv_lrbs xd = supp xd" and
  "fv_pat xe = supp xe" and
  "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and
  "fv_b_pat xe = supp_rel alpha_b_pat xe" and
  "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and 
  "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and
  "fv_b_lrb y = supp_rel alpha_b_lrb y"
apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts)
thm fun_pats.inducts
oops

end