46 "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)" |
46 "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)" |
47 apply (induct x and l) |
47 apply (induct x and l) |
48 apply (simp_all add: eqvts atom_eqvt) |
48 apply (simp_all add: eqvts atom_eqvt) |
49 done |
49 done |
50 |
50 |
51 lemma alpha5_eqvt: |
51 (*lemma alpha5_eqvt: |
52 "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and> |
52 "(xa \<approx>5 y \<longrightarrow> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and> |
53 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
53 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
54 (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
54 (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
55 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) |
55 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) |
56 done |
56 done*) |
|
57 |
|
58 local_setup {* |
|
59 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []), |
|
60 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *} |
|
61 print_theorems |
57 |
62 |
58 lemma alpha5_reflp: |
63 lemma alpha5_reflp: |
59 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
64 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
60 apply (rule rtrm5_rlts.induct) |
65 apply (rule rtrm5_rlts.induct) |
61 apply (simp_all add: alpha5_inj) |
66 apply (simp_all add: alpha5_inj) |
67 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
72 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and> |
68 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
73 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
69 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
74 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
70 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
75 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
71 apply (simp_all add: alpha5_inj) |
76 apply (simp_all add: alpha5_inj) |
72 sorry |
77 apply (erule exE) |
|
78 apply (rule_tac x="- pi" in exI) |
|
79 apply clarify |
|
80 apply (erule alpha_gen_compose_sym) |
|
81 apply (simp add: alpha5_eqvt) |
|
82 apply(clarify) |
|
83 apply (rotate_tac 1) |
|
84 apply (frule_tac p="- pi" in alpha5_eqvt(1)) |
|
85 apply simp |
|
86 done |
|
87 |
|
88 |
73 |
89 |
74 lemma alpha5_equivp: |
90 lemma alpha5_equivp: |
75 "equivp alpha_rtrm5" |
91 "equivp alpha_rtrm5" |
76 "equivp alpha_rlts" |
92 "equivp alpha_rlts" |
77 "equivp (alpha_rbv5 p)" |
93 "equivp (alpha_rbv5 p)" |