1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: Atoms
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
Authors: Brian Huffman, Christian Urban
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
Instantiations of concrete atoms
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
*)
|
2782
|
6 |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
theory Atoms
|
2470
|
8 |
imports Nominal2_Base
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
begin
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
2470
|
11 |
|
|
12 |
|
|
13 |
section {* @{const nat_of} is an example of a function
|
|
14 |
without finite support *}
|
|
15 |
|
|
16 |
|
|
17 |
lemma not_fresh_nat_of:
|
|
18 |
shows "\<not> a \<sharp> nat_of"
|
|
19 |
unfolding fresh_def supp_def
|
|
20 |
proof (clarsimp)
|
|
21 |
assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
|
|
22 |
hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
|
|
23 |
by simp
|
|
24 |
then obtain b where
|
|
25 |
b1: "b \<noteq> a" and
|
|
26 |
b2: "sort_of b = sort_of a" and
|
|
27 |
b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
|
|
28 |
by (rule obtain_atom) auto
|
|
29 |
have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
|
|
30 |
also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
|
|
31 |
also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
|
|
32 |
also have "\<dots> = nat_of b" using b2 by simp
|
|
33 |
finally have "nat_of a = nat_of b" by simp
|
|
34 |
with b2 have "a = b" by (simp add: atom_components_eq_iff)
|
|
35 |
with b1 show "False" by simp
|
|
36 |
qed
|
|
37 |
|
|
38 |
lemma supp_nat_of:
|
|
39 |
shows "supp nat_of = UNIV"
|
|
40 |
using not_fresh_nat_of [unfolded fresh_def] by auto
|
|
41 |
|
|
42 |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
section {* Manual instantiation of class @{text at}. *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
typedef (open) name = "{a. sort_of a = Sort ''name'' []}"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
by (rule exists_eq_simple_sort)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
instantiation name :: at
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
begin
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
definition
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
"p \<bullet> a = Abs_name (p \<bullet> Rep_name a)"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
definition
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
"atom a = Rep_name a"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
instance
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
apply (rule at_class)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
apply (rule type_definition_name)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
apply (rule atom_name_def)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
apply (rule permute_name_def)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
done
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
end
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
lemma sort_of_atom_name:
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
shows "sort_of (atom (a::name)) = Sort ''name'' []"
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
by (simp add: atom_name_def Rep_name[simplified])
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
text {* Custom syntax for concrete atoms of type at *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
term "a:::name"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
text {*
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
a:::name stands for (atom a) with a being of concrete atom
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
type name. The above lemma can therefore also be stated as
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
"sort_of (a:::name) = Sort ''name'' []"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
This does not work for multi-sorted atoms.
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
*}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
|
2744
|
83 |
(* fixme
|
|
84 |
lemma supp_of_finite_name_set:
|
|
85 |
fixes S::"name set"
|
|
86 |
assumes "infinte S" "infinite (UNIV - S)"
|
|
87 |
shows "supp S = UNIV"
|
|
88 |
proof -
|
|
89 |
{ fix a
|
|
90 |
have "a \<in> supp S"
|
|
91 |
proof (cases "a \<in> atom ` S")
|
|
92 |
assume "a \<in> atom ` S"
|
|
93 |
then have "\<forall>b \<in> UNIV - S. (a \<rightleftharpoons> atom b) \<bullet> S \<noteq> S"
|
|
94 |
apply(clarify)
|
|
95 |
|
|
96 |
show "a \<in> supp S"
|
|
97 |
}
|
|
98 |
then show "supp S = UNIV" by auto
|
|
99 |
qed
|
|
100 |
*)
|
|
101 |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
section {* Automatic instantiation of class @{text at}. *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
105 |
atom_decl name2
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
lemma
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
108 |
"sort_of (atom (a::name2)) \<noteq> sort_of (atom (b::name))"
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
by (simp add: sort_of_atom_name)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
text {* example swappings *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
lemma
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
fixes a b::"atom"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
assumes "sort_of a = sort_of b"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
116 |
shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
using assms
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
by simp
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
lemma
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
fixes a b::"name2"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
by simp
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
125 |
section {* An example for multiple-sort atoms *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
126 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
datatype ty =
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
TVar string
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
| Fun ty ty ("_ \<rightarrow> _")
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
primrec
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
sort_of_ty::"ty \<Rightarrow> atom_sort"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
where
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
"sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
| "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
136 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
lemma sort_of_ty_eq_iff:
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
shows "sort_of_ty x = sort_of_ty y \<longleftrightarrow> x = y"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
apply(induct x arbitrary: y)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
140 |
apply(case_tac [!] y)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
apply(simp_all)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
done
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
declare sort_of_ty.simps [simp del]
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
146 |
typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
147 |
by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
148 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
149 |
instantiation var :: at_base
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
begin
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
152 |
definition
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
153 |
"p \<bullet> a = Abs_var (p \<bullet> Rep_var a)"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
154 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
definition
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
"atom a = Rep_var a"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
158 |
instance
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
159 |
apply (rule at_base_class)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
apply (rule type_definition_var)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
161 |
apply (rule atom_var_def)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
162 |
apply (rule permute_var_def)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
163 |
done
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
164 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
165 |
end
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
166 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
167 |
text {* Constructor for variables. *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
168 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
169 |
definition
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
170 |
Var :: "nat \<Rightarrow> ty \<Rightarrow> var"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
where
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
172 |
"Var x t = Abs_var (Atom (sort_of_ty t) x)"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
174 |
lemma Var_eq_iff [simp]:
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
175 |
shows "Var x s = Var y t \<longleftrightarrow> x = y \<and> s = t"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
176 |
unfolding Var_def
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
177 |
by (auto simp add: Abs_var_inject sort_of_ty_eq_iff)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
178 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
lemma sort_of_atom_var [simp]:
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
180 |
"sort_of (atom (Var n ty)) = sort_of_ty ty"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
181 |
unfolding atom_var_def Var_def
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
182 |
by (simp add: Abs_var_inverse)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
183 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
184 |
lemma
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
185 |
assumes "\<alpha> \<noteq> \<beta>"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
186 |
shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
187 |
using assms by simp
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
188 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
189 |
text {* Projecting out the type component of a variable. *}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
190 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
191 |
definition
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
192 |
ty_of :: "var \<Rightarrow> ty"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
193 |
where
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
194 |
"ty_of x = inv sort_of_ty (sort_of (atom x))"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
195 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
196 |
text {*
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
197 |
Functions @{term Var}/@{term ty_of} satisfy many of the same
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
198 |
properties as @{term Atom}/@{term sort_of}.
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
199 |
*}
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
200 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
201 |
lemma ty_of_Var [simp]:
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
202 |
shows "ty_of (Var x t) = t"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
203 |
unfolding ty_of_def
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
204 |
unfolding sort_of_atom_var
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
205 |
apply (rule inv_f_f)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
206 |
apply (simp add: inj_on_def sort_of_ty_eq_iff)
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
207 |
done
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
208 |
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
209 |
lemma ty_of_permute [simp]:
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
210 |
shows "ty_of (p \<bullet> x) = ty_of x"
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
211 |
unfolding ty_of_def
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
212 |
unfolding atom_eqvt [symmetric]
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
213 |
by simp
|
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
214 |
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
216 |
section {* Tests with subtyping and automatic coercions *}
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
|
2597
|
218 |
declare [[coercion_enabled]]
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
219 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
220 |
atom_decl var1
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
221 |
atom_decl var2
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
222 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
223 |
declare [[coercion "atom::var1\<Rightarrow>atom"]]
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
224 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
225 |
declare [[coercion "atom::var2\<Rightarrow>atom"]]
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
226 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
227 |
lemma
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
228 |
fixes a::"var1" and b::"var2"
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
229 |
shows "a \<sharp> t \<and> b \<sharp> t"
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
230 |
oops
|
2782
|
231 |
|
2556
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
232 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
233 |
(* does not yet work: it needs image as
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
coercion map *)
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
235 |
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
lemma
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
fixes as::"var1 set"
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
238 |
shows "atom ` as \<sharp>* t"
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
239 |
oops
|
8ed62410236e
added a test about subtyping; disabled two tests, because of problem with function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
240 |
|
1772
48c2eb84d5ce
merged pearl paper with this repository; started litrature subdirectory
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
241 |
end
|