--- a/Nominal/Nominal2_Base.thy Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/Nominal2_Base.thy Sat Mar 19 21:06:48 2016 +0000
@@ -13,6 +13,9 @@
"atom_decl" "equivariance" :: thy_decl
begin
+declare [[typedef_overloaded]]
+
+
section {* Atoms and Sorts *}
text {* A simple implementation for atom_sorts is strings. *}
@@ -183,7 +186,7 @@
by (simp add: Abs_perm_inverse perm_inv Rep_perm)
instance
-apply default
+apply standard
unfolding Rep_perm_inject [symmetric]
unfolding minus_perm_def
unfolding Rep_perm_add
@@ -325,7 +328,7 @@
"p \<bullet> a = (Rep_perm p) a"
instance
-apply(default)
+apply standard
apply(simp_all add: permute_atom_def Rep_perm_simps)
done
@@ -363,7 +366,7 @@
"p \<bullet> q = p + q - p"
instance
-apply default
+apply standard
apply (simp add: permute_perm_def)
apply (simp add: permute_perm_def algebra_simps)
done
@@ -390,7 +393,7 @@
"p \<bullet> f = (\<lambda>x. p \<bullet> (f (- p \<bullet> x)))"
instance
-apply default
+apply standard
apply (simp add: permute_fun_def)
apply (simp add: permute_fun_def minus_add)
done
@@ -413,7 +416,7 @@
definition "p \<bullet> (b::bool) = b"
instance
-apply(default)
+apply standard
apply(simp_all add: permute_bool_def)
done
@@ -438,7 +441,7 @@
"p \<bullet> X = {p \<bullet> x | x. x \<in> X}"
instance
-apply default
+apply standard
apply (auto simp: permute_set_def)
done
@@ -510,7 +513,7 @@
definition "p \<bullet> (u::unit) = u"
instance
-by (default) (simp_all add: permute_unit_def)
+ by standard (simp_all add: permute_unit_def)
end
@@ -526,7 +529,7 @@
Pair_eqvt: "p \<bullet> (x, y) = (p \<bullet> x, p \<bullet> y)"
instance
-by default auto
+ by standard auto
end
@@ -542,7 +545,7 @@
| Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
instance
-by (default) (case_tac [!] x, simp_all)
+ by standard (case_tac [!] x, simp_all)
end
@@ -558,7 +561,7 @@
| Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
instance
-by (default) (induct_tac [!] x, simp_all)
+ by standard (induct_tac [!] x, simp_all)
end
@@ -580,7 +583,7 @@
| Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
instance
-by (default) (induct_tac [!] x, simp_all)
+ by standard (induct_tac [!] x, simp_all)
end
@@ -667,7 +670,7 @@
done
instance
-apply(default)
+apply standard
apply(transfer)
apply(simp)
apply(transfer)
@@ -685,7 +688,7 @@
definition "p \<bullet> (c::char) = c"
instance
-by (default) (simp_all add: permute_char_def)
+ by standard (simp_all add: permute_char_def)
end
@@ -695,7 +698,7 @@
definition "p \<bullet> (n::nat) = n"
instance
-by (default) (simp_all add: permute_nat_def)
+ by standard (simp_all add: permute_nat_def)
end
@@ -705,7 +708,7 @@
definition "p \<bullet> (i::int) = i"
instance
-by (default) (simp_all add: permute_int_def)
+ by standard (simp_all add: permute_int_def)
end
@@ -729,22 +732,22 @@
text {* Other type constructors preserve purity. *}
instance "fun" :: (pure, pure) pure
-by default (simp add: permute_fun_def permute_pure)
+ by standard (simp add: permute_fun_def permute_pure)
instance set :: (pure) pure
-by default (simp add: permute_set_def permute_pure)
+ by standard (simp add: permute_set_def permute_pure)
instance prod :: (pure, pure) pure
-by default (induct_tac x, simp add: permute_pure)
+ by standard (induct_tac x, simp add: permute_pure)
instance sum :: (pure, pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+ by standard (induct_tac x, simp_all add: permute_pure)
instance list :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+ by standard (induct_tac x, simp_all add: permute_pure)
instance option :: (pure) pure
-by default (induct_tac x, simp_all add: permute_pure)
+ by standard (induct_tac x, simp_all add: permute_pure)
subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *}
@@ -1069,7 +1072,7 @@
begin
instance
-apply(default)
+apply standard
unfolding le_bool_def
apply(perm_simp)
apply(rule refl)
@@ -1081,7 +1084,7 @@
begin
instance
-apply(default)
+apply standard
unfolding le_fun_def
apply(perm_simp)
apply(rule refl)
@@ -1093,7 +1096,7 @@
begin
instance
-apply(default)
+apply standard
unfolding Inf_bool_def
apply(perm_simp)
apply(rule refl)
@@ -1105,7 +1108,7 @@
begin
instance
-apply(default)
+apply standard
unfolding Inf_fun_def INF_def
apply(perm_simp)
apply(rule refl)
@@ -1145,7 +1148,7 @@
by (cases x) simp
lemma split_eqvt [eqvt]:
- shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
+ shows "p \<bullet> (case_prod P x) = case_prod (p \<bullet> P) (p \<bullet> x)"
unfolding split_def
by simp
@@ -1456,7 +1459,7 @@
unfolding fresh_def by (simp add: pure_supp)
instance pure < fs
-by default (simp add: pure_supp)
+ by standard (simp add: pure_supp)
subsection {* Type @{typ atom} is finitely-supported. *}
@@ -1474,7 +1477,7 @@
unfolding fresh_def supp_atom by simp
instance atom :: fs
-by default (simp add: supp_atom)
+ by standard (simp add: supp_atom)
section {* Type @{typ perm} is finitely-supported. *}
@@ -1623,7 +1626,7 @@
instance perm :: fs
-by default (simp add: supp_perm finite_perm_lemma)
+ by standard (simp add: supp_perm finite_perm_lemma)
@@ -1649,7 +1652,7 @@
by (simp add: fresh_def supp_Unit)
instance prod :: (fs, fs) fs
-apply default
+apply standard
apply (case_tac x)
apply (simp add: supp_Pair finite_supp)
done
@@ -1674,7 +1677,7 @@
by (simp add: fresh_def supp_Inr)
instance sum :: (fs, fs) fs
-apply default
+apply standard
apply (case_tac x)
apply (simp_all add: supp_Inl supp_Inr finite_supp)
done
@@ -1699,7 +1702,7 @@
by (simp add: fresh_def supp_Some)
instance option :: (fs) fs
-apply default
+apply standard
apply (induct_tac x)
apply (simp_all add: supp_None supp_Some finite_supp)
done
@@ -1752,7 +1755,7 @@
(simp_all add: supp_Nil supp_Cons supp_atom)
instance list :: (fs) fs
-apply default
+apply standard
apply (induct_tac x)
apply (simp_all add: supp_Nil supp_Cons finite_supp)
done
@@ -1895,7 +1898,7 @@
val cty_inst =
[SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))]
val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)]
- val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+ val thm = Thm.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
in
SOME(thm RS @{thm Eq_TrueI})
end
@@ -2120,12 +2123,12 @@
subsection {* Type @{typ "'a multiset"} is finitely supported *}
-lemma set_of_eqvt [eqvt]:
- shows "p \<bullet> (set_of M) = set_of (p \<bullet> M)"
+lemma set_mset_eqvt [eqvt]:
+ shows "p \<bullet> (set_mset M) = set_mset (p \<bullet> M)"
by (induct M) (simp_all add: insert_eqvt empty_eqvt)
-lemma supp_set_of:
- shows "supp (set_of M) \<subseteq> supp M"
+lemma supp_set_mset:
+ shows "supp (set_mset M) \<subseteq> supp M"
apply (rule supp_fun_app_eqvt)
unfolding eqvt_def
apply(perm_simp)
@@ -2165,11 +2168,11 @@
fixes M::"('a::fs multiset)"
shows "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M"
proof -
- have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_of M})" by simp
- also have "... \<subseteq> (\<Union>x \<in> set_of M. supp x)" by auto
- also have "... = supp (set_of M)"
+ have "(\<Union>{supp x | x. x \<in># M}) = (\<Union>{supp x | x. x \<in> set_mset M})" by simp
+ also have "... \<subseteq> (\<Union>x \<in> set_mset M. supp x)" by auto
+ also have "... = supp (set_mset M)"
by (simp add: supp_of_finite_sets)
- also have " ... \<subseteq> supp M" by (rule supp_set_of)
+ also have " ... \<subseteq> supp M" by (rule supp_set_mset)
finally show "(\<Union>{supp x | x. x \<in># M}) \<subseteq> supp M" .
qed
@@ -2199,9 +2202,7 @@
by simp
instance multiset :: (fs) fs
- apply (default)
- apply (rule multisets_supp_finite)
- done
+ by standard (rule multisets_supp_finite)
subsection {* Type @{typ "'a fset"} is finitely supported *}
@@ -2252,9 +2253,7 @@
by (simp add: supp_union_fset)
instance fset :: (fs) fs
- apply (default)
- apply (rule fset_finite_supp)
- done
+ by standard (rule fset_finite_supp)
subsection {* Type @{typ "('a, 'b) finfun"} is finitely supported *}
@@ -2279,7 +2278,7 @@
by (auto simp: fresh_def supp_Pair)
instance finfun :: (fs, fs) fs
- apply(default)
+ apply standard
apply(induct_tac x rule: finfun_weak_induct)
apply(simp add: supp_finfun_const finite_supp)
apply(rule finite_subset)