Merge branch 2017 into devel

This commit is contained in:
Frédéric Tuong 2019-04-04 19:19:23 +02:00
commit 8523e81952
9 changed files with 208 additions and 5 deletions

View File

@ -57,10 +57,10 @@ holder "u-psud" :: fr where \<open>Université Paris-Saclay\<close>, \<open>Univ
holder vt :: us where \<open>Virginia Tech\<close>
holder wolff :: fr where \<open>B. Wolff\<close>, \<open>Univ. Paris-Saclay\<close>, \<open>Univ. Paris-Sud\<close>
copyright default where 2011-2018 "u-psud"
copyright default where 2011-2019 "u-psud"
2013-2017 "irt-systemx"
2011-2015 brucker
2016-2018 sheffield
2016-2019 sheffield
2016-2017 ntu
2017-2018 vt
@ -70,10 +70,12 @@ This file is part of HOL-TestGen.
\<close> imports default
project LICENSE0 :: "3-Clause BSD" where \<open>LICENSE\<close> defines 2017-2018 vt
2018-2019 "u-psud"
project LICENSE :: "3-Clause BSD" where \<open>
theory LICENSE imports LICENSE0 begin license "3-Clause BSD" where
\<close> defines 2017-2018 vt
2018-2019 "u-psud"
project "Featherweight OCL" :: "3-Clause BSD" where \<open>
Featherweight-OCL --- A Formal Semantics for UML-OCL Version OCL 2.5
@ -89,13 +91,14 @@ project Isabelle_Meta_Model :: "3-Clause BSD" where \<open>A Meta-Model for the
project Isabelle :: "3-Clause BSD" where \<open>
ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER.
\<close> defines 1986-2018 contributors
\<close> defines 1986-2019 contributors
project Haskabelle :: "3-Clause BSD" where \<open>
Haskabelle --- Converting Haskell Source Files to Isabelle/HOL Theories.
http://isabelle.in.tum.de/repos/haskabelle
\<close> defines 2007-2015 tum
2017-2018 vt
2018-2019 "u-psud"
project "HOL-OCL" :: "3-Clause BSD" where \<open>HOL-OCL\<close> imports default
@ -114,6 +117,7 @@ https://hackage.haskell.org/package/language-c-comments
Securify & Orca
\<close> defines 2016-2017 ntu
2017-2018 vt
2018-2019 "u-psud"
project Miscellaneous_Monads :: "3-Clause BSD" where \<open>
HOL-TestGen --- theorem-prover based test case generation

View File

