23 fun makeHthm (part : string, thyID : Rule.thyID) (thm : thm) = |
23 fun makeHthm (part : string, thyID : Rule.thyID) (thm : thm) = |
24 let val theID = [part, thyID, "Theorems"] @ [Celem.thmID_of_derivation_name' thm] : Celem.theID |
24 let val theID = [part, thyID, "Theorems"] @ [Celem.thmID_of_derivation_name' thm] : Celem.theID |
25 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [], |
25 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [], |
26 mathauthors = ["isac-team"], fillpats = [], thm = thm}) |
26 mathauthors = ["isac-team"], fillpats = [], thm = thm}) |
27 end; |
27 end; |
28 fun makeHrls (part : string) (rls' : Rule_Set.rls', thy_rls as (thyID, rls): Rule.thyID * Rule_Set.rls) = |
28 fun makeHrls (part : string) (rls' : Rule_Set.rls', thy_rls as (thyID, rls): Rule.thyID * Rule_Set.T) = |
29 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID |
29 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID |
30 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [], |
30 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [], |
31 mathauthors = ["isac-team"], thy_rls = thy_rls}) |
31 mathauthors = ["isac-team"], thy_rls = thy_rls}) |
32 end; |
32 end; |
33 fun makeHcal (part : string, thyID : Rule.thyID) (calID, cal) = |
33 fun makeHcal (part : string, thyID : Rule.thyID) (calID, cal) = |
50 val thmDeriv' = Thm.get_name_hint thm' |
50 val thmDeriv' = Thm.get_name_hint thm' |
51 in Rule.Thm (thmDeriv', thm') end |
51 in Rule.Thm (thmDeriv', thm') end |
52 else Rule.Thm (Thm.get_name_hint thm, thm) |
52 else Rule.Thm (Thm.get_name_hint thm, thm) |
53 |
53 |
54 (* get all theorems from the list of rule-sets (defined in Knowledge) *) |
54 (* get all theorems from the list of rule-sets (defined in Knowledge) *) |
55 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.rls' * (Rule.theory' * Rule_Set.rls)) list) |
55 fun thms_of_rlss thy rlss = (rlss : (Rule_Set.rls' * (Rule.theory' * Rule_Set.T)) list) |
56 |> map (Rtools.thms_of_rls o #2 o #2) |
56 |> map (Rtools.thms_of_rls o #2 o #2) |
57 |> flat |
57 |> flat |
58 |> map (revert_sym thy) |
58 |> map (revert_sym thy) |
59 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm)) |
59 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm)) |
60 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) |
60 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2) |
62 |
62 |
63 (* collect all thydata defined in in a theory *) |
63 (* collect all thydata defined in in a theory *) |
64 |
64 |
65 fun collect_thms part thy = |
65 fun collect_thms part thy = |
66 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy)) |
66 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy)) |
67 fun collect_rlss part rlss thys = (rlss : (Rule_Set.rls' * (Rule.thyID * Rule_Set.rls)) list) |
67 fun collect_rlss part rlss thys = (rlss : (Rule_Set.rls' * (Rule.thyID * Rule_Set.T)) list) |
68 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID) |
68 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID) |
69 |> map (makeHrls part) |
69 |> map (makeHrls part) |
70 fun collect_cals (part, thy') = |
70 fun collect_cals (part, thy') = |
71 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*) |
71 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*) |
72 in map (makeHcal (part, thy')) cals end; |
72 in map (makeHcal (part, thy')) cals end; |