71 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
71 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
72 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
72 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
73 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
73 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
74 ML {* ObjectLogic.rulify t_b *} |
74 ML {* ObjectLogic.rulify t_b *} |
75 |
75 |
|
76 thm fresh_def |
|
77 thm supp_def |
|
78 |
76 local_setup {* |
79 local_setup {* |
77 make_const_def @{binding lfresh} @{term "fresh :: 'a \<Rightarrow> rlam \<Rightarrow> bool"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #> |
|
78 make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
80 make_const_def @{binding lperm} @{term "perm :: ('a \<times> 'a) list \<Rightarrow> rlam \<Rightarrow> rlam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd |
79 *} |
81 *} |
80 |
82 |
81 ML {* val consts = @{const_name fresh} :: @{const_name perm} :: consts *} |
83 ML {* val consts = @{const_name perm} :: consts *} |
82 ML {* val defs = @{thms lfresh_def 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} *} |
|
86 ML {* val t_a = atomize_thm t_u *} |
|
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 |
83 ML {* val t_t = Toplevel.program (fn () => repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms) *} |
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 *} |
|
157 |
84 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
158 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
85 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
159 ML {* val t_c = simp_allex_prs @{context} quot t_l *} |
86 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
160 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
87 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
161 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_c *} |
88 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
162 ML {* val t_b = MetaSimplifier.rewrite_rule [reps_same] t_d *} |