1 (* Title: BaseDefinitions/thmC.sml
3 (c) due to copyright terms
5 This structure could be dropped due to improved reflection in Isabelle;
6 but ThmC.sym_thm requires still an identifying string thm_id.
8 signature THEOREM_ISAC =
11 type id = ThmC_Def.id (* shortest possible *)
12 type long_id (* e.g. "Test.radd_left_commute"*)
14 val cut_id: string -> id
15 val long_id: T -> long_id
16 val string_of_thm: thm -> string
17 val string_of_thms: thm list -> string
18 val id_of_thm: thm -> id
20 val from_rule : Rule.rule -> T
21 val member': id list -> Rule.rule -> bool
23 val numerals_to_Free: thm -> thm
25 val is_sym: id -> bool
26 val thm_from_thy: theory -> ThmC_Def.id -> thm
30 val revert_sym_rule: theory -> Rule.rule -> Rule.rule
33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
34 val string_of_thm_in_thy: theory -> thm -> string
35 val id_drop_sym: id -> id
36 val make_sym_rule: Rule.rule -> Rule.rule
37 val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
38 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
39 val sym_thm: thm -> thm
40 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
44 structure ThmC(**): THEOREM_ISAC(**) =
48 (** types and conversions **)
51 type id = ThmC_Def.id;
52 type long_id = string;
54 fun long_id (thmID, _) = thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint
55 fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into Know_Store*)
57 val string_of_thm = ThmC_Def.string_of_thm;
58 val string_of_thms = ThmC_Def.string_of_thms;
60 fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;
61 fun of_thm thm = (id_of_thm thm, thm);
62 fun from_rule (Rule.Thm (id, thm)) = (id, thm)
63 | from_rule r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);
64 fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.to_ctxt thy) (Thm.prop_of thm);
65 fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm))
66 handle ERROR _ => false
69 (** convert Isabelle's numerals to ISAC's specific format, LEGACY **)
71 val numerals_to_Free = ThmC_Def.numerals_to_Free; (* numeral \<rightarrow> Free ("int", T) *)
74 (** handle symmetric equalities, generated by deriving input terms **)
77 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true
80 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id
83 (* get the theorem associated with the xstring-identifier;
84 if the identifier starts with "sym_" then swap lhs = rhs" around "=";
85 in case identifiers starting with "#" come from Eval and
86 get an ad-hoc theorem (containing numerals only) -- rejected here
88 fun thm_from_thy thy thmid =
89 case Symbol.explode thmid of
90 "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
91 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
92 | "s" :: "y" :: "m" :: "_" :: id =>
93 ((numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
95 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
97 thmid |> Global_Theory.get_thm thy |> numerals_to_Free
99 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
103 {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps,
104 hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm
105 val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
106 val prop' = case TermC.strip_imp_prems' prop of
107 NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
108 | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
110 Thm.assbl_thm derivation cert tags maxidx constraints shyps hyps tpairs prop'
113 fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
114 | make_sym_rule_set (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
115 Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
116 rules = rules, rew_ord = rew_ord, preconds = preconds}
117 | make_sym_rule_set (Rule_Set.Sequence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
118 Rule_Set.Sequence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
119 rules = rules, rew_ord = rew_ord, preconds = preconds}
120 | make_sym_rule_set (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
121 Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls,
122 prepat = prepat, rew_ord = rew_ord}
124 (* toggles sym_* and keeps "#:" for ad-hoc theorems *)
125 fun make_sym_rule (Rule.Thm (thmID, thm)) =
127 val thm' = sym_thm thm
128 val thmID' = case Symbol.explode thmID of
129 "s" :: "y" :: "m" :: "_" :: id => implode id
130 | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'
131 | _ => "sym_" ^ thmID
132 in Rule.Thm (thmID', thm') end
133 | make_sym_rule (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
134 | make_sym_rule r = raise ERROR ("make_sym_rule: not for " ^ Rule.to_string r)
136 fun revert_sym_rule thy (Rule.Thm (id, thm)) =
137 if is_sym (cut_id id)
140 val id' = id_drop_sym id
141 val thm' = thm_from_thy thy id'
142 val id'' = Thm.get_name_hint thm'
143 in Rule.Thm (id'', thm') end
144 else Rule.Thm (Thm.get_name_hint thm, thm)
145 | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)