src/HOL/Tools/typedef_package.ML
changeset 7481 d44c77be268c
parent 7152 44d46a112127
child 8100 6186ee807f2e
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Sep 04 21:13:01 1999 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Sep 04 21:13:55 1999 +0200
     1.3 @@ -63,11 +63,14 @@
     1.4    end handle ERROR => error ("Bad non-emptiness theorem " ^ Display.string_of_thm thm ^
     1.5      "\nfor set " ^ quote (Display.string_of_cterm cset));
     1.6  
     1.7 -fun goal_nonempty cset =
     1.8 +fun goal_nonempty ex cset =
     1.9    let
    1.10      val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset;
    1.11      val T = HOLogic.dest_setT setT;
    1.12 -  in Thm.cterm_of sign (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), A))) end;
    1.13 +    val tm =
    1.14 +      if ex then HOLogic.mk_exists ("x", T, HOLogic.mk_mem (Free ("x", T), A))
    1.15 +      else HOLogic.mk_mem (Var (("x", maxidx + 1), T), A);   (*old-style version*)
    1.16 +  in Thm.cterm_of sign (HOLogic.mk_Trueprop tm) end;
    1.17  
    1.18  fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) =
    1.19    let
    1.20 @@ -79,7 +82,7 @@
    1.21        if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.22    in
    1.23      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.24 -    prove_goalw_cterm [] (goal_nonempty cset) (K [tac])
    1.25 +    prove_goalw_cterm [] (goal_nonempty false cset) (K [tac])
    1.26    end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.27  
    1.28  
    1.29 @@ -187,12 +190,12 @@
    1.30  (* typedef_proof interface *)
    1.31  
    1.32  fun typedef_attribute cset do_typedef (thy, thm) =
    1.33 -  (check_nonempty cset thm; (thy |> do_typedef, thm));
    1.34 +  (check_nonempty cset (thm RS (select_eq_Ex RS iffD2)); (thy |> do_typedef, thm));
    1.35  
    1.36  fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
    1.37    let
    1.38      val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
    1.39 -    val goal = Thm.term_of (goal_nonempty cset);
    1.40 +    val goal = Thm.term_of (goal_nonempty true cset);
    1.41    in
    1.42      thy
    1.43      |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int