wenzelm@6783: (*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783:     ID:         $Id$
wenzelm@6783:     Author:     Markus Wenzel, TU Muenchen
wenzelm@6783: 
wenzelm@17349: Automatic bindings of Isar text elements.
wenzelm@6783: *)
wenzelm@6783: 
wenzelm@6783: signature AUTO_BIND =
wenzelm@6783: sig
wenzelm@17349:   val rule_contextN: string
wenzelm@9296:   val thesisN: string
wenzelm@17349:   val thisN: string
wenzelm@19075:   val premsN: string
wenzelm@21448:   val assmsN: string
wenzelm@17349:   val goal: theory -> term list -> (indexname * term option) list
wenzelm@17349:   val cases: theory -> term list -> (string * RuleCases.T option) list
wenzelm@17349:   val facts: theory -> term list -> (indexname * term option) list
wenzelm@17852:   val no_facts: (indexname * term option) list
wenzelm@6783: end;
wenzelm@6783: 
wenzelm@6783: structure AutoBind: AUTO_BIND =
wenzelm@6783: struct
wenzelm@6783: 
wenzelm@10359: (** bindings **)
wenzelm@10359: 
wenzelm@17349: val rule_contextN = "rule_context";
wenzelm@10359: val thesisN = "thesis";
wenzelm@10359: val thisN = "this";
wenzelm@19075: val premsN = "prems";
wenzelm@21448: val assmsN = "assms";
wenzelm@10359: 
wenzelm@17349: fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
wenzelm@11764: 
wenzelm@17349: fun statement_binds thy name prop =
wenzelm@17349:   [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
wenzelm@10359: 
wenzelm@10359: 
wenzelm@10359: (* goal *)
wenzelm@10359: 
wenzelm@17349: fun goal thy [prop] = statement_binds thy thesisN prop
skalberg@15531:   | goal _ _ = [((thesisN, 0), NONE)];
wenzelm@10359: 
wenzelm@18605: fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
wenzelm@18605:   | cases _ _ = [(rule_contextN, NONE)];
wenzelm@17349: 
wenzelm@10359: 
wenzelm@10359: (* facts *)
wenzelm@10359: 
wenzelm@17349: fun get_arg thy prop =
wenzelm@17349:   (case strip_judgment thy prop of
skalberg@15531:     _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
skalberg@15531:   | _ => NONE);
wenzelm@10359: 
wenzelm@12140: fun facts _ [] = []
wenzelm@17349:   | facts thy props =
wenzelm@10359:       let val prop = Library.last_elem props
wenzelm@17349:       in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
wenzelm@10359: 
wenzelm@17852: val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
wenzelm@10808: 
wenzelm@6783: end;