--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Manual/Term3.thy	Tue Mar 23 08:19:33 2010 +0100
@@ -0,0 +1,55 @@
+theory Term3
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
+begin
+
+atom_decl name
+
+section {*** lets with many assignments ***}
+
+datatype rtrm3 =
+  rVr3 "name"
+| rAp3 "rtrm3" "rtrm3"
+| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"
+| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"
+and rassigns =
+  rANil
+| rACons "name" "rtrm3" "rassigns"
+
+(* to be given by the user *)
+primrec 
+  bv3
+where
+  "bv3 rANil = {}"
+| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"
+
+setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term3.rtrm3") 2 *}
+
+local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term3.rtrm3")
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],
+   [[], [[], [], []]]] *}
+print_theorems
+
+notation
+  alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and
+  alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)
+thm alpha_rtrm3_alpha_rassigns.intros
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}
+thm alpha3_inj
+
+lemma alpha3_eqvt:
+  "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"
+  "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"
+sorry
+
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),
+  (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}
+thm alpha3_equivp
+
+quotient_type
+  trm3 = rtrm3 / alpha_rtrm3
+and
+  assigns = rassigns / alpha_rassigns
+  by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))
+
+end