30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
30 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *} |
31 thm permute_rtrm1_permute_bp.simps |
31 thm permute_rtrm1_permute_bp.simps |
32 |
32 |
33 local_setup {* |
33 local_setup {* |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
34 snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1") |
35 [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]], |
35 [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]], |
36 [[], [], []]] *} |
36 [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *} |
37 |
37 |
38 notation |
38 notation |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
39 alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
40 alpha_bp ("_ \<approx>1b _" [100, 100] 100) |
41 thm alpha_rtrm1_alpha_bp.intros |
41 thm alpha_rtrm1_alpha_bp_alpha_bv1.intros |
42 thm fv_rtrm1_fv_bp.simps[no_vars] |
42 thm fv_rtrm1_fv_bp.simps[no_vars] |
43 |
43 |
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *} |
44 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *} |
45 thm alpha1_inj |
45 thm alpha1_inj |
46 |
46 |
47 local_setup {* |
47 local_setup {* |
48 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
48 snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)}) |
49 *} |
49 *} |
50 |
50 |
51 local_setup {* |
51 local_setup {* |
52 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
52 snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct} |
53 *} |
53 *} |
54 |
54 |
|
55 lemma alpha1_eqvt: "(rtrm1 \<approx>1 rtrm1a \<longrightarrow> (p \<bullet> rtrm1) \<approx>1 (p \<bullet> rtrm1a)) \<and> (bp \<approx>1b bpa \<longrightarrow> (p \<bullet> bp) \<approx>1b (p \<bullet> bpa)) |
|
56 \<and> (alpha_bv1 a b c \<longrightarrow> alpha_bv1 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
|
57 apply (rule alpha_rtrm1_alpha_bp_alpha_bv1.induct) |
|
58 apply (simp_all add: fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps alpha1_inj) |
|
59 apply (erule exE) |
|
60 apply (rule_tac x="p \<bullet> pi" in exI) |
|
61 apply (erule alpha_gen_compose_eqvt) |
|
62 apply (simp_all add: eqvts) |
|
63 apply (erule exE) |
|
64 apply (rule_tac x="p \<bullet> pi" in exI) |
|
65 apply (rule conjI) |
|
66 apply (erule conjE)+ |
|
67 apply (erule alpha_gen_compose_eqvt) |
|
68 apply (simp_all add: eqvts permute_eqvt[symmetric]) |
|
69 apply (simp add: eqvts[symmetric]) |
|
70 done |
|
71 (* |
55 local_setup {* |
72 local_setup {* |
56 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
73 (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_eqvt}, []), |
57 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} ctxt) ctxt)) *} |
74 build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.induct} ctxt) ctxt)) *}*) |
58 |
75 |
59 lemma alpha1_eqvt_proper[eqvt]: |
76 lemma alpha1_eqvt_proper[eqvt]: |
60 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
77 "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))" |
61 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
78 "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))" |
62 apply (simp_all only: eqvts) |
79 apply (simp_all only: eqvts) |
72 apply (simp_all only: alpha1_eqvt) |
89 apply (simp_all only: alpha1_eqvt) |
73 done |
90 done |
74 thm eqvts_raw(1) |
91 thm eqvts_raw(1) |
75 |
92 |
76 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
93 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []), |
77 (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)) *} |
94 (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp_alpha_bv1.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)) *} |
78 thm alpha1_equivp |
95 thm alpha1_equivp |
79 |
96 |
80 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
97 local_setup {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))] |
81 (rtac @{thm alpha1_equivp(1)} 1) *} |
98 (rtac @{thm alpha1_equivp(1)} 1) *} |
82 |
99 |