Merge commit '59b082d09d55d55ef6c6f8bd8e821122dddf3574' into isabelle_nightly
This commit is contained in:
commit
0a3259fbca
|
|
@ -113,9 +113,9 @@ doc_class inv_test4 = inv_test2 +
|
|||
invariant inv_test4' :: "a (d \<sigma>) = 2"
|
||||
|
||||
text*[inv_test1_instance::inv_test1, a=2]\<open>\<close>
|
||||
text*[inv_test3_instance::inv_test3, a=2, b="@{inv-test1 \<open>inv_test1_instance\<close>}" ]\<open>\<close>
|
||||
text*[inv_test4_instance::inv_test4, b="@{inv-test1 \<open>inv_test1_instance\<close>}"
|
||||
, c=1, d="@{inv-test3 \<open>inv_test3_instance\<close>}"]\<open>\<close>
|
||||
text*[inv_test3_instance::inv_test3, a=2, b="@{inv_test1 \<open>inv_test1_instance\<close>}" ]\<open>\<close>
|
||||
text*[inv_test4_instance::inv_test4, b="@{inv_test1 \<open>inv_test1_instance\<close>}"
|
||||
, c=1, d="@{inv_test3 \<open>inv_test3_instance\<close>}"]\<open>\<close>
|
||||
|
||||
text\<open>To support invariant on attributes in attributes
|
||||
and invariant on attributes of the superclasses,
|
||||
|
|
@ -207,15 +207,15 @@ update_instance*[introduction2::Introduction
|
|||
text\<open>Use of the instance @{docitem_name "church'"}
|
||||
to instantiate a \<^doc_class>\<open>scholarly_paper.introduction\<close> class:\<close>
|
||||
text*[introduction2'::scholarly_paper.introduction,
|
||||
main_author = "Some @{scholarly-paper.author \<open>church'\<close>}", level = "Some 2"]\<open>\<close>
|
||||
main_author = "Some @{scholarly_paper.author \<open>church'\<close>}", level = "Some 2"]\<open>\<close>
|
||||
|
||||
value*\<open>@{scholarly-paper.author \<open>church'\<close>}\<close>
|
||||
value*\<open>@{scholarly_paper.author \<open>church'\<close>}\<close>
|
||||
value*\<open>@{author \<open>church\<close>}\<close>
|
||||
value*\<open>@{Concept-High-Level-Invariants.author \<open>church\<close>}\<close>
|
||||
value*\<open>@{Concept_High_Level_Invariants.author \<open>church\<close>}\<close>
|
||||
|
||||
value*\<open>@{scholarly-paper.author-instances}\<close>
|
||||
value*\<open>@{author-instances}\<close>
|
||||
value*\<open>@{Concept-High-Level-Invariants.author-instances}\<close>
|
||||
value*\<open>@{scholarly_paper.author_instances}\<close>
|
||||
value*\<open>@{author_instances}\<close>
|
||||
value*\<open>@{Concept_High_Level_Invariants.author_instances}\<close>
|
||||
|
||||
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
|
|
|
|||
|
|
@ -99,7 +99,7 @@ text*[cc_assumption_test_ref::cc_assumption_test]\<open>\<close>
|
|||
|
||||
definition tag_l :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where "tag_l \<equiv> \<lambda>x y. y"
|
||||
|
||||
lemma* tagged : "tag_l @{cc-assumption-test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
lemma* tagged : "tag_l @{cc_assumption_test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
by (simp add: tag_l_def)
|
||||
|
||||
find_theorems name:tagged "(_::cc_assumption_test \<Rightarrow> _ \<Rightarrow> _) _ _ \<Longrightarrow>_"
|
||||
|
|
|
|||
|
|
@ -150,10 +150,7 @@ term*\<open>r @{F \<open>xcv4\<close>}\<close>
|
|||
text\<open>We declare a new text element. Note that the class name contains an underscore "\_".\<close>
|
||||
text*[te::text_element]\<open>Lorem ipsum...\<close>
|
||||
|
||||
text\<open>Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
this term antiquotation has to be denoted like this: @{term_ \<open>@{text-element \<open>te\<close>}\<close>}.
|
||||
We need to substitute an hyphen "-" for the underscore "\_".\<close>
|
||||
term*\<open>@{text-element \<open>te\<close>}\<close>
|
||||
term*\<open>@{text_element \<open>te\<close>}\<close>
|
||||
|
||||
text\<open>Terms containing term antiquotations can be checked and evaluated
|
||||
using \<^theory_text>\<open>term_\<close> and \<^theory_text>\<open>value_\<close> text antiquotations respectively:
|
||||
|
|
|
|||
|
|
@ -146,17 +146,17 @@ text*[test2Z::Z, z=4]\<open>lorem ipsum...\<close>
|
|||
text*[test3Z::Z, z=3]\<open>lorem ipsum...\<close>
|
||||
|
||||
text\<open>We want to get all the instances of the @{doc_class Z}:\<close>
|
||||
value*\<open>@{Z-instances}\<close>
|
||||
value*\<open>@{Z_instances}\<close>
|
||||
|
||||
text\<open>Now we want to get the instances of the @{doc_class Z} whose attribute z > 2:\<close>
|
||||
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances}\<close>
|
||||
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z_instances}\<close>
|
||||
|
||||
text\<open>We can check that we have the list of instances we wanted:\<close>
|
||||
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
|
||||
\<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z-instances} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
|
||||
value*\<open>filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z_instances} = [@{Z \<open>test3Z\<close>}, @{Z \<open>test2Z\<close>}]
|
||||
\<or> filter (\<lambda>\<sigma>. Z.z \<sigma> > 2) @{Z_instances} = [@{Z \<open>test2Z\<close>}, @{Z \<open>test3Z\<close>}]\<close>
|
||||
|
||||
text\<open>Now, we want to get all the instances of the @{doc_class A}\<close>
|
||||
value*\<open>@{A-instances}\<close>
|
||||
value*\<open>@{A_instances}\<close>
|
||||
|
||||
(*<*)
|
||||
text\<open>Warning: If you make a request on attributes that are undefined in some instances,
|
||||
|
|
@ -166,7 +166,7 @@ But we have defined an instance @{docitem \<open>sdf\<close>} in theory @{theory
|
|||
whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
|
||||
So in the request result we get an unresolved case because the evaluator can not get
|
||||
the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>sdf\<close>}:\<close>
|
||||
value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
|
||||
value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A_instances}\<close>
|
||||
(*>*)
|
||||
section\<open>Limitations\<close>
|
||||
|
||||
|
|
@ -201,12 +201,12 @@ Consequently, it has the same limitations as \<^emph>\<open>value*\<close>.
|
|||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
|
||||
we can check logical statements:\<close>
|
||||
|
||||
term*\<open>authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept-High-Level-Invariants.introduction \<open>introduction4\<close>})\<close>
|
||||
term*\<open>authored_by @{Concept_High_Level_Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept_High_Level_Invariants.introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{Concept_High_Level_Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept_High_Level_Invariants.introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{Concept_High_Level_Invariants.introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Concept_High_Level_Invariants.introduction \<open>introduction4\<close>})\<close>
|
||||
|
||||
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
||||
(* Error:
|
||||
|
|
@ -226,7 +226,7 @@ text\<open>... and here we reference @{A \<open>assertionA\<close>}.\<close>
|
|||
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>
|
||||
value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
|
||||
value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A_instances}\<close>
|
||||
|
||||
assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
|
||||
\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
|
|
|
|||
|
|
@ -0,0 +1,463 @@
|
|||
(* 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
|
|
@ -1132,13 +1132,10 @@ fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option _ =
|
|||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
|
||||
(* Convert excluded mixfix symbols.
|
||||
Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
|
||||
we can not use "_" or "'" for classes names in term antiquotation.
|
||||
We chose to convert the excluded characters to "-". *)
|
||||
val clean_string = translate_string
|
||||
(fn "_" => "-"
|
||||
| "'" => "-"
|
||||
(* Convert some excluded mixfix symbols that can appear in an inner syntax name. *)
|
||||
val clean_mixfix = translate_string
|
||||
(fn "_" => "'_"
|
||||
| "'" => "''"
|
||||
| c => c);
|
||||
|
||||
fun rm_mixfix name mixfix thy =
|
||||
|
|
@ -1177,8 +1174,8 @@ fun declare_ISA_class_accessor_and_check_instance (doc_class_name, bind_pos) thy
|
|||
|> pair bind_pos |> swap |> Binding.make
|
||||
val const_typ = \<^typ>\<open>string\<close> --> Syntax.read_typ (Proof_Context.init_global thy) doc_class_name
|
||||
fun mixfix_enclose name = name |> enclose "@{" " _}"
|
||||
val mixfix = clean_string bname |> mixfix_enclose
|
||||
val mixfix' = clean_string doc_class_name |> mixfix_enclose
|
||||
val mixfix = clean_mixfix bname |> mixfix_enclose
|
||||
val mixfix' = clean_mixfix doc_class_name |> mixfix_enclose
|
||||
in
|
||||
thy |> rm_mixfix bname' mixfix
|
||||
|> Sign.add_consts [(bind, const_typ, Mixfix.mixfix mixfix)]
|
||||
|
|
@ -1216,8 +1213,8 @@ fun declare_class_instances_annotation (doc_class_name, bind_pos) thy =
|
|||
|> suffix instances_of_suffixN |> pair bind_pos |> swap |> Binding.make
|
||||
val class_typ = doc_class_name |> Proof_Context.read_typ (Proof_Context.init_global thy)
|
||||
fun mixfix_enclose name = name |> enclose "@{" "}"
|
||||
val mixfix = clean_string (bname ^ instances_of_suffixN) |> mixfix_enclose
|
||||
val mixfix' = clean_string (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose
|
||||
val mixfix = clean_mixfix (bname ^ instances_of_suffixN) |> mixfix_enclose
|
||||
val mixfix' = clean_mixfix (doc_class_name ^ instances_of_suffixN) |> mixfix_enclose
|
||||
in
|
||||
thy |> rm_mixfix bname' mixfix
|
||||
|> Sign.add_consts [(bind, \<^Type>\<open>list class_typ\<close>, Mixfix.mixfix mixfix)]
|
||||
|
|
|
|||
|
|
@ -451,7 +451,7 @@ text*[cc_assumption_test_ref::cc_assumption_test]\<open>\<close>
|
|||
|
||||
definition tag_l :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where "tag_l \<equiv> \<lambda>x y. y"
|
||||
|
||||
lemma* tagged : "tag_l @{cc-assumption-test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
lemma* tagged : "tag_l @{cc_assumption_test \<open>cc_assumption_test_ref\<close>} AA \<Longrightarrow> AA"
|
||||
by (simp add: tag_l_def)
|
||||
|
||||
find_theorems name:tagged "(_::cc_assumption_test \<Rightarrow> _ \<Rightarrow> _) _ _ \<Longrightarrow>_"
|
||||
|
|
@ -463,7 +463,7 @@ b::int
|
|||
|
||||
text*[b::B'_test']\<open>\<close>
|
||||
|
||||
term*\<open>@{B--test- \<open>b\<close>}\<close>
|
||||
term*\<open>@{B'_test' \<open>b\<close>}\<close>
|
||||
|
||||
declare_reference*["text-elements-expls"::technical]
|
||||
(*>*)
|
||||
|
|
@ -484,19 +484,6 @@ text\<open>
|
|||
\<close>
|
||||
|
||||
For a declared class \<^theory_text>\<open>cid\<close>, there exists a term-antiquotation of the form \<^theory_text>\<open>@{cid \<open>oid\<close>}\<close>.
|
||||
Due to implementation of term-antiquotation using mixfix annotation
|
||||
(see @{cite "wenzel:isabelle-isar:2020"}),
|
||||
should a class \<open>cid\<close> contains an underscore or a single quote,
|
||||
they will be converted to hyphens in the term-antiquotation.
|
||||
For example:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>doc_class B'_test' =
|
||||
b::int
|
||||
|
||||
text*[b::B'_test']\<open>\<close>
|
||||
|
||||
term*\<open>@{B--test- \<open>b\<close>}\<close>\<close>}
|
||||
|
||||
The major commands providing term-contexts are\<^footnote>\<open>The meta-argument list is optional.\<close>
|
||||
\<^item> \<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
|
||||
\<^item> \<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>, and
|
||||
|
|
@ -561,7 +548,7 @@ lemma* tagged : "tag_l @{cc-assumption-test \<open>cc_assumption_test_ref\<close
|
|||
find_theorems name:tagged "(_::cc_assumption_test \<Rightarrow> _ \<Rightarrow> _) _ _ \<Longrightarrow>_"\<close>}
|
||||
|
||||
In this example, the definition \<^const>\<open>tag_l\<close> adds a tag to the \<open>tagged\<close> lemma using
|
||||
the term-antiquotation @{term_ [source] \<open>@{cc-assumption-test \<open>cc_assumption_test_ref\<close>}\<close>}
|
||||
the term-antiquotation @{term_ [source] \<open>@{cc_assumption_test \<open>cc_assumption_test_ref\<close>}\<close>}
|
||||
inside the \<open>prop\<close> declaration.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
|
|
|
|||
Loading…
Reference in New Issue