# HG changeset patch # User Cezary Kaliszyk # Date 1265731507 -3600 # Node ID 84d666f9faceb48dbf9855f948d099c3c97485b2 # Parent 7e691b3c2414ba058bdbb3dbe895b2449868a876 the specifications of the respects. diff -r 7e691b3c2414 -r 84d666f9face Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Tue Feb 09 16:44:06 2010 +0100 +++ b/Quot/Nominal/Terms.thy Tue Feb 09 17:05:07 2010 +0100 @@ -1023,7 +1023,17 @@ as "rbv6" +lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" +apply simp apply clarify +apply (erule alpha6.induct) +apply simp +apply simp +apply (erule exE) +apply (simp add: alpha_gen) +sorry +lemma [quot_respect]:"(alpha6 ===> op =) rfv_trm6 rfv_trm6" +sorry lemma [quot_respect]: "(op = ===> alpha6) rVr6 rVr6" @@ -1039,6 +1049,11 @@ instantiation trm6 :: pt begin +quotient_definition + "permute_trm6 :: perm \ trm6 \ trm6" +as + "permute :: perm \ rtrm6 \ rtrm6" + instance sorry end @@ -1048,9 +1063,6 @@ apply (unfold alpha_gen) apply (lifting a3[unfolded alpha_gen]) apply injection - - - sorry