47 * entrypoint is specialized for interactive use, since it closes the theory |
47 * entrypoint is specialized for interactive use, since it closes the theory |
48 * after making the definition. This allows later interactive definitions to |
48 * after making the definition. This allows later interactive definitions to |
49 * refer to previous ones. The name for the new theory is automatically |
49 * refer to previous ones. The name for the new theory is automatically |
50 * generated from the name of the argument theory. |
50 * generated from the name of the argument theory. |
51 *---------------------------------------------------------------------------*) |
51 *---------------------------------------------------------------------------*) |
|
52 |
|
53 |
|
54 (*--------------------------------------------------------------------------- |
|
55 * TFL attempts to make definitions where the lhs is a variable. Isabelle |
|
56 * wants it to be a constant, so here we map it to a constant. Moreover, the |
|
57 * theory should already have the constant, so we refrain from adding the |
|
58 * constant to the theory. We just add the axiom and return the theory. |
|
59 *---------------------------------------------------------------------------*) |
52 local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection)) |
60 local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection)) |
53 val Const(eeq_name, ty) = eeq |
61 val Const(eeq_name, ty) = eeq |
54 val prop = #2 (S.strip_type ty) |
62 val prop = #2 (S.strip_type ty) |
55 in |
63 in |
56 fun make_definition parent s tm = |
64 fun make_definition parent s tm = |
57 let val {lhs,rhs} = S.dest_eq tm |
65 let val {lhs,rhs} = S.dest_eq tm |
58 val {Name,Ty} = S.dest_var lhs |
66 val {Name,Ty} = S.dest_var lhs |
59 val lhs1 = S.mk_const{Name = Name, Ty = Ty} |
67 val lhs1 = S.mk_const{Name = Name, Ty = Ty} |
60 val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} |
68 val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop} |
61 val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) |
69 val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *) |
62 val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent |
70 val (_, tm', _) = Sign.infer_types (sign_of parent) |
63 val thry2 = add_defs_i [(s,dtm)] thry1 |
71 (K None) (K None) [] true ([dtm],propT) |
64 val parent_names = map ! (stamps_of_thy parent) |
72 val new_thy = add_defs_i [(s,tm')] parent |
65 val newthy_name = variant parent_names (hd parent_names) |
|
66 val new_thy = add_thyname newthy_name thry2 |
|
67 in |
73 in |
68 ((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy) |
74 (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy) |
69 end |
75 end; |
70 end; |
76 end; |
71 |
|
72 |
77 |
73 (*--------------------------------------------------------------------------- |
78 (*--------------------------------------------------------------------------- |
74 * Utility routine. Insert into list ordered by the key (a string). If two |
79 * Utility routine. Insert into list ordered by the key (a string). If two |
75 * keys are equal, the new element replaces the old. A more efficient option |
80 * keys are equal, the new element replaces the old. A more efficient option |
76 * for the future is needed. In fact, having the list of datatype facts be |
81 * for the future is needed. In fact, having the list of datatype facts be |