132 print_theorems |
132 print_theorems |
133 |
133 |
134 lemma alpha_rfv1: |
134 lemma alpha_rfv1: |
135 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
135 shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s" |
136 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
136 apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1)) |
137 apply(simp_all add: alpha_gen.simps) |
137 apply(simp_all add: fv_rtrm1_fv_bp.simps alpha_gen.simps) |
138 done |
138 done |
139 |
139 |
140 lemma [quot_respect]: |
140 lemma [quot_respect]: |
141 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
141 "(op = ===> alpha_rtrm1) rVr1 rVr1" |
142 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
142 "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1" |
143 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
143 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1" |
144 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
144 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1" |
145 apply (auto simp add: alpha1_inj) |
145 apply (auto simp add: alpha1_inj) |
146 apply (rule_tac x="0" in exI) |
146 apply (rule_tac [!] x="0" in exI) |
147 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
147 apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) |
148 apply (rule_tac x="0" in exI) |
|
149 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1 alpha_bp_eq) |
|
150 apply (rule_tac x="0" in exI) |
|
151 apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1) |
|
152 done |
148 done |
153 |
149 |
154 lemma [quot_respect]: |
150 lemma [quot_respect]: |
155 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" |
151 "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute" |
156 by (simp add: alpha1_eqvt) |
152 by (simp add: alpha1_eqvt) |
539 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
535 "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5" |
540 "(alpha_rlts ===> op =) rbv5 rbv5" |
536 "(alpha_rlts ===> op =) rbv5 rbv5" |
541 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
537 "(op = ===> alpha_rtrm5) rVr5 rVr5" |
542 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
538 "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5" |
543 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
539 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
544 "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5" |
|
545 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
540 "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons" |
546 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
541 "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute" |
547 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
542 "(op = ===> alpha_rlts ===> alpha_rlts) permute permute" |
548 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
543 apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp) |
549 apply (clarify) apply (rule conjI) |
|
550 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
551 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
|
552 apply (clarify) apply (rule conjI) |
544 apply (clarify) apply (rule conjI) |
553 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
545 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
554 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
546 apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv) |
555 done |
547 done |
556 |
548 |
629 |
621 |
630 |
622 |
631 lemma lets_not_ok1: |
623 lemma lets_not_ok1: |
632 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
624 "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
633 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
625 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
634 apply (subst alpha5_INJ(3)) |
626 apply (simp add: alpha5_INJ(3) alpha_gen) |
635 apply(clarify) |
627 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1)) |
636 apply (simp add: alpha_gen) |
|
637 apply (simp add: permute_trm5_lts fresh_star_def) |
|
638 apply (simp add: alpha5_INJ(5)) |
|
639 apply(clarify) |
|
640 apply (simp add: alpha5_INJ(2)) |
|
641 apply (simp add: alpha5_INJ(1)) |
|
642 done |
628 done |
643 |
629 |
644 lemma distinct_helper: |
630 lemma distinct_helper: |
645 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
631 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
646 apply auto |
632 apply auto |
654 |
640 |
655 lemma lets_nok: |
641 lemma lets_nok: |
656 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
642 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
657 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
643 (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
658 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
644 (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
659 apply (subst alpha5_INJ) |
645 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def) |
660 apply (simp only: alpha_gen permute_trm5_lts fresh_star_def) |
|
661 apply (subst alpha5_INJ(5)) |
|
662 apply (subst alpha5_INJ(5)) |
|
663 apply (simp add: distinct_helper2) |
646 apply (simp add: distinct_helper2) |
664 done |
647 done |
665 |
648 |
666 |
649 |
667 (* example with a bn function defined over the type itself *) |
650 (* example with a bn function defined over the type itself *) |