102 |
102 |
103 (* Shouyld we derive it? But bv is given by the user? *) |
103 (* Shouyld we derive it? But bv is given by the user? *) |
104 lemma bv1_eqvt[eqvt]: |
104 lemma bv1_eqvt[eqvt]: |
105 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
105 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
106 apply (induct x) |
106 apply (induct x) |
107 apply (simp_all add: eqvts) |
107 apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt) |
108 apply (rule atom_eqvt) |
|
109 done |
108 done |
110 |
109 |
111 lemma rfv_trm1_eqvt[eqvt]: |
110 lemma rfv_trm1_eqvt[eqvt]: |
112 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
111 shows "(pi\<bullet>rfv_trm1 t) = rfv_trm1 (pi\<bullet>t)" |
113 apply (induct t) |
112 apply (induct t) |
114 apply (simp_all add: eqvts) |
113 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
115 apply (rule atom_eqvt) |
|
116 apply (simp add: atom_eqvt) |
|
117 done |
114 done |
118 |
115 |
119 |
116 |
120 lemma alpha1_eqvt: |
117 lemma alpha1_eqvt: |
121 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
118 shows "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
125 apply (rule_tac x="pi \<bullet> pia" in exI) |
122 apply (rule_tac x="pi \<bullet> pia" in exI) |
126 apply (simp add: alpha_gen) |
123 apply (simp add: alpha_gen) |
127 apply(erule conjE)+ |
124 apply(erule conjE)+ |
128 apply(rule conjI) |
125 apply(rule conjI) |
129 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
126 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
130 apply(simp add: atom_eqvt eqvts) |
127 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt rfv_trm1_eqvt) |
131 apply(rule conjI) |
128 apply(rule conjI) |
132 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
129 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
133 apply(simp add: eqvts atom_eqvt) |
130 apply(simp add: atom_eqvt Diff_eqvt rfv_trm1_eqvt insert_eqvt empty_eqvt) |
134 apply(simp add: permute_eqvt[symmetric]) |
131 apply(simp add: permute_eqvt[symmetric]) |
135 apply (erule exE) |
132 apply (erule exE) |
136 apply (rule_tac x="pi \<bullet> pia" in exI) |
133 apply (rule_tac x="pi \<bullet> pia" in exI) |
137 apply (simp add: alpha_gen) |
134 apply (simp add: alpha_gen) |
138 apply(erule conjE)+ |
135 apply(erule conjE)+ |
139 apply(rule conjI) |
136 apply(rule conjI) |
140 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
137 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
141 apply(simp add: atom_eqvt eqvts) |
138 apply(simp add: rfv_trm1_eqvt Diff_eqvt bv1_eqvt) |
142 apply(rule conjI) |
139 apply(rule conjI) |
143 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
140 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
144 apply(simp add: eqvts atom_eqvt) |
141 apply(simp add: atom_eqvt rfv_trm1_eqvt Diff_eqvt bv1_eqvt) |
145 apply(simp add: permute_eqvt[symmetric]) |
142 apply(simp add: permute_eqvt[symmetric]) |
146 done |
143 done |
147 |
144 |
148 lemma alpha1_equivp: "equivp alpha1" |
145 lemma alpha1_equivp: "equivp alpha1" |
149 sorry |
146 sorry |
644 lemma alpha4list_equivp: "equivp alpha4list" sorry |
641 lemma alpha4list_equivp: "equivp alpha4list" sorry |
645 |
642 |
646 quotient_type |
643 quotient_type |
647 qtrm4 = trm4 / alpha4 and |
644 qtrm4 = trm4 / alpha4 and |
648 qtrm4list = "trm4 list" / alpha4list |
645 qtrm4list = "trm4 list" / alpha4list |
649 by (simp_all add: alpha4_equivp alpha4list_equivp |
646 by (simp_all add: alpha4_equivp alpha4list_equivp) |
650 |
647 |
651 |
648 |
652 datatype rtrm5 = |
649 datatype rtrm5 = |
653 rVr5 "name" |
650 rVr5 "name" |
654 | rAp5 "rtrm5" "rtrm5" |
651 | rAp5 "rtrm5" "rtrm5" |