# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265710954 -3600
# Node ID d3946f1a9341e180dd7485f324059a1c8f1f3e90
# Parent  de2d1929899fd01e6ebd9b61dd366a3b64bbab88
Looking at the trm2 example

diff -r de2d1929899f -r d3946f1a9341 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 09 10:48:42 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 09 11:22:34 2010 +0100
@@ -316,91 +316,92 @@
 
 section {*** lets with single assignments ***}
 
-datatype trm2 =
-  Vr2 "name"
-| Ap2 "trm2" "trm2"
-| Lm2 "name" "trm2"
-| Lt2 "assign" "trm2"
-and assign =
-  As "name" "trm2"
+datatype rtrm2 =
+  rVr2 "name"
+| rAp2 "rtrm2" "rtrm2"
+| rLm2 "name" "rtrm2"
+| rLt2 "rassign" "rtrm2"
+and rassign =
+  rAs "name" "rtrm2"
 
 (* to be given by the user *)
 primrec 
-  bv2
+  rbv2
 where
-  "bv2 (As x t) = {atom x}"
+  "rbv2 (rAs x t) = {atom x}"
 
 (* needs to be calculated by the package *)
 primrec
-  fv_trm2 and fv_assign
+  fv_rtrm2 and fv_rassign
 where
-  "fv_trm2 (Vr2 x) = {atom x}"
-| "fv_trm2 (Ap2 t1 t2) = (fv_trm2 t1) \<union> (fv_trm2 t2)"
-| "fv_trm2 (Lm2 x t) = (fv_trm2 t) - {atom x}"
-| "fv_trm2 (Lt2 as t) = (fv_trm2 t - bv2 as) \<union> (fv_assign as)"
-| "fv_assign (As x t) = (fv_trm2 t)"
+  "fv_rtrm2 (rVr2 x) = {atom x}"
+| "fv_rtrm2 (rAp2 t1 t2) = (fv_rtrm2 t1) \<union> (fv_rtrm2 t2)"
+| "fv_rtrm2 (rLm2 x t) = (fv_rtrm2 t) - {atom x}"
+| "fv_rtrm2 (rLt2 as t) = (fv_rtrm2 t - rbv2 as) \<union> (fv_rassign as)"
+| "fv_rassign (rAs x t) = fv_rtrm2 t"
 
 (* needs to be stated by the package *)
-instantiation 
-  trm2 and assign :: pt
+instantiation
+  rtrm2 and rassign :: pt
 begin
 
 primrec
-  permute_trm2 and permute_assign
+  permute_rtrm2 and permute_rassign
 where
-  "permute_trm2 pi (Vr2 a) = Vr2 (pi \<bullet> a)"
-| "permute_trm2 pi (Ap2 t1 t2) = Ap2 (permute_trm2 pi t1) (permute_trm2 pi t2)"
-| "permute_trm2 pi (Lm2 a t) = Lm2 (pi \<bullet> a) (permute_trm2 pi t)"
-| "permute_trm2 pi (Lt2 as t) = Lt2 (permute_assign pi as) (permute_trm2 pi t)"
-| "permute_assign pi (As a t) = As (pi \<bullet> a) (permute_trm2 pi t)"
+  "permute_rtrm2 pi (rVr2 a) = rVr2 (pi \<bullet> a)"
+| "permute_rtrm2 pi (rAp2 t1 t2) = rAp2 (permute_rtrm2 pi t1) (permute_rtrm2 pi t2)"
+| "permute_rtrm2 pi (rLm2 a t) = rLm2 (pi \<bullet> a) (permute_rtrm2 pi t)"
+| "permute_rtrm2 pi (rLt2 as t) = rLt2 (permute_rassign pi as) (permute_rtrm2 pi t)"
+| "permute_rassign pi (rAs a t) = rAs (pi \<bullet> a) (permute_rtrm2 pi t)"
 
-lemma pt_trm2_assign_zero:
-  fixes t::trm2
-  and   b::assign
+lemma pt_rtrm2_rassign_zero:
+  fixes t::rtrm2
+  and   b::rassign
   shows "0 \<bullet> t = t"
   and   "0 \<bullet> b = b"
-apply(induct t and b rule: trm2_assign.inducts)
+apply(induct t and b rule: rtrm2_rassign.inducts)
 apply(simp_all)
 done
 
-lemma pt_trm2_assign_plus:
-  fixes t::trm2
-  and   b::assign
+lemma pt_rtrm2_rassign_plus:
+  fixes t::rtrm2
+  and   b::rassign
   shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)"
   and   "((p + q) \<bullet> b) = p \<bullet> (q \<bullet> b)"
-apply(induct t and b rule: trm2_assign.inducts)
+apply(induct t and b rule: rtrm2_rassign.inducts)
 apply(simp_all)
 done
 
 instance
 apply default
-apply(simp_all add: pt_trm2_assign_zero pt_trm2_assign_plus)
+apply(simp_all add: pt_rtrm2_rassign_zero pt_rtrm2_rassign_plus)
 done
 
 
 end
 
 inductive
-  alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+  alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+and
+  alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)
 where
-  a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
-| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
-| a3: "\<exists>pi. (fv_trm2 t - {atom a} = fv_trm2 s - {atom b} \<and> 
-            (fv_trm2 t - {atom a})\<sharp>* pi \<and> 
-            (pi \<bullet> t) \<approx>2 s \<and> 
-            (pi \<bullet> a) = b)
-       \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
-| a4: "\<exists>pi. (
-         fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
-         (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
-         pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)
-       ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
+  a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"
+| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"
+| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"
+| a4: "(\<exists>pi. (((bv2 bt), t) \<approx>gen alpha2 fv_rtrm2 pi ((bv2 bs), s))) \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"
+| a5: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rAs a t \<approx>2a rAs b s"
 
-lemma alpha2_equivp: "equivp alpha2" 
+lemma alpha2_equivp:
+  "equivp alpha2"
+  "equivp alpha2a"
   sorry
 
-quotient_type qtrm2 = trm2 / alpha2
-  by (rule alpha2_equivp)
+quotient_type
+  trm2 = rtrm2 / alpha2
+and
+  assign = rassign / alpha2a
+  by (auto intro: alpha2_equivp)
+
 
 section {*** lets with many assignments ***}