52 notation |
52 notation |
53 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
53 alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and |
54 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
54 alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100) |
55 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
55 thm alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2] |
56 |
56 |
57 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} |
57 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros[simplified fix2]} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases[simplified fix2] alpha_rtrm4_list.cases[simplified fix2]} ctxt)) ctxt)) *} |
58 thm alpha4_inj |
58 thm alpha4_inj |
59 |
59 |
60 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
60 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj_no}, []), (build_rel_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *} |
61 thm alpha4_inj_no |
61 thm alpha4_inj_no |
62 |
62 |
63 local_setup {* |
63 local_setup {* snd o (prove_eqvt [@{typ rtrm4},@{typ "rtrm4 list"}] @{thm rtrm4.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] fv_rtrm4_fv_rtrm4_list.simps} [@{term fv_rtrm4}, @{term fv_rtrm4_list}]) *} |
64 snd o build_eqvts @{binding fv_rtrm4_fv_rtrm4_list_eqvt} [@{term fv_rtrm4}, @{term fv_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] (@{thms fv_rtrm4_fv_rtrm4_list.simps permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]}) @{thm rtrm4.induct} |
64 thm eqvts(1-2) |
65 *} |
|
66 print_theorems |
|
67 |
65 |
68 local_setup {* |
66 local_setup {* |
69 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), |
67 (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_eqvt_no}, []), |
70 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"},@{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} ctxt) ctxt)) |
68 build_alpha_eqvts [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] (fn _ => alpha_eqvt_tac @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms permute_rtrm4_permute_rtrm4_list.simps[simplified repaired] alpha4_inj_no} ctxt 1) ctxt) ctxt)) |
71 *} |
69 *} |
72 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
70 lemmas alpha4_eqvt = alpha4_eqvt_no[simplified fix2] |
73 |
71 |
|
72 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_reflp}, []), |
|
73 build_alpha_refl [((0, @{term alpha_rtrm4}), 0), ((0, @{term alpha_rtrm4_list}), 0)] [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thms alpha4_inj_no} ctxt) ctxt)) *} |
|
74 thm alpha4_reflp |
|
75 ML build_equivps |
|
76 |
74 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
77 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp_no}, []), |
75 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} |
78 (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thms alpha4_reflp} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj_no} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt_no} ctxt)) ctxt)) *} |
76 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
79 lemmas alpha4_equivp = alpha4_equivp_no[simplified fix2] |
77 |
|
78 (*lemma fv_rtrm4_rsp: |
|
79 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
|
80 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
|
81 apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) |
|
82 apply (simp_all add: alpha_gen) |
|
83 done*) |
|
84 |
|
85 |
80 |
86 quotient_type |
81 quotient_type |
87 trm4 = rtrm4 / alpha_rtrm4 |
82 trm4 = rtrm4 / alpha_rtrm4 |
88 (*and |
83 (*and |
89 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
84 trm4list = "rtrm4 list" / alpha_rtrm4_list*) |
90 by (simp_all add: alpha4_equivp) |
85 by (simp_all add: alpha4_equivp) |
91 |
86 |
92 local_setup {* |
87 local_setup {* |
93 (fn ctxt => ctxt |
88 (fn ctxt => ctxt |
94 |> snd o (Quotient_Def.quotient_lift_const ("Vr4", @{term rVr4})) |
89 |> snd o (Quotient_Def.quotient_lift_const [] ("Vr4", @{term rVr4})) |
95 |> snd o (Quotient_Def.quotient_lift_const ("Ap4", @{term rAp4})) |
90 |> snd o (Quotient_Def.quotient_lift_const [@{typ "trm4"}] ("Ap4", @{term rAp4})) |
96 |> snd o (Quotient_Def.quotient_lift_const ("Lm4", @{term rLm4}))) |
91 |> snd o (Quotient_Def.quotient_lift_const [] ("Lm4", @{term rLm4})) |
|
92 |> snd o (Quotient_Def.quotient_lift_const [] ("fv_trm4", @{term fv_rtrm4}))) |
97 *} |
93 *} |
98 print_theorems |
94 print_theorems |
99 |
95 |
100 local_setup {* snd o prove_const_rsp @{binding fv_rtrm4_rsp} [@{term fv_rtrm4}] |
96 |
101 (fn _ => fvbv_rsp_tac @{thm alpha_rtrm4_alpha_rtrm4_list.inducts(1)} @{thms fv_rtrm4_fv_rtrm4_list.simps} 1) *} |
97 |
|
98 lemma fv_rtrm4_rsp: |
|
99 "xa \<approx>4 ya \<Longrightarrow> fv_rtrm4 xa = fv_rtrm4 ya" |
|
100 "x \<approx>4l y \<Longrightarrow> fv_rtrm4_list x = fv_rtrm4_list y" |
|
101 apply (induct rule: alpha_rtrm4_alpha_rtrm4_list.inducts) |
|
102 apply (simp_all add: alpha_gen) |
|
103 done |
|
104 |
|
105 local_setup {* snd o prove_const_rsp [] @{binding fv_rtrm4_rsp'} [@{term fv_rtrm4}] |
|
106 (fn _ => asm_full_simp_tac (@{simpset} addsimps @{thms fv_rtrm4_rsp}) 1) *} |
102 print_theorems |
107 print_theorems |
103 |
108 |
104 local_setup {* snd o prove_const_rsp @{binding rVr4_rsp} [@{term rVr4}] |
109 ML constr_rsp_tac |
105 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} |
|
106 lemma "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
|
107 apply simp |
|
108 apply clarify |
|
109 apply (simp add: alpha4_inj) |
|
110 |
110 |
|
111 local_setup {* snd o prove_const_rsp [] @{binding rVr4_rsp} [@{term rVr4}] |
|
112 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
|
113 local_setup {* snd o prove_const_rsp [] @{binding rLm4_rsp} [@{term rLm4}] |
|
114 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp alpha4_equivp} 1) *} |
111 |
115 |
112 local_setup {* snd o prove_const_rsp @{binding rLm4_rsp} [@{term rLm4}] |
116 lemma [quot_respect]: |
113 (fn _ => constr_rsp_tac @{thms alpha4_inj} @{thms fv_rtrm4_rsp} @{thms alpha4_equivp} 1) *} |
117 "(alpha_rtrm4 ===> list_rel alpha_rtrm4 ===> alpha_rtrm4) rAp4 rAp4" |
114 local_setup {* snd o prove_const_rsp @{binding permute_rtrm4_rsp} |
118 by (simp add: alpha4_inj) |
115 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}, @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"}] |
119 |
|
120 (* Maybe also need: @{term "permute :: perm \<Rightarrow> rtrm4 list \<Rightarrow> rtrm4 list"} *) |
|
121 local_setup {* snd o prove_const_rsp [] @{binding permute_rtrm4_rsp} |
|
122 [@{term "permute :: perm \<Rightarrow> rtrm4 \<Rightarrow> rtrm4"}] |
116 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
123 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha4_eqvt}) 1) *} |
|
124 print_theorems |
117 |
125 |
118 thm rtrm4.induct |
126 lemma list_rel_rsp: |
119 lemmas trm1_bp_induct = rtrm4.induct[quot_lifted] |
127 "\<lbrakk>\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b); list_rel R x y; list_rel R a b\<rbrakk> |
|
128 \<Longrightarrow> list_rel S x a = list_rel T y b" |
|
129 sorry |
|
130 |
|
131 lemma[quot_respect]: |
|
132 "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel" |
|
133 by (simp add: list_rel_rsp) |
|
134 |
|
135 lemma[quot_preserve]: |
|
136 assumes a: "Quotient R abs1 rep1" |
|
137 shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel" |
|
138 apply (simp add: expand_fun_eq) |
|
139 apply clarify |
|
140 apply (induct_tac xa xb rule: list_induct2') |
|
141 apply (simp_all add: Quotient_abs_rep[OF a]) |
|
142 done |
|
143 |
|
144 lemma[quot_preserve]: |
|
145 assumes a: "Quotient R abs1 rep1" |
|
146 shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)" |
|
147 by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a]) |
|
148 |
|
149 lemma bla: "(Ap4 trm4 list = Ap4 trm4a lista) = |
|
150 (trm4 = trm4a \<and> list_rel (op =) list lista)" |
|
151 by (lifting alpha4_inj(2)) |
|
152 |
|
153 thm bla[simplified list_rel_eq] |
|
154 |
|
155 lemma " (Lm4 name rtrm4 = Lm4 namea rtrm4a) = |
|
156 (\<exists>pi\<Colon>perm. |
|
157 fv_trm4 rtrm4 - {atom name} = fv_trm4 rtrm4a - {atom namea} \<and> |
|
158 (fv_trm4 rtrm4 - {atom name}) \<sharp>* pi \<and> |
|
159 pi \<bullet> rtrm4 = rtrm4a \<and> pi \<bullet> {atom name} = {atom namea})" |
|
160 |
|
161 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(1)} *} |
|
162 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(2)} *} |
|
163 ML {* lift_thm [@{typ trm4}] @{context} @{thm alpha4_inj(3)[unfolded alpha_gen]} *} |
|
164 ML {* lift_thm [@{typ trm4}] @{context} @{thm rtrm4.induct} *} |
|
165 . |
|
166 |
|
167 (*lemmas trm1_bp_induct = rtrm4.induct[quot_lifted]*) |
120 |
168 |
121 end |
169 end |