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 |
451 thm alpha_rtrm5_alpha_rlts.intros |
423 thm alpha_rtrm5_alpha_rlts.intros |
452 |
424 |
453 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)) *} |
454 thm alpha5_inj |
426 thm alpha5_inj |
455 |
427 |
456 lemma rbv5_eqvt: |
428 lemma rbv5_eqvt[eqvt]: |
457 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
429 "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)" |
458 sorry |
430 apply (induct x) |
459 |
431 apply (simp_all add: eqvts atom_eqvt) |
460 lemma fv_rtrm5_eqvt: |
432 done |
|
433 |
|
434 lemma fv_rtrm5_rlts_eqvt[eqvt]: |
461 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
435 "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)" |
462 sorry |
436 "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)" |
463 |
437 apply (induct x and l) |
464 lemma fv_rlts_eqvt: |
438 apply (simp_all add: eqvts atom_eqvt) |
465 "pi \<bullet> (fv_rlts x) = fv_rlts (pi \<bullet> x)" |
439 done |
466 sorry |
|
467 |
440 |
468 lemma alpha5_eqvt: |
441 lemma alpha5_eqvt: |
469 "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)" |
470 "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)" |
471 apply(induct rule: alpha_rtrm5_alpha_rlts.inducts) |
444 apply (induct rule: alpha_rtrm5_alpha_rlts.inducts) |
472 apply (simp_all add: alpha5_inj) |
445 apply (simp_all add: alpha5_inj) |
473 apply (erule exE)+ |
446 apply (tactic {* |
474 apply(unfold alpha_gen) |
447 ALLGOALS ( |
475 apply (erule conjE)+ |
448 TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW |
476 apply (rule conjI) |
449 (etac @{thm alpha_gen_compose_eqvt}) |
477 apply (rule_tac x="x \<bullet> pi" in exI) |
450 ) *}) |
478 apply (rule conjI) |
451 apply (simp_all only: eqvts atom_eqvt) |
479 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
480 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
481 apply(rule conjI) |
|
482 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
483 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rlts_eqvt) |
|
484 apply (subst permute_eqvt[symmetric]) |
|
485 apply (simp) |
|
486 apply (rule_tac x="x \<bullet> pia" in exI) |
|
487 apply (rule conjI) |
|
488 apply(rule_tac ?p1="- x" in permute_eq_iff[THEN iffD1]) |
|
489 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
|
490 apply(rule conjI) |
|
491 apply(rule_tac ?p1="- x" in fresh_star_permute_iff[THEN iffD1]) |
|
492 apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt rbv5_eqvt fv_rtrm5_eqvt) |
|
493 apply (subst permute_eqvt[symmetric]) |
|
494 apply (simp) |
|
495 done |
452 done |
496 |
453 |
497 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
454 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []), |
498 (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)) *} |
499 thm alpha5_equivp |
456 thm alpha5_equivp |