63 done |
63 done |
64 |
64 |
65 lemma bv1_eqvt[eqvt]: |
65 lemma bv1_eqvt[eqvt]: |
66 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
66 shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)" |
67 apply (induct x) |
67 apply (induct x) |
68 apply (simp_all add: atom_eqvt eqvts) |
68 apply (simp_all add: eqvts atom_eqvt) |
69 done |
69 done |
70 |
70 |
71 lemma fv_rtrm1_eqvt[eqvt]: |
71 lemma fv_rtrm1_eqvt[eqvt]: |
72 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
72 "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)" |
73 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)" |
73 "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)" |
74 apply (induct t and b) |
74 apply (induct t and b) |
75 apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt) |
75 apply (simp_all add: eqvts atom_eqvt) |
76 done |
76 done |
77 |
77 |
78 lemma alpha1_eqvt: |
78 lemma alpha1_eqvt: |
79 "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
79 "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)" |
80 "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)" |
80 "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)" |
81 apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) |
81 apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts) |
82 apply (simp_all add:eqvts alpha1_inj) |
82 apply (simp_all add:eqvts alpha1_inj) |
83 apply (erule exE) |
83 apply (tactic {* |
84 apply (rule_tac x="pi \<bullet> pia" in exI) |
84 ALLGOALS ( |
85 apply (simp add: alpha_gen) |
85 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
86 apply(erule conjE)+ |
86 (etac @{thm alpha_gen_compose_eqvt}) |
87 apply(rule conjI) |
87 ) *}) |
88 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
88 apply (simp_all only: eqvts atom_eqvt) |
89 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt) |
|
90 apply(rule conjI) |
|
91 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
92 apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt) |
|
93 apply(simp add: permute_eqvt[symmetric]) |
|
94 apply (erule exE) |
|
95 apply (erule exE) |
|
96 apply (rule conjI) |
|
97 apply (rule_tac x="pi \<bullet> pia" in exI) |
|
98 apply (simp add: alpha_gen) |
|
99 apply(erule conjE)+ |
|
100 apply(rule conjI) |
|
101 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
102 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
103 apply(rule conjI) |
|
104 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
105 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
106 apply(simp add: permute_eqvt[symmetric]) |
|
107 apply (rule_tac x="pi \<bullet> piaa" in exI) |
|
108 apply (simp add: alpha_gen) |
|
109 apply(erule conjE)+ |
|
110 apply(rule conjI) |
|
111 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
112 apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
113 apply(rule conjI) |
|
114 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
115 apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt) |
|
116 apply(simp add: permute_eqvt[symmetric]) |
|
117 done |
89 done |
118 |
90 |
119 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
91 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
120 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
92 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *} |
121 thm alpha1_equivp |
93 thm alpha1_equivp |
148 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
120 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *} |
149 |
121 |
150 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
122 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted] |
151 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
123 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted] |
152 |
124 |
153 instantiation trm1 and bp :: pt |
125 setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})] |
154 begin |
126 @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *} |
155 |
|
156 quotient_definition |
|
157 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
158 is |
|
159 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
|
160 |
|
161 instance by default |
|
162 (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted]) |
|
163 |
|
164 end |
|
165 |
127 |
166 lemmas |
128 lemmas |
167 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
129 permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted] |
168 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
130 and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted] |
169 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
131 and fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted] |
461 thm alpha_rtrm5_alpha_rlts.intros |
423 thm alpha_rtrm5_alpha_rlts.intros |
462 |
424 |
463 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
425 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *} |
464 thm alpha5_inj |
426 thm alpha5_inj |
465 |
427 |
466 lemma rbv5_eqvt: |
428 lemma rbv5_eqvt[eqvt]: |
467 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
429 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
468 sorry |
430 apply (induct x) |
469 |
431 apply (simp_all add: eqvts atom_eqvt) |
470 lemma fv_rtrm5_eqvt: |
432 done |
|
433 |
|
434 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
471 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
435 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
472 sorry |
436 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
473 |
437 apply (induct x and l) |
474 lemma fv_rlts_eqvt: |
438 apply (simp_all add: eqvts atom_eqvt) |
475 "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)" |
439 done |
476 sorry |
|
477 |
440 |
478 lemma alpha5_eqvt: |
441 lemma alpha5_eqvt: |
479 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
442 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
480 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
443 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
481 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
444 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
482 apply (simp_all add: alpha5_inj) |
445 apply (simp_all add: alpha5_inj) |
483 apply (erule exE)+ |
446 apply (tactic {* |
484 apply(unfold alpha_gen) |
447 ALLGOALS ( |
485 apply (erule conjE)+ |
448 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
486 apply (rule conjI) |
449 (etac @{thm alpha_gen_compose_eqvt}) |
487 apply (rule_tac x="x \<bullet> pi" in exI) |
450 ) *}) |
488 apply (rule conjI) |
451 apply (simp_all only: eqvts atom_eqvt) |
489 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
490 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
491 apply(rule conjI) |
|
492 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
493 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
494 apply (subst permute_eqvt[symmetric]) |
|
495 apply (simp) |
|
496 apply (rule_tac x="x \<bullet> pia" in exI) |
|
497 apply (rule conjI) |
|
498 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
499 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
|
500 apply(rule conjI) |
|
501 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
502 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
|
503 apply (subst permute_eqvt[symmetric]) |
|
504 apply (simp) |
|
505 done |
452 done |
506 |
453 |
507 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
454 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
508 (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} |
455 (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *} |
509 thm alpha5_equivp |
456 thm alpha5_equivp |