@ -483,22 +483,29 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(snd o Typedecl.abbrev_global
(s_bind, map To_string0 v, NoSyn)
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
(Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
[],
Syntax.read_sort (Proof_Context.init_global thy) "object")
fun instantiation2 name n_def expr =
Specification.definition_cmd NONE [] [] ( (To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), [])
, of_semi__term expr)
fun overloading1 n_c e_c = Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)]
fun overloading2 n e =
#2 oo Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e)
fun consts top (Consts (n, ty, symb)) = #theory top
(Sign.add_consts_cmd [( To_sbinding n
, of_semi__typ ty
, Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))])
fun definition top def = #local_theory' top NONE NONE
let val (def, e) = case def of
Definitiona e => (NONE, e)
@ -511,6 +518,7 @@ fun definition top def = #local_theory' top NONE NONE
, NONE
, Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in fn ctxt => ctxt
|> #2 oo Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) end
fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
let val (simp, s, l) =
case lemmas of Lemmas_simp_thm (simp, s, l) =>
@ -523,10 +531,12 @@ fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
l)]
[]
disp) lthy end)
fun lemma1 n l_spec = Specification.theorem_cmd true Thm.theoremK NONE (K I)
Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, [])
,[((String.concatWith (" \<Longrightarrow> ")
(List.map of_semi__term l_spec)), [])])])
fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K I)
(To_sbinding n, [])
[]
@ -536,29 +546,36 @@ fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K
, [(of_semi__term e, [])])])
l_spec)
(Element.Shows [(Binding.empty_atts,[(of_semi__term concl, [])])])
fun lemma3 l_apply = map_filter (fn META.Command_let _ => SOME []
| META.Command_have _ => SOME []
| META.Command_fix_let (_, _, _, l) => SOME l
| _ => NONE)
(rev l_apply)
fun axiomatization top (Axiomatization (n, e)) = #theory top
(#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)])
fun section n s _ =
let fun mk s n = if n <= 0 then s else mk (" " ^ s) (n - 1) in
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
fun ml top (SMLa ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
end #>
Local_Theory.propagate_ml_env)
fun setup top (Setup ml) = #theory top (Isar_Cmd.setup (input_source ml))
fun thm top (Thm thm) = #keep top (fn state =>
let val lthy = #context_of top state in
Print_Mode.with_modes [] (fn () => writeln
(Pretty.string_of
(Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm)))) ()
end)
fun interpretation1 n loc_n loc_param =
Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none)
, ( (To_string0 n, true)
@ -569,6 +586,19 @@ fun interpretation1 n loc_n loc_param =
loc_param)
, [])))]
, [])
fun hide_const top (Hide_const (fully, args)) = #theory top (fn thy =>
fold (Sign.hide_const (not fully) o ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false})
(Proof_Context.init_global thy))
(map To_string0 args)
thy)
fun abbreviation top (Abbreviation e) = #local_theory' top NONE NONE
(Specification.abbreviation_cmd ("", true) NONE [] (of_semi__term e))
fun code_reflect' top (Code_reflect (all_public, module_name, raw_functions)) = #theory top
(Code_Runtime'.code_reflect_cmd all_public [] (map To_string0 raw_functions) (To_string0 module_name) NONE)
end
structure Command_Transition = struct
@ -638,6 +668,12 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|>:: (\<^command_keyword>\<open>interpretation\<close>, #local_theory_to_proof top NONE NONE
(Cmd.interpretation1 n loc_n loc_param))
|>:: terminal_proof_dual top o_by)
| Theory_hide_const hide_const =>
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
| Theory_abbreviation abbreviation =>
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
| Theory_code_reflect code_reflect' =>
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end
@ -700,6 +736,9 @@ fun semi__theory top = let open META open META_overload in (*let val f = *)fn
| Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => #local_theory top NONE NONE (fn lthy => lthy
|> Cmd.interpretation1 n loc_n loc_param
|> global_terminal_proof o_by)
| Theory_hide_const hide_const => Cmd.hide_const top hide_const
| Theory_abbreviation abbreviation => Cmd.abbreviation top abbreviation
| Theory_code_reflect code_reflect' => Cmd.code_reflect' top code_reflect'
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end

View File

@ -472,22 +472,29 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(snd o Typedecl.abbrev_global
(s_bind, map To_string0 v, NoSyn)
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
(Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
[],
Syntax.read_sort (Proof_Context.init_global thy) "object")
fun instantiation2 name n_def expr =
Specification.definition_cmd NONE [] [] ( (To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), [])
, of_semi__term expr)
fun overloading1 n_c e_c = Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)]
fun overloading2 n e =
#2 oo Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e)
fun consts top (Consts (n, ty, symb)) = #theory top
(Sign.add_consts_cmd [( To_sbinding n
, of_semi__typ ty
, Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))])
fun definition top def = #local_theory' top NONE NONE
let val (def, e) = case def of
Definitiona e => (NONE, e)
@ -500,6 +507,7 @@ fun definition top def = #local_theory' top NONE NONE
, NONE
, Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in fn ctxt => ctxt
|> #2 oo Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) end
fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
let val (simp, s, l) =
case lemmas of Lemmas_simp_thm (simp, s, l) =>
@ -512,10 +520,12 @@ fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
l)]
[]
disp) lthy end)
fun lemma1 n l_spec = Specification.theorem_cmd true Thm.theoremK NONE (K I)
Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, [])
,[((String.concatWith (" \<Longrightarrow> ")
(List.map of_semi__term l_spec)), [])])])
fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K I)
(To_sbinding n, [])
[]
@ -525,29 +535,36 @@ fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K
, [(of_semi__term e, [])])])
l_spec)
(Element.Shows [(Binding.empty_atts,[(of_semi__term concl, [])])])
fun lemma3 l_apply = map_filter (fn META.Command_let _ => SOME []
| META.Command_have _ => SOME []
| META.Command_fix_let (_, _, _, l) => SOME l
| _ => NONE)
(rev l_apply)
fun axiomatization top (Axiomatization (n, e)) = #theory top
(#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)])
fun section n s _ =
let fun mk s n = if n <= 0 then s else mk (" " ^ s) (n - 1) in
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
fun ml top (SMLa ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
end #>
Local_Theory.propagate_ml_env)
fun setup top (Setup ml) = #theory top (Isar_Cmd.setup (input_source ml))
fun thm top (Thm thm) = #keep top (fn state =>
let val lthy = #context_of top state in
Print_Mode.with_modes [] (fn () => writeln
(Pretty.string_of
(Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm)))) ()
end)
fun interpretation1 n loc_n loc_param =
Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none)
, ( (To_string0 n, true)
@ -558,6 +575,19 @@ fun interpretation1 n loc_n loc_param =
loc_param)
, [])))]
, [])
fun hide_const top (Hide_const (fully, args)) = #theory top (fn thy =>
fold (Sign.hide_const (not fully) o ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false})
(Proof_Context.init_global thy))
(map To_string0 args)
thy)
fun abbreviation top (Abbreviation e) = #local_theory' top NONE NONE
(Specification.abbreviation_cmd ("", true) NONE [] (of_semi__term e))
fun code_reflect' top (Code_reflect (all_public, module_name, raw_functions)) = #theory top
(Code_Runtime'.code_reflect_cmd all_public [] (map To_string0 raw_functions) (To_string0 module_name) NONE)
end
structure Command_Transition = struct
@ -627,6 +657,12 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|>:: (\<^command_keyword>\<open>interpretation\<close>, #local_theory_to_proof top NONE NONE
(Cmd.interpretation1 n loc_n loc_param))
|>:: terminal_proof_dual top o_by)
| Theory_hide_const hide_const =>
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
| Theory_abbreviation abbreviation =>
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
| Theory_code_reflect code_reflect' =>
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end
@ -689,6 +725,9 @@ fun semi__theory top = let open META open META_overload in (*let val f = *)fn
| Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => #local_theory top NONE NONE (fn lthy => lthy
|> Cmd.interpretation1 n loc_n loc_param
|> global_terminal_proof o_by)
| Theory_hide_const hide_const => Cmd.hide_const top hide_const
| Theory_abbreviation abbreviation => Cmd.abbreviation top abbreviation
| Theory_code_reflect code_reflect' => Cmd.code_reflect' top code_reflect'
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end

