51 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
51 ML {* val consts = [@{const_name "rVar"}, @{const_name "rApp"}, @{const_name "rLam"}]; *} |
52 |
52 |
53 ML {* val rty = @{typ "rlam"} *} |
53 ML {* val rty = @{typ "rlam"} *} |
54 ML {* val qty = @{typ "lam"} *} |
54 ML {* val qty = @{typ "lam"} *} |
55 ML {* val rel = @{term "alpha"} *} |
55 ML {* val rel = @{term "alpha"} *} |
56 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{theory}) *} |
56 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
57 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
57 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
58 ML {* val quot = @{thm QUOTIENT_lam} *} |
58 ML {* val quot = @{thm QUOTIENT_lam} *} |
59 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
59 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rLam_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
60 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
60 ML {* val trans2 = @{thm QUOT_TYPE_I_lam.R_trans2} *} |
61 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
61 ML {* val reps_same = @{thm QUOT_TYPE_I_lam.REPS_same} *} |
75 |
75 |
76 thm fresh_def |
76 thm fresh_def |
77 thm supp_def |
77 thm supp_def |
78 |
78 |
79 local_setup {* |
79 local_setup {* |
80 make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
80 old_make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
81 *} |
81 *} |
82 |
82 |
83 ML {* val consts = @{const_name perm} :: consts *} |
83 ML {* val consts = @{const_name perm} :: consts *} |
84 ML {* val defs = @{thms lperm_def} @ defs *} |
84 ML {* val defs = @{thms lperm_def} @ defs *} |
85 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
85 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
86 ML {* val t_a = atomize_thm t_u *} |
86 ML {* val t_a = atomize_thm @{thm a3} *} |
87 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
87 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
88 |
|
89 ML {* |
|
90 fun r_mk_comb_tac_lam ctxt = r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms |
|
91 *} |
|
92 |
|
93 prove {* build_repabs_goal @{context} t_r consts rty qty *} |
|
94 apply (atomize(full)) |
|
95 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
96 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
97 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
98 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
99 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
100 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
101 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
102 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
103 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
104 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
105 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
106 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
107 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
108 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
109 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
110 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
111 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
112 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
113 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
114 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
115 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
116 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
117 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
118 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
119 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
120 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
121 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
122 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
123 prefer 2 |
|
124 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
125 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
126 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
127 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
128 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
129 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
130 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
131 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
132 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
133 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
134 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
135 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
136 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
137 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
138 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
139 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
140 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
141 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
142 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
143 nitpick |
|
144 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
145 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
146 apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) |
|
147 |
|
148 |
|
149 |
|
150 |
|
151 |
|
152 |
|
153 |
|
154 ML {* val t_t = Toplevel.program (fn () => repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms) *} |
|
155 |
|
156 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
88 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
157 |
|
158 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
89 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
159 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
90 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
160 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
91 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
161 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
92 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
162 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
93 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
163 ML {* ObjectLogic.rulify t_b *} |
|
164 ML {* val rr = (add_lower_defs @{context} @{thms lperm_def}) *} |
94 ML {* val rr = (add_lower_defs @{context} @{thms lperm_def}) *} |
165 ML {* val rrr = @{thm eq_reflection} OF [rr] *} |
95 ML {* val rrr = @{thm eq_reflection} OF [hd (rev rr)] *} |
166 ML {* MetaSimplifier.rewrite_rule [rrr] t_b *} |
96 lemma prod_fun_id: "prod_fun id id = id" |
|
97 apply (simp add: prod_fun_def) |
|
98 done |
|
99 lemma map_id: "map id x = x" |
|
100 apply (induct x) |
|
101 apply (simp_all add: map.simps) |
|
102 done |
167 |
103 |
|
104 ML {* val rrrr = repeat_eqsubst_thm @{context} @{thms prod_fun_id map_id} rrr *} |
|
105 ML {* val t_b' = eqsubst_thm @{context} [rrrr] t_b *} |
|
106 ML {* ObjectLogic.rulify t_b' *} |
168 |
107 |
169 |
108 |
170 |
109 |
171 local_setup {* |
110 local_setup {* |
172 make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
111 make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |