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 is_sym: id -> bool
24 val thm_from_thy: theory -> ThmC_Def.id -> thm
26 val revert_sym_rule: theory -> Rule.rule -> Rule.rule
28 val make_rule: Proof.context -> bool -> string * Position.T -> Rule_Def.rule
31 val dest_eq_concl: thm -> term * term
32 val string_of_thm_in_thy: theory -> thm -> string
33 val id_drop_sym: id -> id
35 val make_sym_rule: Rule.rule -> Rule.rule
36 val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
37 val sym_thm: thm -> thm
41 structure ThmC(**): THEOREM_ISAC(**) =
45 (** types and conversions **)
48 type id = ThmC_Def.id;
49 type long_id = string;
51 fun long_id (thmID, _) = thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint
52 fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into Know_Store*)
54 val string_of_thm = ThmC_Def.string_of_thm;
55 val string_of_thms = ThmC_Def.string_of_thms;
57 fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;
58 fun of_thm thm = (id_of_thm thm, thm);
59 fun from_rule (Rule.Thm (id, thm)) = (id, thm)
60 | from_rule r = raise ERROR ("rule2thm': not defined for " ^ Rule.to_string r);
62 fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.to_ctxt thy) (Thm.prop_of thm);
64 fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm))
65 handle ERROR _ => false
68 (** handle symmetric equalities, generated by deriving input terms **)
71 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true
74 case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id
77 (* get the theorem associated with the xstring-identifier;
78 if the identifier starts with "sym_" then swap "lhs = rhs" around "=";
79 in case identifiers starting with "#" come from Eval and
80 get an ad-hoc theorem (containing numerals only) -- rejected here
82 fun thm_from_thy thy thmid =
83 case Symbol.explode thmid of
84 "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
85 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
86 | "s" :: "y" :: "m" :: "_" :: id =>
87 ((Global_Theory.get_thm thy) (implode id)) RS sym
89 raise ERROR ("thm_from_thy not impl.for " ^ thmid)
91 thmid |> Global_Theory.get_thm thy
93 fun dest_eq_concl thm =
94 (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
95 NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm])
98 (* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
99 (*NB: careful instantiation avoids shifting of schematic variables*)
102 val thy = Thm.theory_of_thm thm;
103 val certT = Thm.global_ctyp_of thy;
104 val cert = Thm.global_cterm_of thy;
106 val (lhs, rhs) = dest_eq_concl thm |> apply2 cert;
107 val A = Thm.typ_of_cterm lhs;
109 val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
110 val (t, s) = dest_eq_concl sym_rule;
112 val instT = map (rpair A) (Term.add_tvars t []);
113 val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, []));
115 val cinstT = map (apsnd certT) instT;
116 val cinst = [(s', lhs), (t', rhs)];
119 |> Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule)
120 |> Thm.put_name_hint (Thm.get_name_hint thm)
123 fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
124 | make_sym_rule_set (Rule_Def.Repeat {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
125 Rule_Def.Repeat {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
126 rules = rules, rew_ord = rew_ord, preconds = preconds}
127 | make_sym_rule_set (Rule_Set.Sequence {id, scr, calc, errpatts, erls, srls, rules, rew_ord, preconds}) =
128 Rule_Set.Sequence {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls, srls = srls,
129 rules = rules, rew_ord = rew_ord, preconds = preconds}
130 | make_sym_rule_set (Rule_Set.Rrls {id, scr, calc, errpatts, erls, prepat, rew_ord}) =
131 Rule_Set.Rrls {id = "sym_" ^ id, scr = scr, calc = calc, errpatts = errpatts, erls = erls,
132 prepat = prepat, rew_ord = rew_ord}
134 (* toggles sym_* and keeps "#:" for ad-hoc theorems *)
135 fun make_sym_rule (Rule.Thm (thmID, thm)) =
137 val thm' = sym_thm thm
138 val thmID' = case Symbol.explode thmID of
139 "s" :: "y" :: "m" :: "_" :: id => implode id
140 | "#" :: ":" :: _ => "#: " ^ string_of_thm thm'
141 | _ => "sym_" ^ thmID
142 in Rule.Thm (thmID', thm') end
143 | make_sym_rule (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
144 | make_sym_rule r = raise ERROR ("make_sym_rule: not for " ^ Rule.to_string r)
146 fun revert_sym_rule thy (Rule.Thm (id, thm)) =
147 if is_sym (cut_id id)
150 val id' = id_drop_sym id
151 val thm' = thm_from_thy thy id'
152 val id'' = Thm.get_name_hint thm'
153 in Rule.Thm (id'', thm') end
154 else Rule.Thm (Thm.get_name_hint thm, thm)
155 | revert_sym_rule _ rule = raise ERROR ("revert_sym_rule: NOT for " ^ Rule.to_string rule)
158 (* ML antiquotations *)
160 val sym_prefix = "sym_";
162 fun make_rule ctxt symmetric (xname, pos) =
165 if String.isPrefix sym_prefix xname
166 then error ("Bad theorem name with sym-prefix " ^ quote xname ^ Position.here pos) else ();
168 val context = Context.Proof ctxt;
169 val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
170 val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos);
172 if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)
173 else Facts.the_single (name, pos) thms;
174 val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);
175 in Rule.Thm (xname', thm') end;
177 fun antiquotation binding sym =
178 ML_Antiquotation.value_embedded binding
179 (Scan.lift Args.embedded_position >> (fn name =>
180 "ThmC.make_rule ML_context " ^ Bool.toString sym ^
181 ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position name));
185 (antiquotation \<^binding>\<open>rule_thm\<close> false #>
186 antiquotation \<^binding>\<open>rule_thm_sym\<close> true);