assert Pure equations for theorem references; tuned
authorhaftmann
Sat Sep 03 17:32:34 2011 +0200 (2011-09-03 ago)
changeset 446848dde3352d5c4
parent 44683 daeb538c57bf
child 44685 f5bc7d9d0d74
assert Pure equations for theorem references; tuned
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_permeq.ML
     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