View File

@ -516,22 +516,29 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(snd o Typedecl.abbrev_global
(s_bind, map To_string0 v, NoSyn)
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
(Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
[],
Syntax.read_sort (Proof_Context.init_global thy) "object")
fun instantiation2 name n_def expr =
Specification.definition_cmd NONE [] [] ( (To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), [])
, of_semi__term expr)
fun overloading1 n_c e_c = Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)]
fun overloading2 n e =
#2 oo Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e)
fun consts top (Consts (n, ty, symb)) = #theory top
(Sign.add_consts_cmd [( To_sbinding n
, of_semi__typ ty
, Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))])
fun definition top def = #local_theory' top NONE NONE
let val (def, e) = case def of
Definitiona e => (NONE, e)
@ -544,6 +551,7 @@ fun definition top def = #local_theory' top NONE NONE
, NONE
, Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in fn ctxt => ctxt
|> #2 oo Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) end
fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
let val (simp, s, l) =
case lemmas of Lemmas_simp_thm (simp, s, l) =>
@ -556,10 +564,12 @@ fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
l)]
[]
disp) lthy end)
fun lemma1 n l_spec = Specification.theorem_cmd true Thm.theoremK NONE (K I)
Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, [])
,[((String.concatWith (" \<Longrightarrow> ")
(List.map of_semi__term l_spec)), [])])])
fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K I)
(To_sbinding n, [])
[]
@ -569,29 +579,36 @@ fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K
, [(of_semi__term e, [])])])
l_spec)
(Element.Shows [(Binding.empty_atts,[(of_semi__term concl, [])])])
fun lemma3 l_apply = map_filter (fn META.Command_let _ => SOME []
| META.Command_have _ => SOME []
| META.Command_fix_let (_, _, _, l) => SOME l
| _ => NONE)
(rev l_apply)
fun axiomatization top (Axiomatization (n, e)) = #theory top
(#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)])
fun section n s _ =
let fun mk s n = if n <= 0 then s else mk (" " ^ s) (n - 1) in
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
fun ml top (SMLa ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
end #>
Local_Theory.propagate_ml_env)
fun setup top (Setup ml) = #theory top (Isar_Cmd.setup (input_source ml))
fun thm top (Thm thm) = #keep top (fn state =>
let val lthy = #context_of top state in
Print_Mode.with_modes [] (fn () => writeln
(Pretty.string_of
(Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm)))) ()
end)
fun interpretation1 n loc_n loc_param =
Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none)
, ( (To_string0 n, true)
@ -602,6 +619,19 @@ fun interpretation1 n loc_n loc_param =
loc_param)
, [])))]
, [])
fun hide_const top (Hide_const (fully, args)) = #theory top (fn thy =>
fold (Sign.hide_const (not fully) o ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false})
(Proof_Context.init_global thy))
(map To_string0 args)
thy)
fun abbreviation top (Abbreviation e) = #local_theory' top NONE NONE
(Specification.abbreviation_cmd ("", true) NONE [] (of_semi__term e))
fun code_reflect' top (Code_reflect (all_public, module_name, raw_functions)) = #theory top
(Code_Runtime'.code_reflect_cmd all_public [] (map To_string0 raw_functions) (To_string0 module_name) NONE)
end
structure Command_Transition = struct
@ -671,6 +701,12 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|>:: (\<^command_keyword>\<open>interpretation\<close>, #local_theory_to_proof top NONE NONE
(Cmd.interpretation1 n loc_n loc_param))
|>:: terminal_proof_dual top o_by)
| Theory_hide_const hide_const =>
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
| Theory_abbreviation abbreviation =>
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
| Theory_code_reflect code_reflect' =>
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end
@ -733,6 +769,9 @@ fun semi__theory top = let open META open META_overload in (*let val f = *)fn
| Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => #local_theory top NONE NONE (fn lthy => lthy
|> Cmd.interpretation1 n loc_n loc_param
|> global_terminal_proof o_by)
| Theory_hide_const hide_const => Cmd.hide_const top hide_const
| Theory_abbreviation abbreviation => Cmd.abbreviation top abbreviation
| Theory_code_reflect code_reflect' => Cmd.code_reflect' top code_reflect'
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end

View File

@ -241,6 +241,9 @@ definition "ML = i Theory_ML"
definition "setup = i Theory_setup"
definition "thm = i Theory_thm"
definition "interpretation = i Theory_interpretation"
definition "hide_const = i Theory_hide_const"
definition "abbreviation = i Theory_abbreviation"
definition "code_reflect' = i Theory_code_reflect'"
end
lemmas [code] =
@ -263,6 +266,9 @@ lemmas [code] =
O.setup_def
O.thm_def
O.interpretation_def
O.hide_const_def
O.abbreviation_def
O.code_reflect'_def
locale O'
begin
@ -282,6 +288,9 @@ definition "ML = Theory_ML"
definition "setup = Theory_setup"
definition "thm = Theory_thm"
definition "interpretation = Theory_interpretation"
definition "hide_const = Theory_hide_const"
definition "abbreviation = Theory_abbreviation"
definition "code_reflect' = Theory_code_reflect'"
end
lemmas [code] =
@ -302,6 +311,9 @@ lemmas [code] =
O'.setup_def
O'.thm_def
O'.interpretation_def
O'.hide_const_def
O'.abbreviation_def
O'.code_reflect'_def
subsubsection\<open>Operations of Fold, Map, ..., on the Meta-Model\<close>

View File

@ -40,7 +40,7 @@ imports Main
begin
ML{*
structure Code_Runtime =
structure Code_Runtime' =
struct
(* Title: Tools/Code/code_runtime.ML
Author: Florian Haftmann, TU Muenchen

View File

@ -198,6 +198,15 @@ datatype "interpretation" = Interpretation string \<comment> \<open>name\<close>
"semi__term list" \<comment> \<open>locale param\<close>
semi__command_final
datatype "hide_const" = Hide_const bool (* true: 'open' *)
"string list"
datatype "abbreviation" = Abbreviation semi__term
datatype code_reflect' = Code_reflect' bool (* true: 'open' *)
string (* module name *)
"string list" (* functions *)
datatype semi__theory = Theory_datatype "datatype"
| Theory_type_synonym "type_synonym"
| Theory_type_notation "type_notation"
@ -215,6 +224,9 @@ datatype semi__theory = Theory_datatype "datatype"
| Theory_setup "setup"
| Theory_thm "thm"
| Theory_interpretation "interpretation"
| Theory_hide_const "hide_const"
| Theory_abbreviation "abbreviation"
| Theory_code_reflect' code_reflect'
record semi__locale =
HolThyLocale_name :: string

View File

@ -364,6 +364,19 @@ definition \<open>of_interpretation _ = (\<lambda> Interpretation n loc_n loc_pa
(String_concat \<open>\<close> (L.map (\<lambda>s. \<open> "%s"\<close> (of_semi__term s)) loc_param))
(of_semi__command_final tac))\<close>
definition "of_hide_const _ = (\<lambda> Hide_const b l \<Rightarrow>
\<open>hide_const %s%s\<close> (if b then \<open>(open) \<close> else \<open>\<close>)
(String_concat \<open> \<close> (L.map To_string l)))"
definition "of_abbreviation _ = (\<lambda> Abbreviation e \<Rightarrow>
\<open>abbreviation \"%s\"\<close> (of_semi__term e))"
definition "of_code_reflect' _ = (\<lambda> Code_reflect' b s l \<Rightarrow>
\<open>code_reflect' %s%s%s\<close>
(if b then \<open>open \<close> else \<open>\<close>)
(To_string s)
(case l of [] \<Rightarrow> \<open>\<close> | _ \<Rightarrow> \<open> functions %s\<close> (String_concat \<open> \<close> (L.map To_string l))))"
definition "of_semi__theory env =
(\<lambda> Theory_datatype dataty \<Rightarrow> of_datatype env dataty
| Theory_type_synonym ty_synonym \<Rightarrow> of_type_synonym env ty_synonym
@ -381,7 +394,10 @@ definition "of_semi__theory env =
| Theory_ML ml \<Rightarrow> of_ML env ml
| Theory_setup setup \<Rightarrow> of_setup env setup
| Theory_thm thm \<Rightarrow> of_thm env thm
| Theory_interpretation thm \<Rightarrow> of_interpretation env thm)"
| Theory_interpretation thm \<Rightarrow> of_interpretation env thm
| Theory_hide_const const \<Rightarrow> of_hide_const env const
| Theory_abbreviation abbreviation \<Rightarrow> of_abbreviation env abbreviation
| Theory_code_reflect' code_reflect' \<Rightarrow> of_code_reflect' env code_reflect')"
definition "String_concat_map s f l = String_concat s (L.map f l)"
@ -447,6 +463,9 @@ lemmas [code] =
Print.of_setup_def
Print.of_thm_def
Print.of_interpretation_def
Print.of_hide_const_def
Print.of_abbreviation_def
Print.of_code_reflect'_def
Print.of_semi__theory_def
Print.String_concat_map_def
Print.of_semi__theories_def

