author haftmann Sat Sep 03 17:32:34 2011 +0200 (2011-09-03 ago) changeset 44684 8dde3352d5c4 parent 44683 daeb538c57bf child 44685 f5bc7d9d0d74
assert Pure equations for theorem references; tuned
```     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 17:32:34 2011 +0200
1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 17:32:34 2011 +0200
1.3 @@ -714,48 +714,48 @@
1.4               fold (fn ak_name => fn thy =>
1.5               let
1.6                 val qu_class = Sign.full_bname thy ("pt_"^ak_name);
1.7 -               val simp_s = HOL_basic_ss addsimps [defn];
1.8 +               val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
1.9                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
1.10               in
1.11 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
1.12 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
1.13               end) ak_names;
1.14
1.15            fun discrete_fs_inst discrete_ty defn =
1.16               fold (fn ak_name => fn thy =>
1.17               let
1.18                 val qu_class = Sign.full_bname thy ("fs_"^ak_name);
1.19 -               val supp_def = @{thm "Nominal.supp_def"};
1.20 -               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
1.21 +               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
1.22 +               val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
1.23                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
1.24               in
1.25 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
1.26 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
1.27               end) ak_names;
1.28
1.29            fun discrete_cp_inst discrete_ty defn =
1.30               fold (fn ak_name' => (fold (fn ak_name => fn thy =>
1.31               let
1.32                 val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
1.33 -               val supp_def = @{thm "Nominal.supp_def"};
1.34 -               val simp_s = HOL_ss addsimps [defn];
1.35 +               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
1.36 +               val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
1.37                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
1.38               in
1.39 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
1.40 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
1.41               end) ak_names)) ak_names;
1.42
1.43          in
1.44           thy26
1.45 -         |> discrete_pt_inst @{type_name nat}  @{thm "perm_nat_def"}
1.46 -         |> discrete_fs_inst @{type_name nat}  @{thm "perm_nat_def"}
1.47 -         |> discrete_cp_inst @{type_name nat}  @{thm "perm_nat_def"}
1.48 -         |> discrete_pt_inst @{type_name bool} @{thm "perm_bool"}
1.49 -         |> discrete_fs_inst @{type_name bool} @{thm "perm_bool"}
1.50 -         |> discrete_cp_inst @{type_name bool} @{thm "perm_bool"}
1.51 -         |> discrete_pt_inst @{type_name int} @{thm "perm_int_def"}
1.52 -         |> discrete_fs_inst @{type_name int} @{thm "perm_int_def"}
1.53 -         |> discrete_cp_inst @{type_name int} @{thm "perm_int_def"}
1.54 -         |> discrete_pt_inst @{type_name char} @{thm "perm_char_def"}
1.55 -         |> discrete_fs_inst @{type_name char} @{thm "perm_char_def"}
1.56 -         |> discrete_cp_inst @{type_name char} @{thm "perm_char_def"}
1.57 +         |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
1.58 +         |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
1.59 +         |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
1.60 +         |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
1.61 +         |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
1.62 +         |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
1.63 +         |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
1.64 +         |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
1.65 +         |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
1.66 +         |> discrete_pt_inst @{type_name char} @{thm perm_char_def}
1.67 +         |> discrete_fs_inst @{type_name char} @{thm perm_char_def}
1.68 +         |> discrete_cp_inst @{type_name char} @{thm perm_char_def}
1.69          end;
1.70
1.71
```
```     2.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 17:32:34 2011 +0200
2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 17:32:34 2011 +0200
2.3 @@ -56,10 +56,10 @@
2.4  val finite_Un     = @{thm "finite_Un"};
2.5  val conj_absorb   = @{thm "conj_absorb"};
2.6  val not_false     = @{thm "not_False_eq_True"}
2.7 -val perm_fun_def  = @{thm "Nominal.perm_fun_def"};
2.8 +val perm_fun_def  = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
2.9  val perm_eq_app   = @{thm "Nominal.pt_fun_app_eq"};
2.10 -val supports_def  = @{thm "Nominal.supports_def"};
2.11 -val fresh_def     = @{thm "Nominal.fresh_def"};
2.12 +val supports_def  = Simpdata.mk_eq @{thm "Nominal.supports_def"};
2.13 +val fresh_def     = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
2.14  val fresh_prod    = @{thm "Nominal.fresh_prod"};
2.15  val fresh_unit    = @{thm "Nominal.fresh_unit"};
2.16  val supports_rule = @{thm "supports_finite"};
2.17 @@ -130,7 +130,7 @@
2.18       case redex of
2.19         (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
2.20         (Const("Nominal.perm",_) \$ pi \$ f)  =>
2.21 -          (if (applicable_fun f) then SOME (perm_fun_def) else NONE)
2.22 +          (if (applicable_fun f) then SOME perm_fun_def else NONE)
2.23        | _ => NONE
2.24     end
2.25
```