equal
deleted
inserted
replaced
65 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
65 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
66 end |
66 end |
67 |
67 |
68 val fresh_prem = |
68 val fresh_prem = |
69 case binders of |
69 case binders of |
70 [] => [] (* case: no binders *) |
70 [] => [] (* case: no binders *) |
71 | binders => binders (* case: binders *) |
71 | _ => binders (* case: binders *) |
72 |> map prep_binder |
72 |> map prep_binder |
73 |> fold_union_env tys |
73 |> fold_union_env tys |
74 |> (fn t => mk_fresh_star t c) |
74 |> (fn t => mk_fresh_star t c) |
75 |> HOLogic.mk_Trueprop |
75 |> HOLogic.mk_Trueprop |
76 |> single |
76 |> single |
79 end |
79 end |
80 *} |
80 *} |
81 |
81 |
82 |
82 |
83 ML {* |
83 ML {* |
|
84 (* derives the freshness theorem that there exists a p, such that |
|
85 (p o as) #* (c, t1,\<dots>, tn) *) |
84 fun fresh_thm ctxt c parms binders bn_finite_thms = |
86 fun fresh_thm ctxt c parms binders bn_finite_thms = |
85 let |
87 let |
86 fun prep_binder (opt, i) = |
88 fun prep_binder (opt, i) = |
87 case opt of |
89 case opt of |
88 NONE => setify ctxt (nth parms i) |
90 NONE => setify ctxt (nth parms i) |
108 in |
110 in |
109 Goal.prove ctxt [] [] goal |
111 Goal.prove ctxt [] [] goal |
110 (K (HEADGOAL (rtac @{thm at_set_avoiding1} |
112 (K (HEADGOAL (rtac @{thm at_set_avoiding1} |
111 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
113 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
112 end |
114 end |
113 |
115 *} |
|
116 |
|
117 ML {* |
|
118 (* derives abs_eq theorems of the form Exists s. [as].t = [p o as].s *) |
114 fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) = |
119 fun abs_eq_thm ctxt fprops p parms bn_finite_thms (BC (bmode, binders, bodies)) = |
115 case binders of |
120 case binders of |
116 [] => [] |
121 [] => [] |
117 | binders => |
122 | _ => |
118 let |
123 let |
119 val binder_trm = Nominal_Dt_Alpha.comb_binders ctxt bmode parms binders |
124 val binder_trm = comb_binders ctxt bmode parms binders |
120 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
125 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
121 val body_ty = fastype_of body_trm |
126 val body_ty = fastype_of body_trm |
122 |
127 |
123 val (abs_name, binder_ty, abs_ty) = |
128 val (abs_name, binder_ty, abs_ty) = |
124 case bmode of |
129 case bmode of |
141 (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
146 (K (HEADGOAL (resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
142 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] |
147 THEN_ALL_NEW (simp_tac (HOL_basic_ss addsimps ss) THEN' TRY o simp_tac HOL_ss))))] |
143 end |
148 end |
144 *} |
149 *} |
145 |
150 |
146 ML {* |
151 |
147 fun partitions [] [] = [] |
152 (* FIXME: use pure cterm functions *) |
148 | partitions xs (i :: js) = |
|
149 let |
|
150 val (head, tail) = chop i xs |
|
151 in |
|
152 head :: partitions tail js |
|
153 end |
|
154 *} |
|
155 |
|
156 |
|
157 ML {* |
153 ML {* |
158 fun mk_cperm ctxt p ctrm = |
154 fun mk_cperm ctxt p ctrm = |
159 mk_perm (term_of p) (term_of ctrm) |
155 mk_perm (term_of p) (term_of ctrm) |
160 |> cterm_of (ProofContext.theory_of ctxt) |
156 |> cterm_of (ProofContext.theory_of ctxt) |
161 *} |
157 *} |
175 val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} |
171 val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} |
176 val (([(_, fperm)], fprops), ctxt') = Obtain.result |
172 val (([(_, fperm)], fprops), ctxt') = Obtain.result |
177 (K (EVERY1 [etac exE, |
173 (K (EVERY1 [etac exE, |
178 full_simp_tac (HOL_basic_ss addsimps ss), |
174 full_simp_tac (HOL_basic_ss addsimps ss), |
179 REPEAT o (etac conjE)])) [fthm] ctxt |
175 REPEAT o (etac conjE)])) [fthm] ctxt |
|
176 |
|
177 val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses) |
|
178 |
|
179 val _ = tracing ("test") |
180 (* |
180 (* |
181 val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops)) |
181 val _ = tracing ("fprop:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) fprops)) |
182 *) |
182 *) |
183 val abs_eqs = flat (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms) bclauses) |
|
184 (* |
183 (* |
185 val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs)) |
184 val _ = tracing ("abs_eqs:\n" ^ cat_lines (map (Syntax.string_of_term ctxt' o prop_of) abs_eqs)) |
186 *) |
185 *) |
187 in |
186 in |
188 (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*) |
187 (*HEADGOAL (rtac prem THEN' RANGE [K all_tac, simp_tac (HOL_basic_ss addsimps prems)])*) |