61 None => raise ERROR |
61 None => raise ERROR |
62 | Some (_, A) => if matches (Logic.incr_indexes ([], maxidx) A, t) then () else raise ERROR) |
62 | Some (_, A) => if matches (Logic.incr_indexes ([], maxidx) A, t) then () else raise ERROR) |
63 end handle ERROR => error ("Bad non-emptiness theorem " ^ Display.string_of_thm thm ^ |
63 end handle ERROR => error ("Bad non-emptiness theorem " ^ Display.string_of_thm thm ^ |
64 "\nfor set " ^ quote (Display.string_of_cterm cset)); |
64 "\nfor set " ^ quote (Display.string_of_cterm cset)); |
65 |
65 |
66 fun goal_nonempty cset = |
66 fun goal_nonempty ex cset = |
67 let |
67 let |
68 val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset; |
68 val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset; |
69 val T = HOLogic.dest_setT setT; |
69 val T = HOLogic.dest_setT setT; |
70 in Thm.cterm_of sign (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), A))) end; |
70 val tm = |
|
71 if ex then HOLogic.mk_exists ("x", T, HOLogic.mk_mem (Free ("x", T), A)) |
|
72 else HOLogic.mk_mem (Var (("x", maxidx + 1), T), A); (*old-style version*) |
|
73 in Thm.cterm_of sign (HOLogic.mk_Trueprop tm) end; |
71 |
74 |
72 fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) = |
75 fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) = |
73 let |
76 let |
74 val is_def = Logic.is_equals o #prop o Thm.rep_thm; |
77 val is_def = Logic.is_equals o #prop o Thm.rep_thm; |
75 val thms = PureThy.get_thmss thy witn_names @ witn_thms; |
78 val thms = PureThy.get_thmss thy witn_names @ witn_thms; |
77 TRY (rewrite_goals_tac (filter is_def thms)) THEN |
80 TRY (rewrite_goals_tac (filter is_def thms)) THEN |
78 TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN |
81 TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN |
79 if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac))); |
82 if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac))); |
80 in |
83 in |
81 message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); |
84 message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); |
82 prove_goalw_cterm [] (goal_nonempty cset) (K [tac]) |
85 prove_goalw_cterm [] (goal_nonempty false cset) (K [tac]) |
83 end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset)); |
86 end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset)); |
84 |
87 |
85 |
88 |
86 (* prepare_typedef *) |
89 (* prepare_typedef *) |
87 |
90 |
185 |
188 |
186 |
189 |
187 (* typedef_proof interface *) |
190 (* typedef_proof interface *) |
188 |
191 |
189 fun typedef_attribute cset do_typedef (thy, thm) = |
192 fun typedef_attribute cset do_typedef (thy, thm) = |
190 (check_nonempty cset thm; (thy |> do_typedef, thm)); |
193 (check_nonempty cset (thm RS (select_eq_Ex RS iffD2)); (thy |> do_typedef, thm)); |
191 |
194 |
192 fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy = |
195 fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy = |
193 let |
196 let |
194 val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy; |
197 val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy; |
195 val goal = Thm.term_of (goal_nonempty cset); |
198 val goal = Thm.term_of (goal_nonempty true cset); |
196 in |
199 in |
197 thy |
200 thy |
198 |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int |
201 |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int |
199 end; |
202 end; |
200 |
203 |