66 HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f)) |
66 HOLogic.mk_split (Abs (n, T, list_tupled_abs (v::vs) f)) |
67 |
67 |
68 fun mk_pointfree_expr t = |
68 fun mk_pointfree_expr t = |
69 let |
69 let |
70 val (vs, t'') = strip_ex (dest_Collect t) |
70 val (vs, t'') = strip_ex (dest_Collect t) |
71 val (eq::conjs) = HOLogic.dest_conj t'' |
71 val conjs = HOLogic.dest_conj t'' |
72 val f = if fst (HOLogic.dest_eq eq) = Bound (length vs) |
72 val is_the_eq = |
73 then snd (HOLogic.dest_eq eq) |
73 the_default false o (try (fn eq => fst (HOLogic.dest_eq eq) = Bound (length vs))) |
74 else raise TERM("mk_pointfree_expr", [t]); |
74 val SOME eq = find_first is_the_eq conjs |
75 val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs |
75 val f = snd (HOLogic.dest_eq eq) |
|
76 val conjs' = filter_out (fn t => eq = t) conjs |
|
77 val mems = map (apfst dest_Bound o HOLogic.dest_mem) conjs' |
76 val grouped_mems = AList.group (op =) mems |
78 val grouped_mems = AList.group (op =) mems |
77 fun mk_grouped_unions (i, T) = |
79 fun mk_grouped_unions (i, T) = |
78 case AList.lookup (op =) grouped_mems i of |
80 case AList.lookup (op =) grouped_mems i of |
79 SOME ts => foldr1 mk_inf ts |
81 SOME ts => foldr1 mk_inf ts |
80 | NONE => HOLogic.mk_UNIV T |
82 | NONE => HOLogic.mk_UNIV T |
105 THEN' (TRY o REPEAT_DETERM1 o |
107 THEN' (TRY o REPEAT_DETERM1 o |
106 (etac @{thm conjE} ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]})); |
108 (etac @{thm conjE} ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]})); |
107 |
109 |
108 val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]} |
110 val intro_Collect_tac = rtac @{thm iffD2[OF mem_Collect_eq]} |
109 THEN' REPEAT_DETERM1 o resolve_tac @{thms exI} |
111 THEN' REPEAT_DETERM1 o resolve_tac @{thms exI} |
110 THEN' (TRY o (rtac @{thm conjI})) |
112 THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI})) |
111 THEN' (TRY o hyp_subst_tac) |
113 THEN' (K (ALLGOALS (TRY o ((TRY o hyp_subst_tac) THEN' rtac @{thm refl})))) |
112 THEN' rtac @{thm refl}; |
|
113 |
114 |
114 val tac = |
115 val tac = |
115 let |
116 let |
116 val subset_tac1 = rtac @{thm subsetI} |
117 val subset_tac1 = rtac @{thm subsetI} |
117 THEN' dest_Collect_tac |
118 THEN' dest_Collect_tac |
123 ORELSE' atac)); |
124 ORELSE' atac)); |
124 |
125 |
125 val subset_tac2 = rtac @{thm subsetI} |
126 val subset_tac2 = rtac @{thm subsetI} |
126 THEN' dest_image_Sigma_tac |
127 THEN' dest_image_Sigma_tac |
127 THEN' intro_Collect_tac |
128 THEN' intro_Collect_tac |
128 THEN' REPEAT_DETERM o |
129 THEN' REPEAT_DETERM o (eresolve_tac @{thms IntD1 IntD2} ORELSE' atac); |
129 (rtac @{thm conjI} |
|
130 ORELSE' eresolve_tac @{thms IntD1 IntD2} |
|
131 ORELSE' atac); |
|
132 in |
130 in |
133 rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2 |
131 rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2 |
134 end; |
132 end; |
135 |
133 |
136 fun conv ctxt t = |
134 fun conv ctxt t = |