# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265194057 -3600
# Node ID 3a60a028cfc5a519ea7ee4c6c8fb5f53af1eda8f
# Parent  c1af17982f986f40894da55ee01dd3ef81daa87e
Starting with a let-rec example.

diff -r c1af17982f98 -r 3a60a028cfc5 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 11:21:34 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 11:47:37 2010 +0100
@@ -371,7 +371,7 @@
   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
   shows   "P a rtrma"
-
+sorry
 
 section {*** lets with single assignments ***}
 
@@ -649,5 +649,67 @@
   by (simp_all add: alpha4_equivp alpha4list_equivp)
 
 
+datatype rtrm5 =
+  rVr5 "name"
+| rAp5 "rtrm5" "rtrm5"
+| rLt5 "rlts" "rtrm5"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
+
+primrec
+  bv5
+where
+  "bv5 rLnil = {}"
+| "bv5 (rLcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+primrec
+  rfv_trm5 and rfv_lts
+where
+  "rfv_trm5 (rVr5 n) = {atom n}"
+| "rfv_trm5 (rAp5 t s) = (rfv_trm5 t) \<union> (rfv_trm5 s)"
+| "rfv_trm5 (rLt5 lts t) = (rfv_trm5 t - bv5 lts) \<union> (rfv_lts lts - bv5 lts)"
+| "rfv_lts (rLnil) = {}"
+| "rfv_lts (rLcons n t ltl) = (rfv_trm5 t) \<union> (rfv_lts ltl)"
+
+instantiation
+  rtrm5 and rlts :: pt
+begin
+
+primrec
+  permute_rtrm5 and permute_rlts
+where
+  "permute_rtrm5 pi (rVr5 a) = rVr5 (pi \<bullet> a)"
+| "permute_rtrm5 pi (rAp5 t1 t2) = rAp5 (permute_rtrm5 pi t1) (permute_rtrm5 pi t2)"
+| "permute_rtrm5 pi (rLt5 as t) = rLt5 (permute_rlts pi as) (permute_rtrm5 pi t)"
+| "permute_rlts pi (rLnil) = rLnil"
+| "permute_rlts pi (rLcons n t ls) = rLcons (pi \<bullet> n) (permute_rtrm5 pi t) (permute_rlts pi ls)"
+
+lemma pt_rtrm5_zero:
+  fixes t::rtrm5
+  and   l::rlts
+  shows "0 \<bullet> t = t"
+  and   "0 \<bullet> l = l"
+apply(induct t and l rule: rtrm5_rlts.inducts)
+apply(simp_all)
+done
+
+lemma pt_rtrm5_plus:
+  fixes t::rtrm5
+  and   l::rlts
+  shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
+  and   "((p + q) \<bullet> l) = p \<bullet> (q \<bullet> l)"
+apply(induct t and l rule: rtrm5_rlts.inducts)
+apply(simp_all)
+done
+
+instance
+apply default
+apply(simp_all add: pt_rtrm5_zero pt_rtrm5_plus)
+done
+
 
 end
+
+
+end