--- a/src/HOL/Nominal/Examples/Pattern.thy Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Sat Sep 03 23:38:06 2011 +0200
@@ -1,7 +1,7 @@
header {* Simply-typed lambda-calculus with let and tuple patterns *}
theory Pattern
-imports Nominal
+imports "../Nominal"
begin
no_syntax
@@ -622,7 +622,7 @@
(auto simp add: Cons_eq_append_conv fresh_star_def
fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
supp_prod fresh_prod supp_atm fresh_atm
- dest: notE [OF iffD1 [OF fresh_def [THEN meta_eq_to_obj_eq]]])
+ dest: notE [OF iffD1 [OF fresh_def]])
lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A"
by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)
--- a/src/HOL/Nominal/Nominal.thy Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/Nominal/Nominal.thy Sat Sep 03 23:38:06 2011 +0200
@@ -32,7 +32,7 @@
(* an auxiliary constant for the decision procedure involving *)
(* permutations (to avoid loops when using perm-compositions) *)
definition
- "perm_aux pi x \<equiv> pi\<bullet>x"
+ "perm_aux pi x = pi\<bullet>x"
(* overloaded permutation operations *)
overloading
@@ -51,61 +51,42 @@
begin
definition
- perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
-
-fun
- perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool"
-where
+ perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
+
+primrec perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
true_eqvt: "perm_bool pi True = True"
| false_eqvt: "perm_bool pi False = False"
-fun
- perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"
-where
+primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where
"perm_unit pi () = ()"
-fun
- perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"
-where
+primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
"perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
-fun
- perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
+primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
nil_eqvt: "perm_list pi [] = []"
| cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
-fun
- perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option"
-where
+primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where
some_eqvt: "perm_option pi (Some x) = Some (pi\<bullet>x)"
| none_eqvt: "perm_option pi None = None"
-definition
- perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char"
-where
- perm_char_def: "perm_char pi c \<equiv> c"
-
-definition
- perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat"
-where
- perm_nat_def: "perm_nat pi i \<equiv> i"
-
-definition
- perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int"
-where
- perm_int_def: "perm_int pi i \<equiv> i"
-
-fun
- perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"
-where
+definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
+ perm_char_def: "perm_char pi c = c"
+
+definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
+ perm_nat_def: "perm_nat pi i = i"
+
+definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
+ perm_int_def: "perm_int pi i = i"
+
+primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
| nnone_eqvt: "perm_noption pi nNone = nNone"
-fun
- perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod"
-where
+primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where
"perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
+
end
@@ -188,18 +169,18 @@
(*==============================*)
definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where
- "pi1 \<triangleq> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
+ "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)"
section {* Support, Freshness and Supports*}
(*========================================*)
definition supp :: "'a \<Rightarrow> ('x set)" where
- "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
+ "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where
- "a \<sharp> x \<equiv> a \<notin> supp x"
+ "a \<sharp> x \<longleftrightarrow> a \<notin> supp x"
definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where
- "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
+ "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))"
(* lemmas about supp *)
lemma supp_fresh_iff:
@@ -1731,7 +1712,7 @@
hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})"
by (force dest: Diff_infinite_finite)
hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
- by (metis Collect_def finite_set set_empty2)
+ by (metis finite_set set_empty2)
hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
then obtain c
where eq1: "[(a,c)]\<bullet>x = x"
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Sep 03 23:38:06 2011 +0200
@@ -714,48 +714,48 @@
fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_bname thy ("pt_"^ak_name);
- val simp_s = HOL_basic_ss addsimps [defn];
+ val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
in
- AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
+ AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
end) ak_names;
fun discrete_fs_inst discrete_ty defn =
fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_bname thy ("fs_"^ak_name);
- val supp_def = @{thm "Nominal.supp_def"};
- val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
+ val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
+ val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
in
- AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
+ AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
end) ak_names;
fun discrete_cp_inst discrete_ty defn =
fold (fn ak_name' => (fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
- val supp_def = @{thm "Nominal.supp_def"};
- val simp_s = HOL_ss addsimps [defn];
+ val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
+ val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
in
- AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
+ AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
end) ak_names)) ak_names;
in
thy26
- |> discrete_pt_inst @{type_name nat} @{thm "perm_nat_def"}
- |> discrete_fs_inst @{type_name nat} @{thm "perm_nat_def"}
- |> discrete_cp_inst @{type_name nat} @{thm "perm_nat_def"}
- |> discrete_pt_inst @{type_name bool} @{thm "perm_bool"}
- |> discrete_fs_inst @{type_name bool} @{thm "perm_bool"}
- |> discrete_cp_inst @{type_name bool} @{thm "perm_bool"}
- |> discrete_pt_inst @{type_name int} @{thm "perm_int_def"}
- |> discrete_fs_inst @{type_name int} @{thm "perm_int_def"}
- |> discrete_cp_inst @{type_name int} @{thm "perm_int_def"}
- |> discrete_pt_inst @{type_name char} @{thm "perm_char_def"}
- |> discrete_fs_inst @{type_name char} @{thm "perm_char_def"}
- |> discrete_cp_inst @{type_name char} @{thm "perm_char_def"}
+ |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
+ |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
+ |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
+ |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
+ |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
+ |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
+ |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
+ |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
+ |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
+ |> discrete_pt_inst @{type_name char} @{thm perm_char_def}
+ |> discrete_fs_inst @{type_name char} @{thm perm_char_def}
+ |> discrete_cp_inst @{type_name char} @{thm perm_char_def}
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Sep 03 23:38:06 2011 +0200
@@ -155,9 +155,9 @@
val supp_prod = @{thm supp_prod};
val fresh_prod = @{thm fresh_prod};
val supports_fresh = @{thm supports_fresh};
-val supports_def = @{thm Nominal.supports_def};
-val fresh_def = @{thm fresh_def};
-val supp_def = @{thm supp_def};
+val supports_def = Simpdata.mk_eq @{thm Nominal.supports_def};
+val fresh_def = Simpdata.mk_eq @{thm fresh_def};
+val supp_def = Simpdata.mk_eq @{thm supp_def};
val rev_simps = @{thms rev.simps};
val app_simps = @{thms append.simps};
val at_fin_set_supp = @{thm at_fin_set_supp};
@@ -306,7 +306,7 @@
val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
- val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
+ val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
val unfolded_perm_eq_thms =
if length descr = length new_type_names then []
--- a/src/HOL/Nominal/nominal_permeq.ML Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Sat Sep 03 23:38:06 2011 +0200
@@ -56,10 +56,10 @@
val finite_Un = @{thm "finite_Un"};
val conj_absorb = @{thm "conj_absorb"};
val not_false = @{thm "not_False_eq_True"}
-val perm_fun_def = @{thm "Nominal.perm_fun_def"};
+val perm_fun_def = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
val perm_eq_app = @{thm "Nominal.pt_fun_app_eq"};
-val supports_def = @{thm "Nominal.supports_def"};
-val fresh_def = @{thm "Nominal.fresh_def"};
+val supports_def = Simpdata.mk_eq @{thm "Nominal.supports_def"};
+val fresh_def = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
val fresh_prod = @{thm "Nominal.fresh_prod"};
val fresh_unit = @{thm "Nominal.fresh_unit"};
val supports_rule = @{thm "supports_finite"};
@@ -130,7 +130,7 @@
case redex of
(* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
(Const("Nominal.perm",_) $ pi $ f) =>
- (if (applicable_fun f) then SOME (perm_fun_def) else NONE)
+ (if (applicable_fun f) then SOME perm_fun_def else NONE)
| _ => NONE
end