author | haftmann |
Thu, 29 Oct 2009 11:41:36 +0100 | |
changeset 33318 | ddd97d9dfbfb |
parent 32799 | 7478ea535416 |
child 33595 | 7264824baf66 |
permissions | -rw-r--r-- |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Record.thy |
32763 | 2 |
Author: Wolfgang Naraschewski, TU Muenchen |
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
Author: Norbert Schirmer, TU Muenchen |
|
5 |
Author: Thomas Sewell, NICTA |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
6 |
*) |
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
7 |
|
22817 | 8 |
header {* Extensible records with structural subtyping *} |
9 |
||
15131 | 10 |
theory Record |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
11 |
imports Product_Type |
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
12 |
uses ("Tools/record.ML") |
15131 | 13 |
begin |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
14 |
|
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
15 |
lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s" |
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14080
diff
changeset
|
16 |
by simp |
11826 | 17 |
|
25705 | 18 |
lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)" |
19 |
by (simp add: comp_def) |
|
11821 | 20 |
|
32743
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
21 |
lemma o_eq_dest_lhs: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
22 |
"a o b = c \<Longrightarrow> a (b v) = c v" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
23 |
by clarsimp |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
24 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
25 |
lemma id_o_refl: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
26 |
"id o f = f o id" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
27 |
by simp |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
28 |
|
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
29 |
lemma o_eq_id_dest: |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
30 |
"a o b = id o c \<Longrightarrow> a (b v) = c v" |
c4e9a48bc50e
Initial attempt at porting record update to repository Isabelle.
tsewell@rubicon.NSW.bigpond.net.au
parents:
31723
diff
changeset
|
31 |
by clarsimp |
22817 | 32 |
|
11833 | 33 |
subsection {* Concrete record syntax *} |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
34 |
|
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
35 |
nonterminals |
5198 | 36 |
ident field_type field_types field fields update updates |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
37 |
syntax |
11821 | 38 |
"_constify" :: "id => ident" ("_") |
39 |
"_constify" :: "longid => ident" ("_") |
|
5198 | 40 |
|
11821 | 41 |
"_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)") |
42 |
"" :: "field_type => field_types" ("_") |
|
43 |
"_field_types" :: "[field_type, field_types] => field_types" ("_,/ _") |
|
44 |
"_record_type" :: "field_types => type" ("(3'(| _ |'))") |
|
10093 | 45 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3'(| _,/ (2... ::/ _) |'))") |
5198 | 46 |
|
11821 | 47 |
"_field" :: "[ident, 'a] => field" ("(2_ =/ _)") |
48 |
"" :: "field => fields" ("_") |
|
49 |
"_fields" :: "[field, fields] => fields" ("_,/ _") |
|
50 |
"_record" :: "fields => 'a" ("(3'(| _ |'))") |
|
10093 | 51 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3'(| _,/ (2... =/ _) |'))") |
5198 | 52 |
|
10641 | 53 |
"_update_name" :: idt |
11821 | 54 |
"_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
55 |
"" :: "update => updates" ("_") |
|
56 |
"_updates" :: "[update, updates] => updates" ("_,/ _") |
|
10093 | 57 |
"_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
58 |
|
10331 | 59 |
syntax (xsymbols) |
11821 | 60 |
"_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
10093 | 61 |
"_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
62 |
"_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
|
63 |
"_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
|
64 |
"_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
|
9729 | 65 |
|
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
66 |
subsection {* Operators and lemmas for types isomorphic to tuples *} |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
67 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
68 |
text {* |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
69 |
Records are isomorphic to compound tuple types. To implement efficient |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
70 |
records, we make this isomorphism explicit. Consider the record |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
71 |
access/update simplification @{text "alpha (beta_update f rec) = alpha rec"} for |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
72 |
distinct fields alpha and beta of some record rec with n fields. There |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
73 |
are @{text "n ^ 2"} such theorems, which prohibits storage of all of them for |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
74 |
large n. The rules can be proved on the fly by case decomposition and |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
75 |
simplification in O(n) time. By creating O(n) isomorphic-tuple types |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
76 |
while defining the record, however, we can prove the access/update |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
77 |
simplification in @{text "O(log(n)^2)"} time. |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
78 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
79 |
The O(n) cost of case decomposition is not because O(n) steps are taken, |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
80 |
but rather because the resulting rule must contain O(n) new variables and |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
81 |
an O(n) size concrete record construction. To sidestep this cost, we would |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
82 |
like to avoid case decomposition in proving access/update theorems. |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
83 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
84 |
Record types are defined as isomorphic to tuple types. For instance, a |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
85 |
record type with fields 'a, 'b, 'c and 'd might be introduced as |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
86 |
isomorphic to @{text "'a \<times> ('b \<times> ('c \<times> 'd))"}. If we balance the tuple tree to |
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
87 |
@{text "('a \<times> 'b) \<times> ('c \<times> 'd)"} then accessors can be defined by converting to |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
88 |
the underlying type then using O(log(n)) fst or snd operations. |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
89 |
Updators can be defined similarly, if we introduce a @{text "fst_update"} and |
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
90 |
@{text "snd_update"} function. Furthermore, we can prove the access/update |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
91 |
theorem in O(log(n)) steps by using simple rewrites on fst, snd, |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
92 |
@{text "fst_update"} and @{text "snd_update"}. |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
93 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
94 |
The catch is that, although O(log(n)) steps were taken, the underlying |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
95 |
type we converted to is a tuple tree of size O(n). Processing this term |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
96 |
type wastes performance. We avoid this for large n by taking each |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
97 |
subtree of size K and defining a new type isomorphic to that tuple |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
98 |
subtree. A record can now be defined as isomorphic to a tuple tree |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
99 |
of these O(n/K) new types, or, if @{text "n > K*K"}, we can repeat the process, |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
100 |
until the record can be defined in terms of a tuple tree of complexity |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
101 |
less than the constant K. |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
102 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
103 |
If we prove the access/update theorem on this type with the analagous |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
104 |
steps to the tuple tree, we consume @{text "O(log(n)^2)"} time as the intermediate |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
105 |
terms are O(log(n)) in size and the types needed have size bounded by K. |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
106 |
To enable this analagous traversal, we define the functions seen below: |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
107 |
@{text "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"} |
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
108 |
and @{text "istuple_snd_update"}. These functions generalise tuple |
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
109 |
operations by taking a parameter that encapsulates a tuple isomorphism. |
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
110 |
The rewrites needed on these functions now need an additional assumption |
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
111 |
which is that the isomorphism works. |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
112 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
113 |
These rewrites are typically used in a structured way. They are here |
32756
fb32a99a7689
Fix unescaped expressions breaking latex output in Record.thy
Thomas Sewell <tsewell@nicta.com.au>
parents:
32752
diff
changeset
|
114 |
presented as the introduction rule @{text "isomorphic_tuple.intros"} rather than |
32752
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
115 |
as a rewrite rule set. The introduction form is an optimisation, as net |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
116 |
matching can be performed at one term location for each step rather than |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
117 |
the simplifier searching the term for possible pattern matches. The rule |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
118 |
set is used as it is viewed outside the locale, with the locale assumption |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
119 |
(that the isomorphism is valid) left as a rule assumption. All rules are |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
120 |
structured to aid net matching, using either a point-free form or an |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
121 |
encapsulating predicate. |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
122 |
*} |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
123 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
124 |
typedef ('a, 'b, 'c) tuple_isomorphism |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
125 |
= "UNIV :: (('a \<Rightarrow> ('b \<times> 'c)) \<times> (('b \<times> 'c) \<Rightarrow> 'a)) set" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
126 |
by simp |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
127 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
128 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
129 |
"TupleIsomorphism repr abst = Abs_tuple_isomorphism (repr, abst)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
130 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
131 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
132 |
istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
133 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
134 |
"istuple_fst isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in fst \<circ> repr" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
135 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
136 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
137 |
istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'c" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
138 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
139 |
"istuple_snd isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in snd \<circ> repr" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
140 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
141 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
142 |
istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
143 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
144 |
"istuple_fst_update isom \<equiv> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
145 |
let (repr, abst) = Rep_tuple_isomorphism isom in |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
146 |
(\<lambda>f v. abst (f (fst (repr v)), snd (repr v)))" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
147 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
148 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
149 |
istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> ('c \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'a)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
150 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
151 |
"istuple_snd_update isom \<equiv> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
152 |
let (repr, abst) = Rep_tuple_isomorphism isom in |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
153 |
(\<lambda>f v. abst (fst (repr v), f (snd (repr v))))" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
154 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
155 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
156 |
istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'a" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
157 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
158 |
"istuple_cons isom \<equiv> let (repr, abst) = Rep_tuple_isomorphism isom in curry abst" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
159 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
160 |
text {* |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
161 |
These predicates are used in the introduction rule set to constrain |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
162 |
matching appropriately. The elimination rules for them produce the |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
163 |
desired theorems once they are proven. The final introduction rules are |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
164 |
used when no further rules from the introduction rule set can apply. |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
165 |
*} |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
166 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
167 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
168 |
istuple_surjective_proof_assist :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
169 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
170 |
"istuple_surjective_proof_assist x y f \<equiv> (f x = y)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
171 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
172 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
173 |
istuple_update_accessor_cong_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
174 |
\<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
175 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
176 |
"istuple_update_accessor_cong_assist upd acc |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
177 |
\<equiv> (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
178 |
\<and> (\<forall>v. upd id v = v)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
179 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
180 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
181 |
istuple_update_accessor_eq_assist :: "(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
182 |
\<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
183 |
where |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
184 |
"istuple_update_accessor_eq_assist upd acc v f v' x |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
185 |
\<equiv> upd f v = v' \<and> acc v = x |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
186 |
\<and> istuple_update_accessor_cong_assist upd acc" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
187 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
188 |
lemma update_accessor_congruence_foldE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
189 |
assumes uac: "istuple_update_accessor_cong_assist upd acc" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
190 |
and r: "r = r'" and v: "acc r' = v'" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
191 |
and f: "\<And>v. v' = v \<Longrightarrow> f v = f' v" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
192 |
shows "upd f r = upd f' r'" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
193 |
using uac r v[symmetric] |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
194 |
apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'") |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
195 |
apply (simp add: istuple_update_accessor_cong_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
196 |
apply (simp add: f) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
197 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
198 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
199 |
lemma update_accessor_congruence_unfoldE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
200 |
"\<lbrakk> istuple_update_accessor_cong_assist upd acc; |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
201 |
r = r'; acc r' = v'; \<And>v. v = v' \<Longrightarrow> f v = f' v \<rbrakk> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
202 |
\<Longrightarrow> upd f r = upd f' r'" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
203 |
apply (erule(2) update_accessor_congruence_foldE) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
204 |
apply simp |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
205 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
206 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
207 |
lemma istuple_update_accessor_cong_assist_id: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
208 |
"istuple_update_accessor_cong_assist upd acc \<Longrightarrow> upd id = id" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
209 |
by (rule ext, simp add: istuple_update_accessor_cong_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
210 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
211 |
lemma update_accessor_noopE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
212 |
assumes uac: "istuple_update_accessor_cong_assist upd acc" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
213 |
and acc: "f (acc x) = acc x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
214 |
shows "upd f x = x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
215 |
using uac |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
216 |
by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def] |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
217 |
cong: update_accessor_congruence_unfoldE[OF uac]) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
218 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
219 |
lemma update_accessor_noop_compE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
220 |
assumes uac: "istuple_update_accessor_cong_assist upd acc" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
221 |
assumes acc: "f (acc x) = acc x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
222 |
shows "upd (g \<circ> f) x = upd g x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
223 |
by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
224 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
225 |
lemma update_accessor_cong_assist_idI: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
226 |
"istuple_update_accessor_cong_assist id id" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
227 |
by (simp add: istuple_update_accessor_cong_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
228 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
229 |
lemma update_accessor_cong_assist_triv: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
230 |
"istuple_update_accessor_cong_assist upd acc |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
231 |
\<Longrightarrow> istuple_update_accessor_cong_assist upd acc" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
232 |
by assumption |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
233 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
234 |
lemma update_accessor_accessor_eqE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
235 |
"\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> acc v = x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
236 |
by (simp add: istuple_update_accessor_eq_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
237 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
238 |
lemma update_accessor_updator_eqE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
239 |
"\<lbrakk> istuple_update_accessor_eq_assist upd acc v f v' x \<rbrakk> \<Longrightarrow> upd f v = v'" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
240 |
by (simp add: istuple_update_accessor_eq_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
241 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
242 |
lemma istuple_update_accessor_eq_assist_idI: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
243 |
"v' = f v \<Longrightarrow> istuple_update_accessor_eq_assist id id v f v' v" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
244 |
by (simp add: istuple_update_accessor_eq_assist_def |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
245 |
update_accessor_cong_assist_idI) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
246 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
247 |
lemma istuple_update_accessor_eq_assist_triv: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
248 |
"istuple_update_accessor_eq_assist upd acc v f v' x |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
249 |
\<Longrightarrow> istuple_update_accessor_eq_assist upd acc v f v' x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
250 |
by assumption |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
251 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
252 |
lemma istuple_update_accessor_cong_from_eq: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
253 |
"istuple_update_accessor_eq_assist upd acc v f v' x |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
254 |
\<Longrightarrow> istuple_update_accessor_cong_assist upd acc" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
255 |
by (simp add: istuple_update_accessor_eq_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
256 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
257 |
lemma o_eq_dest: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
258 |
"a o b = c o d \<Longrightarrow> a (b v) = c (d v)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
259 |
apply (clarsimp simp: o_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
260 |
apply (erule fun_cong) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
261 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
262 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
263 |
lemma o_eq_elim: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
264 |
"\<lbrakk> a o b = c o d; \<lbrakk> \<And>v. a (b v) = c (d v) \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
265 |
apply (erule meta_mp) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
266 |
apply (erule o_eq_dest) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
267 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
268 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
269 |
lemma istuple_surjective_proof_assistI: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
270 |
"f x = y \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
271 |
istuple_surjective_proof_assist x y f" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
272 |
by (simp add: istuple_surjective_proof_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
273 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
274 |
lemma istuple_surjective_proof_assist_idE: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
275 |
"istuple_surjective_proof_assist x y id \<Longrightarrow> x = y" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
276 |
by (simp add: istuple_surjective_proof_assist_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
277 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
278 |
locale isomorphic_tuple = |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
279 |
fixes isom :: "('a, 'b, 'c) tuple_isomorphism" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
280 |
and repr and abst |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
281 |
defines "repr \<equiv> fst (Rep_tuple_isomorphism isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
282 |
defines "abst \<equiv> snd (Rep_tuple_isomorphism isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
283 |
assumes repr_inv: "\<And>x. abst (repr x) = x" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
284 |
assumes abst_inv: "\<And>y. repr (abst y) = y" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
285 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
286 |
begin |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
287 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
288 |
lemma repr_inj: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
289 |
"(repr x = repr y) = (x = y)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
290 |
apply (rule iffI, simp_all) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
291 |
apply (drule_tac f=abst in arg_cong, simp add: repr_inv) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
292 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
293 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
294 |
lemma abst_inj: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
295 |
"(abst x = abst y) = (x = y)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
296 |
apply (rule iffI, simp_all) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
297 |
apply (drule_tac f=repr in arg_cong, simp add: abst_inv) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
298 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
299 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
300 |
lemma split_Rep: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
301 |
"split f (Rep_tuple_isomorphism isom) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
302 |
= f repr abst" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
303 |
by (simp add: split_def repr_def abst_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
304 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
305 |
lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
306 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
307 |
lemma istuple_access_update_fst_fst: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
308 |
"\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
309 |
(f o istuple_fst isom) o (istuple_fst_update isom o h) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
310 |
= j o (f o istuple_fst isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
311 |
by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
312 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
313 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
314 |
lemma istuple_access_update_snd_snd: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
315 |
"\<lbrakk> f o h g = j o f \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
316 |
(f o istuple_snd isom) o (istuple_snd_update isom o h) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
317 |
= j o (f o istuple_snd isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
318 |
by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
319 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
320 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
321 |
lemma istuple_access_update_fst_snd: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
322 |
"(f o istuple_fst isom) o (istuple_snd_update isom o h) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
323 |
= id o (f o istuple_fst isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
324 |
by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
325 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
326 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
327 |
lemma istuple_access_update_snd_fst: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
328 |
"(f o istuple_snd isom) o (istuple_fst_update isom o h) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
329 |
= id o (f o istuple_snd isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
330 |
by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
331 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
332 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
333 |
lemma istuple_update_swap_fst_fst: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
334 |
"\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
335 |
(istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
336 |
= (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
337 |
by (clarsimp simp: istuple_fst_update_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
338 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
339 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
340 |
lemma istuple_update_swap_snd_snd: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
341 |
"\<lbrakk> h f o j g = j g o h f \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
342 |
(istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
343 |
= (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
344 |
by (clarsimp simp: istuple_snd_update_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
345 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
346 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
347 |
lemma istuple_update_swap_fst_snd: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
348 |
"(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
349 |
= (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
350 |
by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
351 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
352 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
353 |
lemma istuple_update_swap_snd_fst: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
354 |
"(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
355 |
= (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
356 |
by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
357 |
intro!: ext elim!: o_eq_elim) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
358 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
359 |
lemma istuple_update_compose_fst_fst: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
360 |
"\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
361 |
(istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
362 |
= (istuple_fst_update isom o k) (f o g)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
363 |
by (fastsimp simp: istuple_fst_update_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
364 |
intro!: ext elim!: o_eq_elim dest: fun_cong) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
365 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
366 |
lemma istuple_update_compose_snd_snd: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
367 |
"\<lbrakk> h f o j g = k (f o g) \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
368 |
(istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
369 |
= (istuple_snd_update isom o k) (f o g)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
370 |
by (fastsimp simp: istuple_snd_update_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
371 |
intro!: ext elim!: o_eq_elim dest: fun_cong) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
372 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
373 |
lemma istuple_surjective_proof_assist_step: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
374 |
"\<lbrakk> istuple_surjective_proof_assist v a (istuple_fst isom o f); |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
375 |
istuple_surjective_proof_assist v b (istuple_snd isom o f) \<rbrakk> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
376 |
\<Longrightarrow> istuple_surjective_proof_assist v (istuple_cons isom a b) f" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
377 |
by (clarsimp simp: istuple_surjective_proof_assist_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
378 |
istuple_fst_def istuple_snd_def istuple_cons_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
379 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
380 |
lemma istuple_fst_update_accessor_cong_assist: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
381 |
"istuple_update_accessor_cong_assist f g \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
382 |
istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
383 |
by (clarsimp simp: istuple_update_accessor_cong_assist_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
384 |
istuple_fst_update_def istuple_fst_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
385 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
386 |
lemma istuple_snd_update_accessor_cong_assist: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
387 |
"istuple_update_accessor_cong_assist f g \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
388 |
istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
389 |
by (clarsimp simp: istuple_update_accessor_cong_assist_def simps |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
390 |
istuple_snd_update_def istuple_snd_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
391 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
392 |
lemma istuple_fst_update_accessor_eq_assist: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
393 |
"istuple_update_accessor_eq_assist f g a u a' v \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
394 |
istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
395 |
(istuple_cons isom a b) u (istuple_cons isom a' b) v" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
396 |
by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
397 |
istuple_update_accessor_cong_assist_def istuple_cons_def simps) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
398 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
399 |
lemma istuple_snd_update_accessor_eq_assist: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
400 |
"istuple_update_accessor_eq_assist f g b u b' v \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
401 |
istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
402 |
(istuple_cons isom a b) u (istuple_cons isom a b') v" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
403 |
by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
404 |
istuple_update_accessor_cong_assist_def istuple_cons_def simps) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
405 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
406 |
lemma istuple_cons_conj_eqI: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
407 |
"\<lbrakk> (a = c \<and> b = d \<and> P) = Q \<rbrakk> \<Longrightarrow> |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
408 |
(istuple_cons isom a b = istuple_cons isom c d \<and> P) = Q" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
409 |
by (clarsimp simp: istuple_cons_def simps) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
410 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
411 |
lemmas intros = |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
412 |
istuple_access_update_fst_fst |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
413 |
istuple_access_update_snd_snd |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
414 |
istuple_access_update_fst_snd |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
415 |
istuple_access_update_snd_fst |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
416 |
istuple_update_swap_fst_fst |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
417 |
istuple_update_swap_snd_snd |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
418 |
istuple_update_swap_fst_snd |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
419 |
istuple_update_swap_snd_fst |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
420 |
istuple_update_compose_fst_fst |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
421 |
istuple_update_compose_snd_snd |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
422 |
istuple_surjective_proof_assist_step |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
423 |
istuple_fst_update_accessor_eq_assist |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
424 |
istuple_snd_update_accessor_eq_assist |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
425 |
istuple_fst_update_accessor_cong_assist |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
426 |
istuple_snd_update_accessor_cong_assist |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
427 |
istuple_cons_conj_eqI |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
428 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
429 |
end |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
430 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
431 |
lemma isomorphic_tuple_intro: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
432 |
assumes repr_inj: "\<And>x y. (repr x = repr y) = (x = y)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
433 |
and abst_inv: "\<And>z. repr (abst z) = z" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
434 |
shows "v \<equiv> TupleIsomorphism repr abst \<Longrightarrow> isomorphic_tuple v" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
435 |
apply (rule isomorphic_tuple.intro, |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
436 |
simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
437 |
tuple_isomorphism_def abst_inv) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
438 |
apply (cut_tac x="abst (repr x)" and y="x" in repr_inj) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
439 |
apply (simp add: abst_inv) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
440 |
done |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
441 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
442 |
definition |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
443 |
"tuple_istuple \<equiv> TupleIsomorphism id id" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
444 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
445 |
lemma tuple_istuple: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
446 |
"isomorphic_tuple tuple_istuple" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
447 |
by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def) |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
448 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
449 |
lemma refl_conj_eq: |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
450 |
"Q = R \<Longrightarrow> (P \<and> Q) = (P \<and> R)" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
451 |
by simp |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
452 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
453 |
lemma istuple_UNIV_I: "\<And>x. x\<in>UNIV \<equiv> True" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
454 |
by simp |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
455 |
|
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
456 |
lemma istuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
457 |
by simp |
f65d74a264dd
Initial response to feedback from Norbert, Makarius on record patch
tsewell@rubicon.NSW.bigpond.net.au
parents:
32745
diff
changeset
|
458 |
|
32744
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
459 |
use "Tools/record.ML" |
50406c4951d9
Record patch imported and working.
Thomas Sewell <tsewell@nicta.com.au>
parents:
32743
diff
changeset
|
460 |
setup Record.setup |
10641 | 461 |
|
4870
cc36acb5b114
Extensible records with structural subtyping in HOL. See
wenzelm
parents:
diff
changeset
|
462 |
end |