Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
Burkhart Wolff
commit
d835665b6b
|
|
@ -30,6 +30,10 @@ text\<open>
|
|||
\vfill
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
@{block (title = "\<open>Title\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close>") "\<open>Block content\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close>"}
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
end
|
||||
(*>*)
|
||||
|
|
|
|||
|
|
@ -6,3 +6,4 @@ session "presentation-example" (AFP) = "Isabelle_DOF-Ontologies" +
|
|||
"presentation"
|
||||
document_files
|
||||
"preamble.tex"
|
||||
"figures/A.png"
|
||||
|
|
|
|||
Binary file not shown.
|
After Width: | Height: | Size: 12 KiB |
|
|
@ -19,6 +19,51 @@ text\<open>
|
|||
\end{frame}
|
||||
\<close>
|
||||
|
||||
|
||||
frame*[test_frame
|
||||
, frametitle = \<open>\<open>\<open>Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> with items @{thm "HOL.refl"}\<close>\<close>
|
||||
, framesubtitle = "''Subtitle''"]
|
||||
\<open>This is an example!
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame\<close>}\<close>\<close>
|
||||
|
||||
frame*[test_frame2
|
||||
, frametitle = "''Example Slide''"
|
||||
, framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
|
||||
\<open>Test frame env \<^term>\<open>refl\<close>\<close>
|
||||
|
||||
frame*[test_frame3, frametitle = "''A slide with a Figure''"]
|
||||
\<open>A figure
|
||||
@{figure_content (width=45, caption=\<open>\<open>Figure\<^sub>t\<^sub>e\<^sub>s\<^sub>t\<close> is not the \<^term>\<open>refl\<close> theorem (@{thm "refl"}).\<close>)
|
||||
"figures/A.png"}\<close>
|
||||
|
||||
frame*[test_frame4
|
||||
, options = "''allowframebreaks''"
|
||||
, frametitle = "''Example Slide with frame break''"
|
||||
, framesubtitle = \<open>\<open>\<open>Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\<close> the value of \<^term>\<open>(3::int) + 3\<close> is @{value "(3::int) + 3"}\<close>\<close>]
|
||||
\<open>
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> and the term encoding the title of this frame is \<^term_>\<open>frametitle @{frame \<open>test_frame4\<close>}\<close>
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<^item> The term \<^term>\<open>refl\<close> is...
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
end
|
||||
(*>*)
|
||||
|
|
|
|||
|
|
@ -206,11 +206,10 @@ ML\<open>
|
|||
map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
|
||||
|
||||
let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D",
|
||||
"Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
|
||||
"Isa_COL.float", "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.listing",
|
||||
"Isa_COL.section",
|
||||
"Isa_COL.paragraph", "Isa_COL.subsection",
|
||||
"Isa_COL.text_element", "Isa_COL.subsubsection"]
|
||||
"Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M",
|
||||
"Isa_COL.float", "Isa_COL.frame", "Isa_COL.figure", "Isa_COL.chapter",
|
||||
"Isa_COL.listing", "Isa_COL.section", "Isa_COL.paragraph",
|
||||
"Isa_COL.subsection", "Isa_COL.text_element", "Isa_COL.subsubsection"]
|
||||
val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>));
|
||||
in @{assert} (class_ids_so_far = docclass_tab) end\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -1,463 +0,0 @@
|
|||
(* Title: HOL/Record.thy
|
||||
Author: Wolfgang Naraschewski, TU Muenchen
|
||||
Author: Markus Wenzel, TU Muenchen
|
||||
Author: Norbert Schirmer, TU Muenchen
|
||||
Author: Thomas Sewell, NICTA
|
||||
Author: Florian Haftmann, TU Muenchen
|
||||
*)
|
||||
|
||||
section \<open>Extensible records with structural subtyping\<close>
|
||||
|
||||
theory Test
|
||||
imports HOL.Quickcheck_Exhaustive
|
||||
keywords
|
||||
"record*" :: thy_defn and
|
||||
"print_record*" :: diag
|
||||
begin
|
||||
|
||||
subsection \<open>Introduction\<close>
|
||||
|
||||
text \<open>
|
||||
Records are isomorphic to compound tuple types. To implement
|
||||
efficient records, we make this isomorphism explicit. Consider the
|
||||
record access/update simplification \<open>alpha (beta_update f
|
||||
rec) = alpha rec\<close> for distinct fields alpha and beta of some record
|
||||
rec with n fields. There are \<open>n ^ 2\<close> such theorems, which
|
||||
prohibits storage of all of them for large n. The rules can be
|
||||
proved on the fly by case decomposition and simplification in O(n)
|
||||
time. By creating O(n) isomorphic-tuple types while defining the
|
||||
record, however, we can prove the access/update simplification in
|
||||
\<open>O(log(n)^2)\<close> time.
|
||||
|
||||
The O(n) cost of case decomposition is not because O(n) steps are
|
||||
taken, but rather because the resulting rule must contain O(n) new
|
||||
variables and an O(n) size concrete record construction. To sidestep
|
||||
this cost, we would like to avoid case decomposition in proving
|
||||
access/update theorems.
|
||||
|
||||
Record types are defined as isomorphic to tuple types. For instance,
|
||||
a record type with fields \<open>'a\<close>, \<open>'b\<close>, \<open>'c\<close>
|
||||
and \<open>'d\<close> might be introduced as isomorphic to \<open>'a \<times>
|
||||
('b \<times> ('c \<times> 'd))\<close>. If we balance the tuple tree to \<open>('a \<times>
|
||||
'b) \<times> ('c \<times> 'd)\<close> then accessors can be defined by converting to the
|
||||
underlying type then using O(log(n)) fst or snd operations.
|
||||
Updators can be defined similarly, if we introduce a \<open>fst_update\<close> and \<open>snd_update\<close> function. Furthermore, we can
|
||||
prove the access/update theorem in O(log(n)) steps by using simple
|
||||
rewrites on fst, snd, \<open>fst_update\<close> and \<open>snd_update\<close>.
|
||||
|
||||
The catch is that, although O(log(n)) steps were taken, the
|
||||
underlying type we converted to is a tuple tree of size
|
||||
O(n). Processing this term type wastes performance. We avoid this
|
||||
for large n by taking each subtree of size K and defining a new type
|
||||
isomorphic to that tuple subtree. A record can now be defined as
|
||||
isomorphic to a tuple tree of these O(n/K) new types, or, if \<open>n > K*K\<close>, we can repeat the process, until the record can be
|
||||
defined in terms of a tuple tree of complexity less than the
|
||||
constant K.
|
||||
|
||||
If we prove the access/update theorem on this type with the
|
||||
analogous steps to the tuple tree, we consume \<open>O(log(n)^2)\<close>
|
||||
time as the intermediate terms are \<open>O(log(n))\<close> in size and
|
||||
the types needed have size bounded by K. To enable this analogous
|
||||
traversal, we define the functions seen below: \<open>iso_tuple_fst\<close>, \<open>iso_tuple_snd\<close>, \<open>iso_tuple_fst_update\<close>
|
||||
and \<open>iso_tuple_snd_update\<close>. These functions generalise tuple
|
||||
operations by taking a parameter that encapsulates a tuple
|
||||
isomorphism. The rewrites needed on these functions now need an
|
||||
additional assumption which is that the isomorphism works.
|
||||
|
||||
These rewrites are typically used in a structured way. They are here
|
||||
presented as the introduction rule \<open>isomorphic_tuple.intros\<close>
|
||||
rather than as a rewrite rule set. The introduction form is an
|
||||
optimisation, as net matching can be performed at one term location
|
||||
for each step rather than the simplifier searching the term for
|
||||
possible pattern matches. The rule set is used as it is viewed
|
||||
outside the locale, with the locale assumption (that the isomorphism
|
||||
is valid) left as a rule assumption. All rules are structured to aid
|
||||
net matching, using either a point-free form or an encapsulating
|
||||
predicate.
|
||||
\<close>
|
||||
|
||||
subsection \<open>Operators and lemmas for types isomorphic to tuples\<close>
|
||||
|
||||
datatype (dead 'a, dead 'b, dead 'c) tuple_isomorphism =
|
||||
Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a"
|
||||
|
||||
primrec
|
||||
repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where
|
||||
"repr (Tuple_Isomorphism r a) = r"
|
||||
|
||||
primrec
|
||||
abst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'a" where
|
||||
"abst (Tuple_Isomorphism r a) = a"
|
||||
|
||||
definition
|
||||
iso_tuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" where
|
||||
"iso_tuple_fst isom = fst \<circ> repr isom"
|
||||
|
||||
definition
|
||||
iso_tuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" where
|
||||
"iso_tuple_snd isom = snd \<circ> repr isom"
|
||||
|
||||
definition
|
||||
iso_tuple_fst_update ::
|
||||
"('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" where
|
||||
"iso_tuple_fst_update isom f = abst isom \<circ> apfst f \<circ> repr isom"
|
||||
|
||||
definition
|
||||
iso_tuple_snd_update ::
|
||||
"('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" where
|
||||
"iso_tuple_snd_update isom f = abst isom \<circ> apsnd f \<circ> repr isom"
|
||||
|
||||
definition
|
||||
iso_tuple_cons ::
|
||||
"('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" where
|
||||
"iso_tuple_cons isom = curry (abst isom)"
|
||||
|
||||
|
||||
subsection \<open>Logical infrastructure for records\<close>
|
||||
|
||||
definition
|
||||
iso_tuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
|
||||
"iso_tuple_surjective_proof_assist x y f \<longleftrightarrow> f x = y"
|
||||
|
||||
definition
|
||||
iso_tuple_update_accessor_cong_assist ::
|
||||
"(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
|
||||
"iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>
|
||||
(\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
|
||||
|
||||
definition
|
||||
iso_tuple_update_accessor_eq_assist ::
|
||||
"(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
|
||||
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>
|
||||
upd f v = v' \<and> ac v = x \<and> iso_tuple_update_accessor_cong_assist upd ac"
|
||||
|
||||
lemma update_accessor_congruence_foldE:
|
||||
assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
|
||||
and r: "r = r'" and v: "ac r' = v'"
|
||||
and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
|
||||
shows "upd f r = upd f' r'"
|
||||
using uac r v [symmetric]
|
||||
apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>x. f' (ac r')) r'")
|
||||
apply (simp add: iso_tuple_update_accessor_cong_assist_def)
|
||||
apply (simp add: f)
|
||||
done
|
||||
|
||||
lemma update_accessor_congruence_unfoldE:
|
||||
"iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
|
||||
r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
|
||||
upd f r = upd f' r'"
|
||||
apply (erule(2) update_accessor_congruence_foldE)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma iso_tuple_update_accessor_cong_assist_id:
|
||||
"iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> upd id = id"
|
||||
by rule (simp add: iso_tuple_update_accessor_cong_assist_def)
|
||||
|
||||
lemma update_accessor_noopE:
|
||||
assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
|
||||
and ac: "f (ac x) = ac x"
|
||||
shows "upd f x = x"
|
||||
using uac
|
||||
by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def]
|
||||
cong: update_accessor_congruence_unfoldE [OF uac])
|
||||
|
||||
lemma update_accessor_noop_compE:
|
||||
assumes uac: "iso_tuple_update_accessor_cong_assist upd ac"
|
||||
and ac: "f (ac x) = ac x"
|
||||
shows "upd (g \<circ> f) x = upd g x"
|
||||
by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac])
|
||||
|
||||
lemma update_accessor_cong_assist_idI:
|
||||
"iso_tuple_update_accessor_cong_assist id id"
|
||||
by (simp add: iso_tuple_update_accessor_cong_assist_def)
|
||||
|
||||
lemma update_accessor_cong_assist_triv:
|
||||
"iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
|
||||
iso_tuple_update_accessor_cong_assist upd ac"
|
||||
by assumption
|
||||
|
||||
lemma update_accessor_accessor_eqE:
|
||||
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> ac v = x"
|
||||
by (simp add: iso_tuple_update_accessor_eq_assist_def)
|
||||
|
||||
lemma update_accessor_updator_eqE:
|
||||
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> upd f v = v'"
|
||||
by (simp add: iso_tuple_update_accessor_eq_assist_def)
|
||||
|
||||
lemma iso_tuple_update_accessor_eq_assist_idI:
|
||||
"v' = f v \<Longrightarrow> iso_tuple_update_accessor_eq_assist id id v f v' v"
|
||||
by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI)
|
||||
|
||||
lemma iso_tuple_update_accessor_eq_assist_triv:
|
||||
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
|
||||
iso_tuple_update_accessor_eq_assist upd ac v f v' x"
|
||||
by assumption
|
||||
|
||||
lemma iso_tuple_update_accessor_cong_from_eq:
|
||||
"iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
|
||||
iso_tuple_update_accessor_cong_assist upd ac"
|
||||
by (simp add: iso_tuple_update_accessor_eq_assist_def)
|
||||
|
||||
lemma iso_tuple_surjective_proof_assistI:
|
||||
"f x = y \<Longrightarrow> iso_tuple_surjective_proof_assist x y f"
|
||||
by (simp add: iso_tuple_surjective_proof_assist_def)
|
||||
|
||||
lemma iso_tuple_surjective_proof_assist_idE:
|
||||
"iso_tuple_surjective_proof_assist x y id \<Longrightarrow> x = y"
|
||||
by (simp add: iso_tuple_surjective_proof_assist_def)
|
||||
|
||||
locale isomorphic_tuple =
|
||||
fixes isom :: "('a, 'b, 'c) tuple_isomorphism"
|
||||
assumes repr_inv: "\<And>x. abst isom (repr isom x) = x"
|
||||
and abst_inv: "\<And>y. repr isom (abst isom y) = y"
|
||||
begin
|
||||
|
||||
lemma repr_inj: "repr isom x = repr isom y \<longleftrightarrow> x = y"
|
||||
by (auto dest: arg_cong [of "repr isom x" "repr isom y" "abst isom"]
|
||||
simp add: repr_inv)
|
||||
|
||||
lemma abst_inj: "abst isom x = abst isom y \<longleftrightarrow> x = y"
|
||||
by (auto dest: arg_cong [of "abst isom x" "abst isom y" "repr isom"]
|
||||
simp add: abst_inv)
|
||||
|
||||
lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj
|
||||
|
||||
lemma iso_tuple_access_update_fst_fst:
|
||||
"f \<circ> h g = j \<circ> f \<Longrightarrow>
|
||||
(f \<circ> iso_tuple_fst isom) \<circ> (iso_tuple_fst_update isom \<circ> h) g =
|
||||
j \<circ> (f \<circ> iso_tuple_fst isom)"
|
||||
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps
|
||||
fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_access_update_snd_snd:
|
||||
"f \<circ> h g = j \<circ> f \<Longrightarrow>
|
||||
(f \<circ> iso_tuple_snd isom) \<circ> (iso_tuple_snd_update isom \<circ> h) g =
|
||||
j \<circ> (f \<circ> iso_tuple_snd isom)"
|
||||
by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps
|
||||
fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_access_update_fst_snd:
|
||||
"(f \<circ> iso_tuple_fst isom) \<circ> (iso_tuple_snd_update isom \<circ> h) g =
|
||||
id \<circ> (f \<circ> iso_tuple_fst isom)"
|
||||
by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps
|
||||
fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_access_update_snd_fst:
|
||||
"(f \<circ> iso_tuple_snd isom) \<circ> (iso_tuple_fst_update isom \<circ> h) g =
|
||||
id \<circ> (f \<circ> iso_tuple_snd isom)"
|
||||
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps
|
||||
fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_update_swap_fst_fst:
|
||||
"h f \<circ> j g = j g \<circ> h f \<Longrightarrow>
|
||||
(iso_tuple_fst_update isom \<circ> h) f \<circ> (iso_tuple_fst_update isom \<circ> j) g =
|
||||
(iso_tuple_fst_update isom \<circ> j) g \<circ> (iso_tuple_fst_update isom \<circ> h) f"
|
||||
by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_update_swap_snd_snd:
|
||||
"h f \<circ> j g = j g \<circ> h f \<Longrightarrow>
|
||||
(iso_tuple_snd_update isom \<circ> h) f \<circ> (iso_tuple_snd_update isom \<circ> j) g =
|
||||
(iso_tuple_snd_update isom \<circ> j) g \<circ> (iso_tuple_snd_update isom \<circ> h) f"
|
||||
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_update_swap_fst_snd:
|
||||
"(iso_tuple_snd_update isom \<circ> h) f \<circ> (iso_tuple_fst_update isom \<circ> j) g =
|
||||
(iso_tuple_fst_update isom \<circ> j) g \<circ> (iso_tuple_snd_update isom \<circ> h) f"
|
||||
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def
|
||||
simps fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_update_swap_snd_fst:
|
||||
"(iso_tuple_fst_update isom \<circ> h) f \<circ> (iso_tuple_snd_update isom \<circ> j) g =
|
||||
(iso_tuple_snd_update isom \<circ> j) g \<circ> (iso_tuple_fst_update isom \<circ> h) f"
|
||||
by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps
|
||||
fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_update_compose_fst_fst:
|
||||
"h f \<circ> j g = k (f \<circ> g) \<Longrightarrow>
|
||||
(iso_tuple_fst_update isom \<circ> h) f \<circ> (iso_tuple_fst_update isom \<circ> j) g =
|
||||
(iso_tuple_fst_update isom \<circ> k) (f \<circ> g)"
|
||||
by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_update_compose_snd_snd:
|
||||
"h f \<circ> j g = k (f \<circ> g) \<Longrightarrow>
|
||||
(iso_tuple_snd_update isom \<circ> h) f \<circ> (iso_tuple_snd_update isom \<circ> j) g =
|
||||
(iso_tuple_snd_update isom \<circ> k) (f \<circ> g)"
|
||||
by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff)
|
||||
|
||||
lemma iso_tuple_surjective_proof_assist_step:
|
||||
"iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom \<circ> f) \<Longrightarrow>
|
||||
iso_tuple_surjective_proof_assist v b (iso_tuple_snd isom \<circ> f) \<Longrightarrow>
|
||||
iso_tuple_surjective_proof_assist v (iso_tuple_cons isom a b) f"
|
||||
by (clarsimp simp: iso_tuple_surjective_proof_assist_def simps
|
||||
iso_tuple_fst_def iso_tuple_snd_def iso_tuple_cons_def)
|
||||
|
||||
lemma iso_tuple_fst_update_accessor_cong_assist:
|
||||
assumes "iso_tuple_update_accessor_cong_assist f g"
|
||||
shows "iso_tuple_update_accessor_cong_assist
|
||||
(iso_tuple_fst_update isom \<circ> f) (g \<circ> iso_tuple_fst isom)"
|
||||
proof -
|
||||
from assms have "f id = id"
|
||||
by (rule iso_tuple_update_accessor_cong_assist_id)
|
||||
with assms show ?thesis
|
||||
by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
|
||||
iso_tuple_fst_update_def iso_tuple_fst_def)
|
||||
qed
|
||||
|
||||
lemma iso_tuple_snd_update_accessor_cong_assist:
|
||||
assumes "iso_tuple_update_accessor_cong_assist f g"
|
||||
shows "iso_tuple_update_accessor_cong_assist
|
||||
(iso_tuple_snd_update isom \<circ> f) (g \<circ> iso_tuple_snd isom)"
|
||||
proof -
|
||||
from assms have "f id = id"
|
||||
by (rule iso_tuple_update_accessor_cong_assist_id)
|
||||
with assms show ?thesis
|
||||
by (clarsimp simp: iso_tuple_update_accessor_cong_assist_def simps
|
||||
iso_tuple_snd_update_def iso_tuple_snd_def)
|
||||
qed
|
||||
|
||||
lemma iso_tuple_fst_update_accessor_eq_assist:
|
||||
assumes "iso_tuple_update_accessor_eq_assist f g a u a' v"
|
||||
shows "iso_tuple_update_accessor_eq_assist
|
||||
(iso_tuple_fst_update isom \<circ> f) (g \<circ> iso_tuple_fst isom)
|
||||
(iso_tuple_cons isom a b) u (iso_tuple_cons isom a' b) v"
|
||||
proof -
|
||||
from assms have "f id = id"
|
||||
by (auto simp add: iso_tuple_update_accessor_eq_assist_def
|
||||
intro: iso_tuple_update_accessor_cong_assist_id)
|
||||
with assms show ?thesis
|
||||
by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
|
||||
iso_tuple_fst_update_def iso_tuple_fst_def
|
||||
iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
|
||||
qed
|
||||
|
||||
lemma iso_tuple_snd_update_accessor_eq_assist:
|
||||
assumes "iso_tuple_update_accessor_eq_assist f g b u b' v"
|
||||
shows "iso_tuple_update_accessor_eq_assist
|
||||
(iso_tuple_snd_update isom \<circ> f) (g \<circ> iso_tuple_snd isom)
|
||||
(iso_tuple_cons isom a b) u (iso_tuple_cons isom a b') v"
|
||||
proof -
|
||||
from assms have "f id = id"
|
||||
by (auto simp add: iso_tuple_update_accessor_eq_assist_def
|
||||
intro: iso_tuple_update_accessor_cong_assist_id)
|
||||
with assms show ?thesis
|
||||
by (clarsimp simp: iso_tuple_update_accessor_eq_assist_def
|
||||
iso_tuple_snd_update_def iso_tuple_snd_def
|
||||
iso_tuple_update_accessor_cong_assist_def iso_tuple_cons_def simps)
|
||||
qed
|
||||
|
||||
lemma iso_tuple_cons_conj_eqI:
|
||||
"a = c \<and> b = d \<and> P \<longleftrightarrow> Q \<Longrightarrow>
|
||||
iso_tuple_cons isom a b = iso_tuple_cons isom c d \<and> P \<longleftrightarrow> Q"
|
||||
by (clarsimp simp: iso_tuple_cons_def simps)
|
||||
|
||||
lemmas intros =
|
||||
iso_tuple_access_update_fst_fst
|
||||
iso_tuple_access_update_snd_snd
|
||||
iso_tuple_access_update_fst_snd
|
||||
iso_tuple_access_update_snd_fst
|
||||
iso_tuple_update_swap_fst_fst
|
||||
iso_tuple_update_swap_snd_snd
|
||||
iso_tuple_update_swap_fst_snd
|
||||
iso_tuple_update_swap_snd_fst
|
||||
iso_tuple_update_compose_fst_fst
|
||||
iso_tuple_update_compose_snd_snd
|
||||
iso_tuple_surjective_proof_assist_step
|
||||
iso_tuple_fst_update_accessor_eq_assist
|
||||
iso_tuple_snd_update_accessor_eq_assist
|
||||
iso_tuple_fst_update_accessor_cong_assist
|
||||
iso_tuple_snd_update_accessor_cong_assist
|
||||
iso_tuple_cons_conj_eqI
|
||||
|
||||
end
|
||||
|
||||
lemma isomorphic_tuple_intro:
|
||||
fixes repr abst
|
||||
assumes repr_inj: "\<And>x y. repr x = repr y \<longleftrightarrow> x = y"
|
||||
and abst_inv: "\<And>z. repr (abst z) = z"
|
||||
and v: "v \<equiv> Tuple_Isomorphism repr abst"
|
||||
shows "isomorphic_tuple v"
|
||||
proof
|
||||
fix x have "repr (abst (repr x)) = repr x"
|
||||
by (simp add: abst_inv)
|
||||
then show "Test.abst v (Test.repr v x) = x"
|
||||
by (simp add: v repr_inj)
|
||||
next
|
||||
fix y
|
||||
show "Test.repr v (Test.abst v y) = y"
|
||||
by (simp add: v) (fact abst_inv)
|
||||
qed
|
||||
|
||||
definition
|
||||
"tuple_iso_tuple \<equiv> Tuple_Isomorphism id id"
|
||||
|
||||
lemma tuple_iso_tuple:
|
||||
"isomorphic_tuple tuple_iso_tuple"
|
||||
by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def)
|
||||
|
||||
lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
|
||||
by simp
|
||||
|
||||
lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
|
||||
by simp
|
||||
|
||||
lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
|
||||
by simp
|
||||
|
||||
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
|
||||
by simp
|
||||
|
||||
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
|
||||
by (simp add: comp_def)
|
||||
|
||||
|
||||
subsection \<open>Concrete record syntax\<close>
|
||||
|
||||
nonterminal
|
||||
ident and
|
||||
field_type and
|
||||
field_types and
|
||||
field and
|
||||
fields and
|
||||
field_update and
|
||||
field_updates
|
||||
|
||||
syntax
|
||||
"_constify" :: "id => ident" ("_")
|
||||
"_constify" :: "longid => ident" ("_")
|
||||
|
||||
"_field_type" :: "ident => type => field_type" ("(2_ ::/ _)")
|
||||
"" :: "field_type => field_types" ("_")
|
||||
"_field_types" :: "field_type => field_types => field_types" ("_,/ _")
|
||||
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
|
||||
"_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
|
||||
|
||||
"_field" :: "ident => 'a => field" ("(2_ =/ _)")
|
||||
"" :: "field => fields" ("_")
|
||||
"_fields" :: "field => fields => fields" ("_,/ _")
|
||||
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
|
||||
"_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
|
||||
|
||||
"_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)")
|
||||
"" :: "field_update => field_updates" ("_")
|
||||
"_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _")
|
||||
"_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
|
||||
|
||||
syntax (ASCII)
|
||||
"_record_type" :: "field_types => type" ("(3'(| _ |'))")
|
||||
"_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))")
|
||||
"_record" :: "fields => 'a" ("(3'(| _ |'))")
|
||||
"_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))")
|
||||
"_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900)
|
||||
|
||||
|
||||
subsection \<open>Record package\<close>
|
||||
|
||||
ML_file "test.ML"
|
||||
|
||||
hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
|
||||
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
|
||||
iso_tuple_surjective_proof_assist iso_tuple_update_accessor_cong_assist
|
||||
iso_tuple_update_accessor_eq_assist tuple_iso_tuple
|
||||
|
||||
end
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -26,7 +26,7 @@ theory Isa_COL
|
|||
keywords "title*" "subtitle*"
|
||||
"chapter*" "section*" "paragraph*"
|
||||
"subsection*" "subsubsection*"
|
||||
"figure*" "listing*" :: document_body
|
||||
"figure*" "listing*" "frame*" :: document_body
|
||||
|
||||
begin
|
||||
|
||||
|
|
@ -269,15 +269,24 @@ val mt_fig_content = {relative_width = 100,
|
|||
relative_height = 100,
|
||||
caption = Input.empty }: fig_content
|
||||
|
||||
fun upd_relative_width key {relative_width,relative_height,caption } : fig_content =
|
||||
{relative_width = key,relative_height = relative_height,caption = caption}: fig_content
|
||||
fun make_fig_content (relative_width, relative_height, caption) =
|
||||
{relative_width = relative_width, relative_height = relative_height, caption = caption}
|
||||
|
||||
fun upd_relative_height key {relative_width,relative_height,caption } : fig_content =
|
||||
{relative_width = relative_width,relative_height = key,caption = caption}: fig_content
|
||||
fun upd_fig_content f =
|
||||
fn {relative_width, relative_height, caption} =>
|
||||
make_fig_content (f (relative_width, relative_height, caption))
|
||||
|
||||
fun upd_caption key {relative_width,relative_height,caption} : fig_content =
|
||||
{relative_width = relative_width,relative_height = relative_height,caption= key}: fig_content
|
||||
fun upd_relative_width f =
|
||||
upd_fig_content (fn (relative_width, relative_height, caption) =>
|
||||
(f relative_width, relative_height, caption))
|
||||
|
||||
fun upd_relative_height f =
|
||||
upd_fig_content (fn (relative_width, relative_height, caption) =>
|
||||
(relative_width, f relative_height, caption))
|
||||
|
||||
fun upd_caption f =
|
||||
upd_fig_content (fn (relative_width, relative_height, caption) =>
|
||||
(relative_width, relative_height, f caption))
|
||||
|
||||
val widthN = "width"
|
||||
val heightN = "height"
|
||||
|
|
@ -288,11 +297,11 @@ fun fig_content_modes (ctxt, toks) =
|
|||
(Args.parens
|
||||
(Parse.list1
|
||||
( (Args.$$$ widthN |-- Args.$$$ "=" -- Parse.int
|
||||
>> (fn (_, k) => upd_relative_width k))
|
||||
>> (fn (_, k) => upd_relative_width (K k)))
|
||||
|| (Args.$$$ heightN |-- Args.$$$ "=" -- Parse.int
|
||||
>> (fn (_, k) => upd_relative_height k))
|
||||
>> (fn (_, k) => upd_relative_height (K k)))
|
||||
|| (Args.$$$ captionN |-- Args.$$$ "=" -- Parse.document_source
|
||||
>> (fn (_, k) => upd_caption k))
|
||||
>> (fn (_, k) => upd_caption (K k)))
|
||||
))) [K mt_fig_content])
|
||||
: (fig_content -> fig_content) list parser)
|
||||
>> (foldl1 (op #>)))
|
||||
|
|
@ -322,25 +331,34 @@ fun generate_caption ctxt caption =
|
|||
in
|
||||
drop_latex_macros cap_txt
|
||||
end
|
||||
|
||||
fun process_args cfg_trans =
|
||||
let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content
|
||||
val _ = if relative_width < 0 orelse relative_height <0
|
||||
then error("negative parameter.")
|
||||
else ()
|
||||
val wdth_val_s = Real.toString((Real.fromInt relative_width)
|
||||
/ (Real.fromInt 100))^"\\textwidth"
|
||||
val ht_s= if relative_height = 100
|
||||
then ""
|
||||
else "height="
|
||||
^ Real.toString((Real.fromInt relative_height)
|
||||
/ (Real.fromInt 100))
|
||||
^ "\\textheight"
|
||||
in (wdth_val_s, ht_s, caption) end
|
||||
|
||||
fun fig_content ctxt (cfg_trans,file:Input.source) =
|
||||
let val {relative_width,relative_height,caption} = cfg_trans mt_fig_content
|
||||
val _ = if relative_width < 0 orelse relative_height <0 then error("negative parameter.")
|
||||
else ()
|
||||
val wdth_val_s = Real.toString((Real.fromInt relative_width)
|
||||
/ (Real.fromInt 100))^"\\textwidth"
|
||||
val ht_s= if relative_height = 100 then ""
|
||||
else "height="^Real.toString((Real.fromInt relative_height)
|
||||
/ (Real.fromInt 100)) ^"\\textheight"
|
||||
val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s])
|
||||
val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s])
|
||||
val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
|
||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||
let val (wdth_val_s, ht_s, caption) = process_args cfg_trans
|
||||
val arg_single = enclose "[" "]" (commas ["keepaspectratio","width="^wdth_val_s,ht_s])
|
||||
val arg = enclose "[" "]" (commas ["keepaspectratio","width=\\textwidth",ht_s])
|
||||
val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
|
||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||
|
||||
in if Input.string_of(caption) = "" then
|
||||
in if Input.string_of(caption) = "" then
|
||||
file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> Latex.macro ("includegraphics"^arg_single)
|
||||
else
|
||||
else
|
||||
file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> (fn X => (Latex.string ("{"^wdth_val_s^"}"))
|
||||
|
|
@ -349,7 +367,7 @@ fun fig_content ctxt (cfg_trans,file:Input.source) =
|
|||
@ (Latex.macro "caption" (generate_caption ctxt caption)))
|
||||
|> (Latex.environment ("subcaptionblock") )
|
||||
(* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *)
|
||||
end
|
||||
end
|
||||
|
||||
fun fig_content_antiquotation name scan =
|
||||
(Document_Output.antiquotation_raw_embedded name
|
||||
|
|
@ -357,8 +375,29 @@ fun fig_content_antiquotation name scan =
|
|||
(fig_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text));
|
||||
|
||||
|
||||
fun figure_content ctxt (cfg_trans,file:Input.source) =
|
||||
let val _ = Resources.check_file ctxt (SOME (get_document_dir ctxt)) file
|
||||
(* ToDo: must be declared source of type png or jpeg or pdf, ... *)
|
||||
val (wdth_val_s, ht_s, caption) = process_args cfg_trans
|
||||
val args = ["keepaspectratio","width=" ^ wdth_val_s, ht_s]
|
||||
|> commas
|
||||
|> enclose "[" "]"
|
||||
in file
|
||||
|> (Latex.string o Input.string_of)
|
||||
|> Latex.macro ("includegraphics" ^ args)
|
||||
|> (fn X => X @ Latex.macro "caption" (generate_caption ctxt caption))
|
||||
|> Latex.environment ("figure")
|
||||
end
|
||||
|
||||
fun figure_antiquotation name scan =
|
||||
(Document_Output.antiquotation_raw_embedded name
|
||||
(scan : ((fig_content -> fig_content) * Input.source) context_parser)
|
||||
(figure_content : Proof.context -> (fig_content -> fig_content) * Input.source -> Latex.text));
|
||||
|
||||
val _ = Theory.setup
|
||||
( fig_content_antiquotation \<^binding>\<open>fig_content\<close>
|
||||
(fig_content_modes -- Scan.lift(Parse.path_input))
|
||||
#> figure_antiquotation \<^binding>\<open>figure_content\<close>
|
||||
(fig_content_modes -- Scan.lift(Parse.path_input)))
|
||||
|
||||
\<close>
|
||||
|
|
@ -372,9 +411,9 @@ fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
|
|||
handle TERM _ => error "Illegal int format."
|
||||
in
|
||||
(case YXML.content_of str of
|
||||
"relative_width" => upd_relative_width (conv_int value)
|
||||
"relative_width" => upd_relative_width (K (conv_int value))
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| "relative_height" => upd_relative_height (conv_int value)
|
||||
| "relative_height" => upd_relative_height (K (conv_int value))
|
||||
o convert_meta_args ctxt (X, R )
|
||||
| "file_src" => convert_meta_args ctxt (X, R)
|
||||
| s => error("!undefined attribute:"^s))
|
||||
|
|
@ -404,11 +443,11 @@ fun float_command (name, pos) descr cid =
|
|||
|> Latex.string)
|
||||
fun parse_and_tex (margs as (((oid, _),_), _), cap_src) ctxt =
|
||||
(convert_src_from_margs ctxt margs)
|
||||
|> pair (upd_caption Input.empty #> convert_meta_args ctxt margs)
|
||||
|> pair (upd_caption (K Input.empty) #> convert_meta_args ctxt margs)
|
||||
|> fig_content ctxt
|
||||
|> generate_fig_ltx_ctxt ctxt cap_src oid
|
||||
|> (Latex.environment ("figure") )
|
||||
in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
|
||||
in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
|
||||
end
|
||||
|
||||
fun listing_command (name, pos) descr cid =
|
||||
|
|
@ -421,7 +460,7 @@ fun listing_command (name, pos) descr cid =
|
|||
{define = true} oid pos (set_default_class cid_pos) doc_attrs
|
||||
fun parse_and_tex (margs as (((_, pos),_), _), _) _ =
|
||||
ISA_core.err ("Not yet implemented.\n Please use text*[oid::listing]\<open>\<close> instead.") pos
|
||||
in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
|
||||
in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -715,5 +754,144 @@ text\<open> @{table_inline [display] (cell_placing = center,cell_height =\<open
|
|||
|
||||
(*>*)
|
||||
|
||||
text\<open>beamer support\<close>
|
||||
(* Under development *)
|
||||
|
||||
doc_class frame =
|
||||
options :: string
|
||||
frametitle :: string
|
||||
framesubtitle :: string
|
||||
|
||||
ML\<open>
|
||||
type frame = {options: Input.source
|
||||
, frametitle: Input.source
|
||||
, framesubtitle: Input.source}
|
||||
|
||||
val empty_frame = {options = Input.empty
|
||||
, frametitle = Input.empty
|
||||
, framesubtitle = Input.empty}: frame
|
||||
|
||||
fun make_frame (options, frametitle, framesubtitle) =
|
||||
{options = options, frametitle = frametitle, framesubtitle = framesubtitle}
|
||||
|
||||
fun upd_frame f =
|
||||
fn {options, frametitle, framesubtitle} => make_frame (f (options, frametitle, framesubtitle))
|
||||
|
||||
fun upd_options f =
|
||||
upd_frame (fn (options, frametitle, framesubtitle) => (f options, frametitle, framesubtitle))
|
||||
|
||||
fun upd_frametitle f =
|
||||
upd_frame (fn (options, frametitle, framesubtitle) => (options, f frametitle, framesubtitle))
|
||||
|
||||
fun upd_framesubtitle f =
|
||||
upd_frame (fn (options, frametitle, framesubtitle) => (options, frametitle, f framesubtitle))
|
||||
|
||||
type block = {title: Input.source}
|
||||
|
||||
val empty_block = {title = Input.empty}
|
||||
|
||||
fun make_block title = {title = title}
|
||||
|
||||
fun upd_block f =
|
||||
fn {title} => make_block (f title)
|
||||
|
||||
fun upd_block_title f =
|
||||
upd_block (fn title => f title)
|
||||
|
||||
val unenclose_end = unenclose
|
||||
val unenclose_string = unenclose o unenclose o unenclose_end
|
||||
|
||||
fun read_string s =
|
||||
let val symbols = unenclose_end s |> Symbol_Pos.explode0
|
||||
in if hd symbols |> fst |> equal Symbol.open_
|
||||
then Token.read_cartouche symbols |> Token.input_of
|
||||
else unenclose_string s |> Syntax.read_input
|
||||
end
|
||||
|
||||
val block_titleN = "title"
|
||||
|
||||
fun block_modes (ctxt, toks) =
|
||||
let val (y, toks') = ((((Scan.optional
|
||||
(Args.parens
|
||||
(Parse.list1
|
||||
((Args.$$$ block_titleN |-- Args.$$$ "=" -- Parse.document_source
|
||||
>> (fn (_, k) => upd_block_title (K k)))
|
||||
))) [K empty_block])
|
||||
: (block -> block) list parser)
|
||||
>> (foldl1 (op #>)))
|
||||
: (block -> block) parser)
|
||||
(toks)
|
||||
in (y, (ctxt, toks')) end
|
||||
|
||||
fun process_args cfg_trans =
|
||||
let val {title} = cfg_trans empty_block
|
||||
in title end
|
||||
|
||||
fun block ctxt (cfg_trans,src) =
|
||||
let val title = process_args cfg_trans
|
||||
in Latex.string "{"
|
||||
@ (title |> Document_Output.output_document ctxt {markdown = false})
|
||||
@ Latex.string "}"
|
||||
@ (src |> Document_Output.output_document ctxt {markdown = false})
|
||||
|> (Latex.environment "block")
|
||||
end
|
||||
|
||||
fun block_antiquotation name scan =
|
||||
(Document_Output.antiquotation_raw_embedded name
|
||||
(scan : ((block -> block) * Input.source) context_parser)
|
||||
(block: Proof.context -> (block -> block) * Input.source -> Latex.text));
|
||||
|
||||
val _ = block_antiquotation \<^binding>\<open>block\<close> (block_modes -- Scan.lift Parse.document_source)
|
||||
|> Theory.setup
|
||||
|
||||
fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
|
||||
(case YXML.content_of str of
|
||||
"frametitle" => upd_frametitle (K(YXML.content_of value |> read_string))
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| "framesubtitle" => upd_framesubtitle (K(YXML.content_of value |> read_string))
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| "options" => upd_options (K(YXML.content_of value |> read_string))
|
||||
o convert_meta_args ctxt (X, R)
|
||||
| s => error("!undefined attribute:"^s))
|
||||
| convert_meta_args _ (_,[]) = I
|
||||
|
||||
fun frame_command (name, pos) descr cid =
|
||||
let fun set_default_class NONE = SOME(cid,pos)
|
||||
|set_default_class (SOME X) = SOME X
|
||||
fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
|
||||
Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false}
|
||||
{is_inline = true}
|
||||
{define = true} oid pos (set_default_class cid_pos) doc_attrs
|
||||
fun titles_src ctxt frametitle framesubtitle src =
|
||||
Latex.string "{"
|
||||
@ Document_Output.output_document ctxt {markdown = false} frametitle
|
||||
@ Latex.string "}"
|
||||
@ Latex.string "{"
|
||||
@ (Document_Output.output_document ctxt {markdown = false} framesubtitle)
|
||||
@ Latex.string "}"
|
||||
@ Document_Output.output_document ctxt {markdown = true} src
|
||||
fun generate_src_ltx_ctxt ctxt src cfg_trans =
|
||||
let val {options, frametitle, framesubtitle} = cfg_trans empty_frame
|
||||
in
|
||||
let val options_str = Input.string_of options
|
||||
in if options_str = ""
|
||||
then titles_src ctxt frametitle framesubtitle src
|
||||
else (options_str
|
||||
|> enclose "[" "]"
|
||||
|> Latex.string)
|
||||
@ titles_src ctxt frametitle framesubtitle src
|
||||
end
|
||||
end
|
||||
fun parse_and_tex (margs, src) ctxt =
|
||||
convert_meta_args ctxt margs
|
||||
|> generate_src_ltx_ctxt ctxt src
|
||||
|> Latex.environment ("frame")
|
||||
|> Latex.environment ("isamarkuptext")
|
||||
in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex
|
||||
end
|
||||
|
||||
val _ = frame_command \<^command_keyword>\<open>frame*\<close> "frame environment" "Isa_COL.frame" ;
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -2199,22 +2199,25 @@ fun document_output_reports name {markdown, body} sem_attrs transform_attr meta_
|
|||
|
||||
fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
|
||||
Outer_Syntax.command (name, pos) descr
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
|
||||
(fn (meta_args, text) =>
|
||||
Toplevel.theory' (fn _ => cmd meta_args)
|
||||
((Toplevel.presentation_context
|
||||
#> document_output_reports name mark sem_attrs transform_attr meta_args text
|
||||
#> SOME): Toplevel.state -> Latex.text option)) );
|
||||
|
||||
fun onto_macro_cmd_output_reports output_cmd (meta_args, text) ctxt =
|
||||
let
|
||||
val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
|
||||
in output_cmd (meta_args, text) ctxt end
|
||||
|
||||
fun float_command (name, pos) descr
|
||||
cmd output_figure =
|
||||
fun onto_macro_cmd_command (name, pos) descr cmd output_cmd =
|
||||
Outer_Syntax.command (name, pos) descr
|
||||
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
|
||||
(fn (meta_args, text) =>
|
||||
Toplevel.theory' (fn _ => cmd meta_args)
|
||||
(Toplevel.presentation_context
|
||||
#> output_figure (meta_args, text)
|
||||
#> onto_macro_cmd_output_reports output_cmd (meta_args, text)
|
||||
#> SOME)))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -51,7 +51,13 @@ definition rep1 :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrace>(_)\<rbrace>\<^sup
|
|||
|
||||
definition opt :: "'a rexp \<Rightarrow> 'a rexp" ("\<lbrakk>(_)\<rbrakk>")
|
||||
where "\<lbrakk>A\<rbrakk> \<equiv> A || One"
|
||||
|
||||
|
||||
find_consts name:"RegExpI*"
|
||||
|
||||
ML\<open>
|
||||
val t = Sign.syn_of \<^theory>
|
||||
\<close>
|
||||
print_syntax
|
||||
value "Star (Conc(Alt (Atom(CHR ''a'')) (Atom(CHR ''b''))) (Atom(CHR ''c'')))"
|
||||
text\<open>or better equivalently:\<close>
|
||||
value "\<lbrace>(\<lfloor>CHR ''a''\<rfloor> || \<lfloor>CHR ''b''\<rfloor>) ~~ \<lfloor>CHR ''c''\<rfloor>\<rbrace>\<^sup>*"
|
||||
|
|
@ -240,6 +246,8 @@ no_notation Star ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
|
|||
no_notation Plus (infixr "||" 55)
|
||||
no_notation Times (infixr "~~" 60)
|
||||
no_notation Atom ("\<lfloor>_\<rfloor>" 65)
|
||||
no_notation rep1 ("\<lbrace>(_)\<rbrace>\<^sup>+")
|
||||
no_notation opt ("\<lbrakk>(_)\<rbrakk>")
|
||||
|
||||
ML\<open>
|
||||
structure RegExpInterface_Notations =
|
||||
|
|
@ -248,7 +256,9 @@ val Star = (\<^term>\<open>Regular_Exp.Star\<close>, Mixfix (Syntax.read_input "
|
|||
val Plus = (\<^term>\<open>Regular_Exp.Plus\<close>, Infixr (Syntax.read_input "||", 55, Position.no_range))
|
||||
val Times = (\<^term>\<open>Regular_Exp.Times\<close>, Infixr (Syntax.read_input "~~", 60, Position.no_range))
|
||||
val Atom = (\<^term>\<open>Regular_Exp.Atom\<close>, Mixfix (Syntax.read_input "\<lfloor>_\<rfloor>", [], 65, Position.no_range))
|
||||
val notations = [Star, Plus, Times, Atom]
|
||||
val opt = (\<^term>\<open>RegExpInterface.opt\<close>, Mixfix (Syntax.read_input "\<lbrakk>(_)\<rbrakk>", [], 1000, Position.no_range))
|
||||
val rep1 = (\<^term>\<open>RegExpInterface.rep1\<close>, Mixfix (Syntax.read_input "\<lbrace>(_)\<rbrace>\<^sup>+", [], 1000, Position.no_range))
|
||||
val notations = [Star, Plus, Times, Atom, rep1, opt]
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue