101 sorry |
101 sorry |
102 |
102 |
103 quotient_type trm1 = rtrm1 / alpha1 |
103 quotient_type trm1 = rtrm1 / alpha1 |
104 by (rule alpha1_equivp) |
104 by (rule alpha1_equivp) |
105 |
105 |
106 quotient_definition |
106 local_setup {* |
107 "Vr1 :: name \<Rightarrow> trm1" |
107 (fn ctxt => ctxt |
108 is |
108 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1})) |
109 "rVr1" |
109 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1})) |
110 |
110 |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1})) |
111 quotient_definition |
111 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1})) |
112 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
112 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1}))) |
113 is |
113 *} |
114 "rAp1" |
114 print_theorems |
115 |
|
116 quotient_definition |
|
117 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
118 is |
|
119 "rLm1" |
|
120 |
|
121 quotient_definition |
|
122 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
123 is |
|
124 "rLt1" |
|
125 |
|
126 quotient_definition |
|
127 "fv_trm1 :: trm1 \<Rightarrow> atom set" |
|
128 is |
|
129 "fv_rtrm1" |
|
130 |
115 |
131 lemma alpha_rfv1: |
116 lemma alpha_rfv1: |
132 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
117 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
133 apply(induct rule: alpha1.induct) |
118 apply(induct rule: alpha1.induct) |
134 apply(simp_all add: alpha_gen.simps) |
119 apply(simp_all add: alpha_gen.simps) |
315 trm2 = rtrm2 / alpha2 |
300 trm2 = rtrm2 / alpha2 |
316 and |
301 and |
317 assign = rassign / alpha2a |
302 assign = rassign / alpha2a |
318 by (auto intro: alpha2_equivp) |
303 by (auto intro: alpha2_equivp) |
319 |
304 |
|
305 local_setup {* |
|
306 (fn ctxt => ctxt |
|
307 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2})) |
|
308 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2})) |
|
309 |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2})) |
|
310 |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2})) |
|
311 |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs})) |
|
312 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2})) |
|
313 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2}))) |
|
314 *} |
|
315 print_theorems |
320 |
316 |
321 |
317 |
322 section {*** lets with many assignments ***} |
318 section {*** lets with many assignments ***} |
323 |
319 |
324 datatype trm3 = |
320 datatype trm3 = |
493 trm5 = rtrm5 / alpha5 |
489 trm5 = rtrm5 / alpha5 |
494 and |
490 and |
495 lts = rlts / alphalts |
491 lts = rlts / alphalts |
496 by (auto intro: alpha5_equivps) |
492 by (auto intro: alpha5_equivps) |
497 |
493 |
498 quotient_definition |
494 local_setup {* |
499 "Vr5 :: name \<Rightarrow> trm5" |
495 (fn ctxt => ctxt |
500 is |
496 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5})) |
501 "rVr5" |
497 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5})) |
502 |
498 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5})) |
503 quotient_definition |
499 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil})) |
504 "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5" |
500 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons})) |
505 is |
501 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5})) |
506 "rAp5" |
502 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts})) |
507 |
503 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))) |
508 quotient_definition |
504 *} |
509 "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5" |
505 print_theorems |
510 is |
|
511 "rLt5" |
|
512 |
|
513 quotient_definition |
|
514 "Lnil :: lts" |
|
515 is |
|
516 "rLnil" |
|
517 |
|
518 quotient_definition |
|
519 "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts" |
|
520 is |
|
521 "rLcons" |
|
522 |
|
523 quotient_definition |
|
524 "fv_trm5 :: trm5 \<Rightarrow> atom set" |
|
525 is |
|
526 "fv_rtrm5" |
|
527 |
|
528 quotient_definition |
|
529 "fv_lts :: lts \<Rightarrow> atom set" |
|
530 is |
|
531 "fv_rlts" |
|
532 |
|
533 quotient_definition |
|
534 "bv5 :: lts \<Rightarrow> atom set" |
|
535 is |
|
536 "rbv5" |
|
537 |
506 |
538 lemma rbv5_eqvt: |
507 lemma rbv5_eqvt: |
539 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
508 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
540 sorry |
509 sorry |
541 |
510 |
752 |
721 |
753 quotient_type |
722 quotient_type |
754 trm6 = rtrm6 / alpha6 |
723 trm6 = rtrm6 / alpha6 |
755 by (auto intro: alpha6_equivps) |
724 by (auto intro: alpha6_equivps) |
756 |
725 |
757 quotient_definition |
726 local_setup {* |
758 "Vr6 :: name \<Rightarrow> trm6" |
727 (fn ctxt => ctxt |
759 is |
728 |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6})) |
760 "rVr6" |
729 |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6})) |
761 |
730 |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6})) |
762 quotient_definition |
731 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6})) |
763 "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6" |
732 |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6}))) |
764 is |
733 *} |
765 "rLm6" |
734 print_theorems |
766 |
|
767 quotient_definition |
|
768 "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6" |
|
769 is |
|
770 "rLt6" |
|
771 |
|
772 quotient_definition |
|
773 "fv_trm6 :: trm6 \<Rightarrow> atom set" |
|
774 is |
|
775 "fv_rtrm6" |
|
776 |
|
777 quotient_definition |
|
778 "bv6 :: trm6 \<Rightarrow> atom set" |
|
779 is |
|
780 "rbv6" |
|
781 |
735 |
782 lemma [quot_respect]: |
736 lemma [quot_respect]: |
783 "(op = ===> alpha6 ===> alpha6) permute permute" |
737 "(op = ===> alpha6 ===> alpha6) permute permute" |
784 apply auto (* will work with eqvt *) |
738 apply auto (* will work with eqvt *) |
785 sorry |
739 sorry |
786 |
740 |
787 (* Definitely not true , see lemma below *) |
741 (* Definitely not true , see lemma below *) |
788 |
|
789 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
742 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6" |
790 apply simp apply clarify |
743 apply simp apply clarify |
791 apply (erule alpha6.induct) |
744 apply (erule alpha6.induct) |
792 oops |
745 oops |
793 |
746 |
1006 |
959 |
1007 quotient_type |
960 quotient_type |
1008 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
961 lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b |
1009 sorry |
962 sorry |
1010 |
963 |
1011 quotient_definition |
964 local_setup {* |
1012 "qVar9 :: name \<Rightarrow> lam9" |
965 (fn ctxt => ctxt |
1013 is |
966 |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9})) |
1014 "Var9" |
967 |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9})) |
1015 |
968 |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9})) |
1016 quotient_definition |
969 |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9})) |
1017 "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9" |
970 |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9})) |
1018 is |
971 |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9}))) |
1019 "Lam9" |
972 *} |
1020 |
973 print_theorems |
1021 quotient_definition |
|
1022 "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9" |
|
1023 is |
|
1024 "Bla9" |
|
1025 |
|
1026 quotient_definition |
|
1027 "fv_lam9 :: lam9 \<Rightarrow> atom set" |
|
1028 is |
|
1029 "fv_rlam9" |
|
1030 |
|
1031 quotient_definition |
|
1032 "fv_bla9 :: bla9 \<Rightarrow> atom set" |
|
1033 is |
|
1034 "fv_rbla9" |
|
1035 |
|
1036 quotient_definition |
|
1037 "bv9 :: lam9 \<Rightarrow> atom set" |
|
1038 is |
|
1039 "rbv9" |
|
1040 |
974 |
1041 instantiation lam9 and bla9 :: pt |
975 instantiation lam9 and bla9 :: pt |
1042 begin |
976 begin |
1043 |
977 |
1044 quotient_definition |
978 quotient_definition |