1011 and in the theory's HTML file*) |
1011 and in the theory's HTML file*) |
1012 fun store_thm (name, thm) = |
1012 fun store_thm (name, thm) = |
1013 let |
1013 let |
1014 val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, |
1014 val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, |
1015 theory, thms, methods, data}) = |
1015 theory, thms, methods, data}) = |
1016 thyinfo_of_sign (#sign (rep_thm thm)); |
1016 thyinfo_of_sign (#sign (rep_thm thm)) |
1017 |
1017 |
1018 val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) |
1018 val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) |
1019 handle Symtab.DUPLICATE s => |
1019 handle Symtab.DUPLICATE s => |
1020 (if eq_thm (the (Symtab.lookup (thms, name)), thm) then |
1020 (if eq_thm (the (Symtab.lookup (thms, name)), thm) then |
1021 (writeln ("Warning: Theory database already contains copy of\ |
1021 (writeln ("Warning: Theory database already contains copy of\ |
1042 escape (explode (string_of_thm (freeze thm))) ^ |
1042 escape (explode (string_of_thm (freeze thm))) ^ |
1043 "</PRE><P>\n") |
1043 "</PRE><P>\n") |
1044 ) |
1044 ) |
1045 | None => () |
1045 | None => () |
1046 end; |
1046 end; |
|
1047 |
|
1048 (*Return version with trivial proof object; store original version *) |
|
1049 val thm' = Thm.name_thm (the theory, name, thm) handle OPTION _ => thm |
1047 in |
1050 in |
1048 loaded_thys := Symtab.update |
1051 loaded_thys := Symtab.update |
1049 ((thy_name, ThyInfo {path = path, children = children, parents = parents, |
1052 ((thy_name, ThyInfo {path = path, children = children, parents = parents, |
1050 thy_time = thy_time, ml_time = ml_time, |
1053 thy_time = thy_time, ml_time = ml_time, |
1051 theory = theory, thms = thms', |
1054 theory = theory, thms = thms', |
1052 methods = methods, data = data}), |
1055 methods = methods, data = data}), |
1053 !loaded_thys); |
1056 !loaded_thys); |
1054 thm_to_html (); |
1057 thm_to_html (); |
1055 if duplicate then thm else store_thm_db (name, thm) |
1058 if duplicate then thm' else store_thm_db (name, thm') |
1056 end; |
1059 end; |
1057 |
1060 |
1058 (*Store result of proof in loaded_thys and as ML value*) |
1061 (*Store result of proof in loaded_thys and as ML value*) |
1059 |
1062 |
1060 val qed_thm = ref flexpair_def(*dummy*); |
1063 val qed_thm = ref flexpair_def(*dummy*); |
1061 |
1064 |
1062 fun bind_thm (name, thm) = |
1065 fun bind_thm (name, thm) = |
1063 (qed_thm := standard thm; |
1066 (qed_thm := store_thm (name, (standard thm)); |
1064 store_thm (name, !qed_thm); |
|
1065 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1067 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1066 |
1068 |
1067 fun qed name = |
1069 fun qed name = |
1068 (qed_thm := result (); |
1070 (qed_thm := store_thm (name, result ()); |
1069 store_thm (name, !qed_thm); |
|
1070 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1071 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1071 |
1072 |
1072 fun qed_goal name thy agoal tacsf = |
1073 fun qed_goal name thy agoal tacsf = |
1073 (qed_thm := prove_goal thy agoal tacsf; |
1074 (qed_thm := store_thm (name, prove_goal thy agoal tacsf); |
1074 store_thm (name, !qed_thm); |
|
1075 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1075 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1076 |
1076 |
1077 fun qed_goalw name thy rths agoal tacsf = |
1077 fun qed_goalw name thy rths agoal tacsf = |
1078 (qed_thm := prove_goalw thy rths agoal tacsf; |
1078 (qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf); |
1079 store_thm (name, !qed_thm); |
|
1080 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1079 use_string ["val " ^ name ^ " = !qed_thm;"]); |
1081 |
1080 |
1082 |
1081 |
1083 (** Retrieve theorems **) |
1082 (** Retrieve theorems **) |
1084 |
1083 |
1089 |
1088 |
1090 fun thmtab_of_name name = |
1089 fun thmtab_of_name name = |
1091 let val ThyInfo {thms, ...} = the (get_thyinfo name); |
1090 let val ThyInfo {thms, ...} = the (get_thyinfo name); |
1092 in thms end; |
1091 in thms end; |
1093 |
1092 |
1094 (*Get a stored theorem specified by theory and name*) |
1093 (*Get a stored theorem specified by theory and name. |
|
1094 Derivation has the form Theorem(thy,name). *) |
1095 fun get_thm thy name = |
1095 fun get_thm thy name = |
1096 let fun get [] [] searched = |
1096 let fun get [] [] searched = |
1097 raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) |
1097 raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) |
1098 | get [] ng searched = |
1098 | get [] ng searched = |
1099 get (ng \\ searched) [] searched |
1099 get (ng \\ searched) [] searched |
1100 | get (t::ts) ng searched = |
1100 | get (t::ts) ng searched = |
1101 (case Symtab.lookup (thmtab_of_name t, name) of |
1101 (case Symtab.lookup (thmtab_of_name t, name) of |
1102 Some thm => thm |
1102 Some thm => Thm.name_thm(thy,name,thm) |
1103 | None => get ts (ng union (parents_of_name t)) (t::searched)); |
1103 | None => get ts (ng union (parents_of_name t)) (t::searched)); |
1104 |
1104 |
1105 val (tname, _) = thyinfo_of_sign (sign_of thy); |
1105 val (tname, _) = thyinfo_of_sign (sign_of thy); |
1106 in get [tname] [] [] end; |
1106 in get [tname] [] [] end; |
1107 |
1107 |
1108 (*Get stored theorems of a theory*) |
1108 (*Get stored theorems of a theory (original derivations) *) |
1109 val thms_of = Symtab.dest o thmtab_of_thy; |
1109 val thms_of = Symtab.dest o thmtab_of_thy; |
1110 |
1110 |
1111 |
1111 |
1112 |
1112 |
1113 |
1113 |