supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)
(* Title: Atoms+ −
Authors: Brian Huffman, Christian Urban+ −
+ −
Instantiations of concrete atoms + −
*)+ −
theory Atoms+ −
imports Nominal2_Base+ −
begin+ −
+ −
+ −
+ −
section {* @{const nat_of} is an example of a function + −
without finite support *}+ −
+ −
+ −
lemma not_fresh_nat_of:+ −
shows "\<not> a \<sharp> nat_of"+ −
unfolding fresh_def supp_def+ −
proof (clarsimp)+ −
assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"+ −
hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"+ −
by simp+ −
then obtain b where+ −
b1: "b \<noteq> a" and+ −
b2: "sort_of b = sort_of a" and+ −
b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"+ −
by (rule obtain_atom) auto+ −
have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)+ −
also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)+ −
also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp+ −
also have "\<dots> = nat_of b" using b2 by simp+ −
finally have "nat_of a = nat_of b" by simp+ −
with b2 have "a = b" by (simp add: atom_components_eq_iff)+ −
with b1 show "False" by simp+ −
qed+ −
+ −
lemma supp_nat_of:+ −
shows "supp nat_of = UNIV"+ −
using not_fresh_nat_of [unfolded fresh_def] by auto+ −
+ −
+ −
section {* Manual instantiation of class @{text at}. *}+ −
+ −
typedef (open) name = "{a. sort_of a = Sort ''name'' []}"+ −
by (rule exists_eq_simple_sort)+ −
+ −
instantiation name :: at+ −
begin+ −
+ −
definition+ −
"p \<bullet> a = Abs_name (p \<bullet> Rep_name a)"+ −
+ −
definition+ −
"atom a = Rep_name a"+ −
+ −
instance+ −
apply (rule at_class)+ −
apply (rule type_definition_name)+ −
apply (rule atom_name_def)+ −
apply (rule permute_name_def)+ −
done+ −
+ −
end+ −
+ −
lemma sort_of_atom_name: + −
shows "sort_of (atom (a::name)) = Sort ''name'' []"+ −
unfolding atom_name_def using Rep_name by simp+ −
+ −
text {* Custom syntax for concrete atoms of type at *}+ −
+ −
term "a:::name"+ −
+ −
text {* + −
a:::name stands for (atom a) with a being of concrete atom + −
type name. The above lemma can therefore also be stated as+ −
+ −
"sort_of (a:::name) = Sort ''name'' []"+ −
+ −
This does not work for multi-sorted atoms.+ −
*}+ −
+ −
+ −
section {* Automatic instantiation of class @{text at}. *}+ −
+ −
atom_decl name2+ −
+ −
lemma sort_of_atom_name2:+ −
"sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []"+ −
unfolding atom_name2_def + −
using Rep_name2 + −
by simp+ −
+ −
text {* example swappings *}+ −
lemma+ −
fixes a b::"atom"+ −
assumes "sort_of a = sort_of b"+ −
shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)"+ −
using assms+ −
by simp+ −
+ −
lemma+ −
fixes a b::"name2"+ −
shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)"+ −
by simp+ −
+ −
section {* An example for multiple-sort atoms *}+ −
+ −
datatype ty =+ −
TVar string+ −
| Fun ty ty ("_ \<rightarrow> _")+ −
+ −
primrec+ −
sort_of_ty::"ty \<Rightarrow> atom_sort"+ −
where+ −
"sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]"+ −
| "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]"+ −
+ −
lemma sort_of_ty_eq_iff:+ −
shows "sort_of_ty x = sort_of_ty y \<longleftrightarrow> x = y"+ −
apply(induct x arbitrary: y)+ −
apply(case_tac [!] y)+ −
apply(simp_all)+ −
done+ −
+ −
declare sort_of_ty.simps [simp del]+ −
+ −
typedef (open) var = "{a. sort_of a \<in> range sort_of_ty}"+ −
by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp)+ −
+ −
instantiation var :: at_base+ −
begin+ −
+ −
definition+ −
"p \<bullet> a = Abs_var (p \<bullet> Rep_var a)"+ −
+ −
definition+ −
"atom a = Rep_var a"+ −
+ −
instance+ −
apply (rule at_base_class)+ −
apply (rule type_definition_var)+ −
apply (rule atom_var_def)+ −
apply (rule permute_var_def)+ −
done+ −
+ −
end+ −
+ −
text {* Constructor for variables. *}+ −
+ −
definition+ −
Var :: "nat \<Rightarrow> ty \<Rightarrow> var"+ −
where+ −
"Var x t = Abs_var (Atom (sort_of_ty t) x)"+ −
+ −
lemma Var_eq_iff [simp]:+ −
shows "Var x s = Var y t \<longleftrightarrow> x = y \<and> s = t"+ −
unfolding Var_def+ −
by (auto simp add: Abs_var_inject sort_of_ty_eq_iff)+ −
+ −
lemma sort_of_atom_var [simp]:+ −
"sort_of (atom (Var n ty)) = sort_of_ty ty"+ −
unfolding atom_var_def Var_def+ −
by (simp add: Abs_var_inverse)+ −
+ −
lemma + −
assumes "\<alpha> \<noteq> \<beta>" + −
shows "(Var x \<alpha> \<leftrightarrow> Var y \<alpha>) \<bullet> (Var x \<alpha>, Var x \<beta>) = (Var y \<alpha>, Var x \<beta>)"+ −
using assms by simp+ −
+ −
text {* Projecting out the type component of a variable. *}+ −
+ −
definition+ −
ty_of :: "var \<Rightarrow> ty"+ −
where+ −
"ty_of x = inv sort_of_ty (sort_of (atom x))"+ −
+ −
text {*+ −
Functions @{term Var}/@{term ty_of} satisfy many of the same+ −
properties as @{term Atom}/@{term sort_of}.+ −
*}+ −
+ −
lemma ty_of_Var [simp]:+ −
shows "ty_of (Var x t) = t"+ −
unfolding ty_of_def+ −
unfolding sort_of_atom_var+ −
apply (rule inv_f_f)+ −
apply (simp add: inj_on_def sort_of_ty_eq_iff)+ −
done+ −
+ −
lemma ty_of_permute [simp]:+ −
shows "ty_of (p \<bullet> x) = ty_of x"+ −
unfolding ty_of_def+ −
unfolding atom_eqvt [symmetric]+ −
by simp+ −
+ −
end+ −