1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Jun 04 16:35:11 2014 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Jun 04 17:20:40 2014 +0200
1.3 @@ -74,28 +74,28 @@
1.4 val thy = @{theory};
1.5
1.6 (** theory elements for transfer into html **)
1.7 +store_thes
1.8 + [make_thy @{theory}
1.9 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.10 + make_isa @{theory} ("IsacKnowledge", "Theorems")
1.11 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.12 + make_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
1.13 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.14 + make_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
1.15 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.16 + make_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
1.17 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.18 + make_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
1.19 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.20 + make_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
1.21 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.22 + make_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
1.23 + ["Walther Neuper 2005 supported by a grant from NMI Austria"],
1.24 + make_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
1.25 + ["Walther Neuper 2005 supported by a grant from NMI Austria"]
1.26 + ]
1.27 +*}
1.28
1.29 -store_isa ["IsacKnowledge"] [];
1.30 -store_thy thy
1.31 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.32 -store_isa ["IsacKnowledge", theory2thyID thy, "Theorems"]
1.33 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.34 -store_thm thy "IsacKnowledge" ("Belastung_Querkraft", prop_of @{thm Belastung_Querkraft})
1.35 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.36 -store_thm thy "IsacKnowledge" ("Moment_Neigung", prop_of @{thm Moment_Neigung})
1.37 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.38 -store_thm thy "IsacKnowledge" ("Moment_Querkraft", prop_of @{thm Moment_Querkraft})
1.39 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.40 -store_thm thy "IsacKnowledge" ("Neigung_Moment", prop_of @{thm Neigung_Moment})
1.41 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.42 -store_thm thy "IsacKnowledge" ("Querkraft_Belastung", prop_of @{thm Querkraft_Belastung})
1.43 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.44 -store_thm thy "IsacKnowledge" ("Querkraft_Moment", prop_of @{thm Querkraft_Moment})
1.45 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.46 -store_thm thy "IsacKnowledge" ("make_fun_explicit", prop_of @{thm make_fun_explicit})
1.47 - ["Walther Neuper 2005 supported by a grant from NMI Austria"];
1.48 -
1.49 -*}
1.50 (** problems **)
1.51 setup {* KEStore_Elems.add_pbts
1.52 [(prep_pbt thy "pbl_bieg" [] e_pblID
2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Jun 04 16:35:11 2014 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Jun 04 17:20:40 2014 +0200
2.3 @@ -101,26 +101,28 @@
2.4
2.5 ML {*
2.6 (*/========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============\*)
2.7 -store_thy @{theory "Diff"} ["Isabelle2011-->12"];
2.8 -store_isa ["IsacKnowledge","Diff","Theorems"] ["Isabelle2011-->12"];
2.9 -store_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
2.10 - ["Isabelle2011-->12"];
2.11 -store_thm @{theory "Diff"} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})
2.12 - ["Isabelle2011-->12"];
2.13 -store_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
2.14 - ["Isabelle2011-->12"];
2.15 -store_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
2.16 - ["Isabelle2011-->12"];
2.17 -store_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
2.18 - ["Isabelle2011-->12"];
2.19 -store_isa ["IsacKnowledge","Diff","Rulesets"] ["Isabelle2011-->12"];
2.20 -store_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"];
2.21 +store_thes
2.22 + [make_thy @{theory "Diff"} ["Isabelle2011-->12"],
2.23 + make_isa @{theory "Diff"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
2.24 + make_thm @{theory "Diff"} "IsacKnowledge" ("diff_sin_chain", prop_of @{thm diff_sin_chain})
2.25 + ["Isabelle2011-->12"],
2.26 + make_thm @{theory "Diff"} "IsacKnowledge" ("diff_cos_chain", prop_of @{thm diff_cos_chain})
2.27 + ["Isabelle2011-->12"],
2.28 + make_thm @{theory "Diff"} "IsacKnowledge" ("diff_pow_chain", prop_of @{thm diff_pow_chain})
2.29 + ["Isabelle2011-->12"],
2.30 + make_thm @{theory "Diff"} "IsacKnowledge" ("diff_ln_chain", prop_of @{thm diff_ln_chain})
2.31 + ["Isabelle2011-->12"],
2.32 + make_thm @{theory "Diff"} "IsacKnowledge" ("diff_exp_chain", prop_of @{thm diff_exp_chain})
2.33 + ["Isabelle2011-->12"],
2.34
2.35 -store_thy @{theory "Test"} ["Isabelle2011-->12"];
2.36 -store_isa ["IsacKnowledge","Test","Theorems"] ["Isabelle2011-->12"];
2.37 -store_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute
2.38 -})
2.39 - ["Isabelle2011-->12"];
2.40 + make_isa @{theory "Diff"} ("IsacKnowledge", "Rulesets") ["Isabelle2011-->12"],
2.41 + make_rls @{theory "Diff"} norm_diff ["Isabelle2011-->12"],
2.42 +
2.43 + make_thy @{theory "Test"} ["Isabelle2011-->12"],
2.44 + make_isa @{theory "Test"} ("IsacKnowledge", "Theorems") ["Isabelle2011-->12"],
2.45 + make_thm @{theory "Test"} "IsacKnowledge" ("radd_left_commute", prop_of @{thm radd_left_commute})
2.46 + ["Isabelle2011-->12"]
2.47 + ]
2.48 (*\========= inhibit exn WN130620 (1.4.1) below: fill thehier ==============/*)
2.49 *}
2.50
2.51 @@ -140,7 +142,8 @@
2.52 *}
2.53
2.54 ML {*
2.55 -insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
2.56 +store_thes
2.57 + [insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
2.58 ([("fill-d_d-arg",
2.59 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
2.60 ("fill-both-args",
2.61 @@ -150,7 +153,8 @@
2.62 ("fill-inner-deriv",
2.63 parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
2.64 ("fill-all",
2.65 - parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
2.66 + parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list)
2.67 + ]
2.68 *}
2.69
2.70 subsubsection {* Error patterns for calculation with rationals *}
3.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Jun 04 16:35:11 2014 +0200
3.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Wed Jun 04 17:20:40 2014 +0200
3.3 @@ -291,8 +291,9 @@
3.4 (["IsacKnowledge", theory2thyID Biegelinie.thy, "Theorems"],
3.5 ["Walther Neuper 2005 supported by a grant from NMI Austria"]);
3.6 *)
3.7 -fun store_isa (theID : theID) (mathauthors : authors) =
3.8 - let val guh = case theID of
3.9 +fun make_isa thy (part, thypart) (mathauthors : authors) =
3.10 + let val theID = [part, string_of_thy thy, thypart]
3.11 + val guh = case theID of
3.12 [part] => part2guh theID
3.13 | [part, thyID, thypart] => thypart2guh theID
3.14 val theID = guh2theID guh
3.15 @@ -300,20 +301,18 @@
3.16 coursedesign = [],
3.17 mathauthors = mathauthors,
3.18 html = ""}
3.19 - in (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.20 - thehier := insrt theID the theID (! thehier) end;
3.21 -
3.22 -fun store_thy thy (mathauthors : authors) =
3.23 + in (the, theID) end
3.24 +
3.25 +fun make_thy thy (mathauthors : authors) =
3.26 let val guh = thy2guh ["IsacKnowledge", theory2thyID thy]
3.27 val theID = guh2theID guh
3.28 val the = Html {guh = guh,
3.29 coursedesign = [],
3.30 mathauthors = mathauthors,
3.31 html = ""}
3.32 - in (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.33 - thehier := insrt theID the theID (! thehier) end;
3.34 -
3.35 -fun store_thm thy part (thmID : thmID, thm) (mathauthors : authors) =
3.36 + in (the, theID) end
3.37 +
3.38 +fun make_thm thy part (thmID : thmID, thm) (mathauthors : authors) =
3.39 let
3.40 val guh = thm2guh (part, theory2thyID thy) thmID
3.41 val theID = guh2theID guh
3.42 @@ -322,29 +321,29 @@
3.43 mathauthors = mathauthors,
3.44 fillpats = [],
3.45 thm = thm}
3.46 - in (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.47 - thehier := insrt theID the theID (! thehier) end;
3.48 + in (the, theID) end
3.49
3.50 -(*WN120512 DESIGN TODO: build thehier already in respective theories*)
3.51 -fun insert_fillpats thy part (thmID : thmID, thm) fillpats =
3.52 +(*WN120512 DESIGN TODO: build thehier already in respective theories
3.53 +fun make_fillpats thy part (thmID : thmID, thm) fillpats =
3.54 let
3.55 val guh = thm2guh (part, theory2thyID thy) thmID
3.56 val theID = guh2theID guh
3.57 val Hthm {guh, coursedesign, mathauthors, thm, ...} = get_the theID
3.58 val the = Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
3.59 fillpats = fillpats, thm = thm}
3.60 - in thehier := insrt theID the theID (! thehier) end;
3.61 + in (the, theID) end
3.62 +WAS DEFINDE TWICE: here as insert_fillpats; below still the same id*)
3.63
3.64 -fun store_rls thy rls (mathauthors : authors) =
3.65 +fun make_rls thy rls (mathauthors : authors) =
3.66 let
3.67 val guh = rls2guh ("IsacKnowledge", theory2thyID thy) ((#id o rep_rls) rls)
3.68 val theID = guh2theID guh
3.69 val the = Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
3.70 thy_rls = (theory2thyID thy, rls)}
3.71 (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.72 - in thehier := insrt theID the theID (! thehier) end;
3.73 + in (the, theID) end
3.74
3.75 -fun store_cal thy cal (mathauthors : authors) =
3.76 +fun make_cal thy cal (mathauthors : authors) =
3.77 let val guh = cal2guh ("IsacKnowledge", theory2thyID thy)
3.78 ("TODO store_cal")
3.79 val theID = guh2theID guh
3.80 @@ -352,10 +351,9 @@
3.81 coursedesign = [],
3.82 mathauthors = mathauthors,
3.83 calc = cal}
3.84 - in (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.85 - thehier := insrt theID the theID (! thehier) end;
3.86 + in (the, theID) end
3.87
3.88 -fun store_ord thy ord (mathauthors : authors) =
3.89 +fun make_ord thy ord (mathauthors : authors) =
3.90 let val guh = ord2guh ("IsacKnowledge", theory2thyID thy)
3.91 ("TODO store_ord")
3.92 val theID = guh2theID guh
3.93 @@ -363,8 +361,13 @@
3.94 coursedesign = [],
3.95 mathauthors = mathauthors,
3.96 ord = ord}
3.97 - in (*needs no (!check_guhs_unique) because guh is generated automatically*)
3.98 - thehier := insrt theID the theID (! thehier) end;
3.99 + in (the, theID) end
3.100 +
3.101 +(*needs no (!check_guhs_unique) because guh is generated automatically*)
3.102 +fun store_thes thes thy =
3.103 + let
3.104 + fun store_the (the, theID) thy = thehier := insrt theID the theID (get_thes ())
3.105 + in fold store_the thes () end
3.106
3.107 fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
3.108 Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
3.109 @@ -398,11 +401,12 @@
3.110 val hthm = get_the theID
3.111 val hthm' = update_hthm hthm fillpats
3.112 handle ERROR _ => error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
3.113 - in thehier := insrt theID hthm' theID (! thehier) end;
3.114 + in (hthm', theID) end
3.115
3.116 fun insert_errpatIDs theID errpatIDs =
3.117 let
3.118 val hrls = get_the theID
3.119 val hrls' = update_hrls hrls errpatIDs
3.120 handle ERROR _ => error ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
3.121 - in thehier := insrt theID hrls' theID (! thehier) end;
3.122 + in (hrls', theID) end
3.123 +