View File

@ -491,22 +491,29 @@ fun type_synonym top (Type_synonym ((n, v), l)) = #theory top (fn thy => let val
(snd o Typedecl.abbrev_global
(s_bind, map To_string0 v, NoSyn)
(Isabelle_Typedecl.abbrev_cmd0 (SOME s_bind) thy (of_semi__typ l))) thy end)
fun type_notation top (Type_notation (n, e)) = #local_theory top NONE NONE
(Specification.type_notation_cmd true ("", true) [(To_string0 n, Mixfix (Input.string (To_string0 e), [], 1000, Position.no_range))])
fun instantiation1 name thy = thy
|> Class.instantiation ([ let val Term.Type (s, _) = Isabelle_Typedecl.abbrev_cmd0 NONE thy name in s end ],
[],
Syntax.read_sort (Proof_Context.init_global thy) "object")
fun instantiation2 name n_def expr =
Specification.definition_cmd NONE [] [] ( (To_binding (To_string0 n_def ^ "_" ^ name ^ "_def"), [])
, of_semi__term expr)
fun overloading1 n_c e_c = Overloading.overloading_cmd [(To_string0 n_c, of_semi__term e_c, true)]
fun overloading2 n e =
#2 oo Specification.definition_cmd NONE [] [] ((To_sbinding n, []), of_semi__term e)
fun consts top (Consts (n, ty, symb)) = #theory top
(Sign.add_consts_cmd [( To_sbinding n
, of_semi__typ ty
, Mixfix (Input.string ("(_) " ^ To_string0 symb), [], 1000, Position.no_range))])
fun definition top def = #local_theory' top NONE NONE
let val (def, e) = case def of
Definition e => (NONE, e)
@ -519,6 +526,7 @@ fun definition top def = #local_theory' top NONE NONE
, NONE
, Mixfix (Input.string ("(" ^ of_semi__term abbrev ^ ")"), [], 1000, Position.no_range)), e) in fn ctxt => ctxt
|> #2 oo Specification.definition_cmd def [] [] (Binding.empty_atts, of_semi__term e) end
fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
let val (simp, s, l) =
case lemmas of Lemmas_simp_thm (simp, s, l) =>
@ -531,10 +539,12 @@ fun lemmas top lemmas = #local_theory' top NONE NONE (fn disp => fn lthy =>
l)]
[]
disp) lthy end)
fun lemma1 n l_spec = Specification.theorem_cmd true Thm.theoremK NONE (K I)
Binding.empty_atts [] [] (Element.Shows [((To_sbinding n, [])
,[((String.concatWith (" \<Longrightarrow> ")
(List.map of_semi__term l_spec)), [])])])
fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K I)
(To_sbinding n, [])
[]
@ -544,29 +554,36 @@ fun lemma1' n l_spec concl = Specification.theorem_cmd true Thm.theoremK NONE (K
, [(of_semi__term e, [])])])
l_spec)
(Element.Shows [(Binding.empty_atts,[(of_semi__term concl, [])])])
fun lemma3 l_apply = map_filter (fn META.Command_let _ => SOME []
| META.Command_have _ => SOME []
| META.Command_fix_let (_, _, _, l) => SOME l
| _ => NONE)
(rev l_apply)
fun axiomatization top (Axiomatization (n, e)) = #theory top
(#2 o Specification.axiomatization_cmd [] [] [] [((To_sbinding n, []), of_semi__term e)])
fun section n s _ =
let fun mk s n = if n <= 0 then s else mk (" " ^ s) (n - 1) in
out_intensify (mk (Markup.markup Markup.keyword3 (To_string0 s)) n) ""
end
fun ml top (SML ml) = #generic_theory top
(ML_Context.exec let val source = input_source ml in
fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source
end #>
Local_Theory.propagate_ml_env)
fun setup top (Setup ml) = #theory top (Isar_Cmd.setup (input_source ml))
fun thm top (Thm thm) = #keep top (fn state =>
let val lthy = #context_of top state in
Print_Mode.with_modes [] (fn () => writeln
(Pretty.string_of
(Proof_Context.pretty_fact lthy ("", List.map (semi__thm_attribute_single lthy) thm)))) ()
end)
fun interpretation1 n loc_n loc_param =
Interpretation.interpretation_cmd ( [ ( (To_string0 loc_n, Position.none)
, ( (To_string0 n, true)
@ -577,6 +594,19 @@ fun interpretation1 n loc_n loc_param =
loc_param)
, [])))]
, [])
fun hide_const top (Hide_const (fully, args)) = #theory top (fn thy =>
fold (Sign.hide_const (not fully) o ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false})
(Proof_Context.init_global thy))
(map To_string0 args)
thy)
fun abbreviation top (Abbreviation e) = #local_theory' top NONE NONE
(Specification.abbreviation_cmd ("", true) NONE [] (of_semi__term e))
fun code_reflect' top (Code_reflect (all_public, module_name, raw_functions)) = #theory top
(Code_Runtime'.code_reflect_cmd all_public [] (map To_string0 raw_functions) (To_string0 module_name) NONE)
end
structure Command_Transition = struct
@ -646,6 +676,12 @@ fun semi__theory (top : ('transitionM, 'transitionM, 'state) toplevel) = let ope
|>:: (\<^command_keyword>\<open>interpretation\<close>, #local_theory_to_proof top NONE NONE
(Cmd.interpretation1 n loc_n loc_param))
|>:: terminal_proof_dual top o_by)
| Theory_hide_const hide_const =>
cons (@{command_keyword hide_const}, Cmd.hide_const top hide_const)
| Theory_abbreviation abbreviation =>
cons (@{command_keyword abbreviation}, Cmd.abbreviation top abbreviation)
| Theory_code_reflect code_reflect' =>
cons (@{command_keyword code_reflect'}, Cmd.code_reflect' top code_reflect')
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end
@ -708,6 +744,9 @@ fun semi__theory top = let open META open META_overload in (*let val f = *)fn
| Theory_interpretation (Interpretation (n, loc_n, loc_param, o_by)) => #local_theory top NONE NONE (fn lthy => lthy
|> Cmd.interpretation1 n loc_n loc_param
|> global_terminal_proof o_by)
| Theory_hide_const hide_const => Cmd.hide_const top hide_const
| Theory_abbreviation abbreviation => Cmd.abbreviation top abbreviation
| Theory_code_reflect code_reflect' => Cmd.code_reflect' top code_reflect'
(*in fn t => fn thy => f t thy handle ERROR s => (warning s; thy)
end*)
end