# HG changeset patch # User Christian Urban # Date 1265197506 -3600 # Node ID ef024a42c1bbfc4b7af0fe2aad5941ea4eed0cdf # Parent 534d4c604f8073092da7dad8914fafbfaf1b0368# Parent 5a3bc323661cf800617a33e8c7cb05f4368ba95a merged diff -r 534d4c604f80 -r ef024a42c1bb Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Wed Feb 03 12:44:29 2010 +0100 +++ b/Quot/Nominal/Terms.thy Wed Feb 03 12:45:06 2010 +0100 @@ -719,7 +719,44 @@ (pi \ (bv5 l1) = bv5 l2)) \ rLt5 l1 t1 \5 rLt5 l2 t2" | a4: "rLnil \l rLnil" -| a5: "ls1 \l ls2 \ t1 \5 t2 \ rLcons n1 t1 ls1 \l rLcons n2 t2 ls2" +| a5: "ls1 \l ls2 \ t1 \5 t2 \ n1 = n2 \ rLcons n1 t1 ls1 \l rLcons n2 t2 ls2" + +print_theorems -thm a3[simplified alpha_gen] +lemma alpha5_inj: + "((rVr5 a) \5 (rVr5 b)) = (a = b)" + "(rAp5 t1 s1 \5 rAp5 t2 s2) = (t1 \5 t2 \ s1 \5 s2)" + "(rLt5 l1 t1 \5 rLt5 l2 t2) = (\pi. ((bv5 l1, t1) \gen alpha5 rfv_trm5 pi (bv5 l2, t2) \ + (bv5 l1, l1) \gen alphalts rfv_lts pi (bv5 l2, l2) \ + (pi \ (bv5 l1) = bv5 l2)))" + "rLnil \l rLnil" + "(rLcons n1 t1 ls1 \l rLcons n2 t2 ls2) = (ls1 \l ls2 \ t1 \5 t2 \ n1 = n2)" +apply - +apply (simp_all add: alpha5_alphalts.intros) +apply rule +apply (erule alpha5.cases) +apply (simp_all add: alpha5_alphalts.intros) +apply rule +apply (erule alpha5.cases) +apply (simp_all add: alpha5_alphalts.intros) +apply rule +apply (erule alpha5.cases) +apply (simp_all add: alpha5_alphalts.intros) +apply rule +apply (erule alphalts.cases) +apply (simp_all add: alpha5_alphalts.intros) +done + +lemma alpha5_equivps: + shows "equivp alpha5" + and "equivp alphalts" +sorry + +quotient_type + trm5 = rtrm5 / alpha5 +and + lts = rlts / alphalts + by (auto intro: alpha5_equivps) + + end