diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index 51dd726..bd914f4 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -39,6 +39,9 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) "doc_class" "onto_class" (* a syntactic alternative *) "ML*" "define_shortcut*" "define_macro*" :: thy_decl + and "definition*" :: thy_defn + and "theorem*" "lemma*" "corollary*" "proposition*" :: thy_goal_stmt + and "schematic_goal*" :: thy_goal_stmt and "text*" "text-macro*" :: document_body and "term*" "value*" "assert*" :: document_body @@ -2316,6 +2319,265 @@ val _ = end \ +\ \c.f. \<^file>\~~/src/Pure/Isar/specification.ML\ and \<^file>\~~/src/Pure/Pure.thy\\ +ML\ +structure Definition_Star_Command = +struct + +fun get_positions ctxt x = + let + fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t + | get Cs (Free (y, T)) = + if x = y then + map_filter Term_Position.decode_positionT + (T :: map (Type.constraint_type ctxt) Cs) + else [] + | get _ (t $ u) = get [] t @ get [] u + | get _ (Abs (_, _, t)) = get [] t + | get _ _ = []; + in get [] end; + +fun prep_decls prep_var raw_vars ctxt = + let + val (vars, ctxt') = fold_map prep_var raw_vars ctxt; + val (xs, ctxt'') = ctxt' + |> Context_Position.set_visible false + |> Proof_Context.add_fixes vars + ||> Context_Position.restore_visible ctxt'; + val _ = + Context_Position.reports ctxt'' + (map (Binding.pos_of o #1) vars ~~ + map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs); + in ((vars, xs), ctxt'') end; + +fun dummy_frees ctxt xs tss = + let + val names = + Variable.names_of ((fold o fold) Variable.declare_term tss ctxt) + |> fold Name.declare xs; + val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names; + in tss' end; + +fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt = + let + val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt; + val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes; + + val props = + map (parse_prop params_ctxt) (raw_concl :: raw_prems) + |> singleton (dummy_frees params_ctxt (xs @ ys)); + val concl :: prems = Syntax.check_props params_ctxt props; + val spec = Logic.list_implies (prems, concl); + val spec' = DOF_core.transduce_term_global {mk_elaboration=true} + (spec , Position.none) + (Proof_Context.theory_of ctxt) + val spec_ctxt = Variable.declare_term spec' params_ctxt; + + fun get_pos x = maps (get_positions spec_ctxt x) props; + in ((vars, xs, get_pos, spec'), spec_ctxt) end; + +val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop; + +(* definition *) + +fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy = + let + val atts = map (prep_att lthy) raw_atts; + + val ((vars, xs, get_pos, spec), _) = lthy + |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec; + val (((x, T), rhs), prove) = Local_Defs.derived_def lthy get_pos {conditional = true} spec; + val _ = Name.reject_internal (x, []); + val (b, mx) = + (case (vars, xs) of + ([], []) => (Binding.make (x, (case get_pos x of [] => Position.none | p :: _ => p)), NoSyn) + | ([(b, _, mx)], [y]) => + if x = y then (b, mx) + else + error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^ + Position.here (Binding.pos_of b))); + + val name = Thm.def_binding_optional b a; + val ((lhs, (_, raw_th)), lthy2) = lthy + |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs)); + + val th = prove lthy2 raw_th; + val lthy3 = lthy2 |> Spec_Rules.add name Spec_Rules.equational [lhs] [th]; + + val ([(def_name, [th'])], lthy4) = lthy3 + |> Local_Theory.notes [((name, atts), [([th], [])])]; + + val lthy5 = lthy4 + |> Code.declare_default_eqns [(th', true)]; + + val lhs' = Morphism.term (Local_Theory.target_morphism lthy5) lhs; + + val _ = + Proof_Display.print_consts int (Position.thread_data ()) lthy5 + (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)]; + in ((lhs, (def_name, th')), lthy5) end; + +val definition_cmd = gen_def read_spec_open Attrib.check_src; + +fun definition_cmd' meta_args_opt decl params prems spec bool ctxt = + Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) ctxt + |> definition_cmd decl params prems spec bool + +val _ = + Outer_Syntax.local_theory' \<^command_keyword>\definition*\ "constant definition" + (ODL_Meta_Args_Parser.opt_attributes -- + (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- + Parse_Spec.if_assumes -- Parse.for_fixes) + >> (fn (meta_args_opt, (((decl, spec), prems), params)) => + #2 oo definition_cmd' meta_args_opt decl params prems spec)); +end +\ + +\ \c.f. \<^file>\~~/src/Pure/Isar/specification.ML\ and \<^file>\~~/src/Pure/Pure.thy\\ +ML\ +(* theorem*, lemma*, etc. commands *) + +local + +fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = + let + val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt; + val prems = Assumption.local_prems_of elems_ctxt ctxt; + val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt; + in + (case raw_stmt of + Element.Shows _ => + let val stmt' = Attrib.map_specs (map prep_att) stmt + val stmt'' = map (fn (b, ts) => + (b, map (fn (t', t's) => + (DOF_core.transduce_term_global {mk_elaboration=true} + (t' , Position.none) + (Proof_Context.theory_of ctxt), + map (fn t'' => + DOF_core.transduce_term_global {mk_elaboration=true} + (t'' , Position.none) + (Proof_Context.theory_of ctxt)) + t's)) ts)) stmt' + in (([], prems, stmt'', NONE), stmt_ctxt) end + | Element.Obtains raw_obtains => + let + val asms_ctxt = stmt_ctxt + |> fold (fn ((name, _), asm) => + snd o Proof_Context.add_assms Assumption.assume_export + [((name, [Context_Rules.intro_query NONE]), asm)]) stmt; + val that = Assumption.local_prems_of asms_ctxt stmt_ctxt; + val ([(_, that')], that_ctxt) = asms_ctxt + |> Proof_Context.set_stmt true + |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])] + ||> Proof_Context.restore_stmt asms_ctxt; + + val stmt' = [(Binding.empty_atts, [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])]; + val stmt'' = map (fn (b, ts) => + (b, map (fn (t', t's) => + (DOF_core.transduce_term_global {mk_elaboration=true} + (t' , Position.none) + (Proof_Context.theory_of ctxt), + map (fn t'' => + DOF_core.transduce_term_global {mk_elaboration=true} + (t'' , Position.none) + (Proof_Context.theory_of ctxt)) + t's)) ts)) stmt' + in ((Obtain.obtains_attribs raw_obtains, prems, stmt'', SOME that'), that_ctxt) end) + end; + +fun gen_theorem schematic bundle_includes prep_att prep_stmt + long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = + let + val _ = Local_Theory.assert lthy; + + val elems = raw_elems |> map (Element.map_ctxt_attrib (prep_att lthy)); + val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy + |> bundle_includes raw_includes + |> prep_statement (prep_att lthy) prep_stmt elems raw_concl; + val atts = more_atts @ map (prep_att lthy) raw_atts; + + val pos = Position.thread_data (); + fun after_qed' results goal_ctxt' = + let + val results' = + burrow (map (Goal.norm_result lthy) o Proof_Context.export goal_ctxt' lthy) results; + val (res, lthy') = + if forall (Binding.is_empty_atts o fst) stmt then (map (pair "") results', lthy) + else + Local_Theory.notes_kind kind + (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; + val lthy'' = + if Binding.is_empty_atts (name, atts) then + (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy') + else + let + val ([(res_name, _)], lthy'') = + Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; + val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res); + in lthy'' end; + in after_qed results' lthy'' end; + + val prems_name = if long then Auto_Bind.assmsN else Auto_Bind.thatN; + in + goal_ctxt + |> not (null prems) ? + (Proof_Context.note_thmss "" [((Binding.name prems_name, []), [(prems, [])])] #> snd) + |> Proof.theorem before_qed after_qed' (map snd stmt) + |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) + |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso + error "Illegal schematic goal statement") + end; + +in + +val theorem_cmd = + gen_theorem false Bundle.includes_cmd Attrib.check_src Expression.read_statement; + +fun theorem_cmd' meta_args_opt long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = + Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) lthy + |> theorem_cmd long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int; + +val schematic_theorem_cmd = + gen_theorem true Bundle.includes_cmd Attrib.check_src Expression.read_statement; + +fun schematic_theorem_cmd' meta_args_opt long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy = + Local_Theory.background_theory (Value_Command.meta_args_exec meta_args_opt) lthy + |> schematic_theorem_cmd long kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int; + +end; + +local +val long_keyword = + Parse_Spec.includes >> K "" || + Parse_Spec.long_statement_keyword; + +val long_statement = + ODL_Meta_Args_Parser.opt_attributes -- + Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- + Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement + >> (fn (((meta_args_opt, binding), includes), (elems, concl)) => (meta_args_opt, true, binding, includes, elems, concl)); + +val short_statement = + ODL_Meta_Args_Parser.opt_attributes -- + Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes + >> (fn (((meta_args_opt, shows), assumes), fixes) => + (meta_args_opt, false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], + Element.Shows shows)); + +fun theorem spec schematic descr = + Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) + ((long_statement || short_statement) >> (fn (meta_args_opt, long, binding, includes, elems, concl) => + ((if schematic then schematic_theorem_cmd' else theorem_cmd') + meta_args_opt long Thm.theoremK NONE (K I) binding includes elems concl))); + +val _ = theorem \<^command_keyword>\theorem*\ false "theorem"; +val _ = theorem \<^command_keyword>\lemma*\ false "lemma"; +val _ = theorem \<^command_keyword>\corollary*\ false "corollary"; +val _ = theorem \<^command_keyword>\proposition*\ false "proposition"; +val _ = theorem \<^command_keyword>\schematic_goal*\ true "schematic goal"; +in end +\ + ML\ structure ODL_LTX_Converter = struct