--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term4.thy	Thu Feb 25 14:14:08 2010 +0100
@@ -0,0 +1,65 @@
+theory Term4
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+section {*** lam with indirect list recursion ***}
+
+datatype rtrm4 =
+  rVr4 "name"
+| rAp4 "rtrm4" "rtrm4 list"
+| rLm4 "name" "rtrm4"  --"bind (name) in (trm)"
+print_theorems
+
+thm rtrm4.recs
+
+(* there cannot be a clause for lists, as *)
+(* permutations are  already defined in Nominal (also functions, options, and so on) *)
+setup {* snd o define_raw_perms ["rtrm4"] ["Term4.rtrm4"] *}
+
+(* "repairing" of the permute function *)
+lemma repaired:
+  fixes ts::"rtrm4 list"
+  shows "permute_rtrm4_list p ts = p \<bullet> ts"
+  apply(induct ts)
+  apply(simp_all)
+  done
+
+thm permute_rtrm4_permute_rtrm4_list.simps
+thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]
+
+local_setup {* snd o define_fv_alpha "Term4.rtrm4" [
+  [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}
+print_theorems
+
+notation
+  alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and
+  alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)
+thm alpha_rtrm4_alpha_rtrm4_list.intros
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}
+thm alpha4_inj
+thm alpha_rtrm4_alpha_rtrm4_list.induct
+
+local_setup {*
+snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct}
+*}
+print_theorems
+
+local_setup {*
+(fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt}, []),
+  build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt))
+*}
+print_theorems
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),
+  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}
+thm alpha4_equivp
+
+quotient_type 
+  qrtrm4 = rtrm4 / alpha_rtrm4 and
+  qrtrm4list = "rtrm4 list" / alpha_rtrm4_list
+  by (simp_all add: alpha4_equivp)
+
+end