equal
deleted
inserted
replaced
27 val _ = ba 1 |
27 val _ = ba 1 |
28 in |
28 in |
29 val helper = Goals.result() |
29 val helper = Goals.result() |
30 end |
30 end |
31 |
31 |
32 (* Akin to HOLogic.exists_const *) |
|
33 fun choice_const T = Const("Hilbert_Choice.Eps",(T-->HOLogic.boolT)-->T) |
|
34 |
|
35 (* Actual code *) |
32 (* Actual code *) |
36 |
33 |
37 local |
34 local |
38 fun mk_definitional [] arg = arg |
35 fun mk_definitional [] arg = arg |
39 | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = |
36 | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = |
43 val ctype = domain_type (type_of P) |
40 val ctype = domain_type (type_of P) |
44 val cname_full = Sign.intern_const (sign_of thy) cname |
41 val cname_full = Sign.intern_const (sign_of thy) cname |
45 val cdefname = if thname = "" |
42 val cdefname = if thname = "" |
46 then Thm.def_name (Sign.base_name cname) |
43 then Thm.def_name (Sign.base_name cname) |
47 else thname |
44 else thname |
48 val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $ P) |
45 val def_eq = Logic.mk_equals (Const(cname_full,ctype), |
|
46 HOLogic.choice_const ctype $ P) |
49 val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy |
47 val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy |
50 val thm' = [thm,hd thms] MRS helper |
48 val thm' = [thm,hd thms] MRS helper |
51 in |
49 in |
52 mk_definitional cos (thy',thm') |
50 mk_definitional cos (thy',thm') |
53 end |
51 end |