merged
authorhaftmann
Sat Sep 03 23:38:06 2011 +0200 (2011-09-03)
changeset 4468867b78d5dea5b
parent 44682 e5ba1c0b8cac
parent 44687 20deab90494e
child 44689 f247fc952f31
child 44693 a9635943a3e9
merged
     1.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Sat Sep 03 22:11:49 2011 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Sat Sep 03 23:38:06 2011 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  header {* Simply-typed lambda-calculus with let and tuple patterns *}
     1.5  
     1.6  theory Pattern
     1.7 -imports Nominal
     1.8 +imports "../Nominal"
     1.9  begin
    1.10  
    1.11  no_syntax
    1.12 @@ -622,7 +622,7 @@
    1.13      (auto simp add: Cons_eq_append_conv fresh_star_def
    1.14       fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append
    1.15       supp_prod fresh_prod supp_atm fresh_atm
    1.16 -     dest: notE [OF iffD1 [OF fresh_def [THEN meta_eq_to_obj_eq]]])
    1.17 +     dest: notE [OF iffD1 [OF fresh_def]])
    1.18  
    1.19  lemma perm_mem_left: "(x::name) \<in> ((pi::name prm) \<bullet> A) \<Longrightarrow> (rev pi \<bullet> x) \<in> A"
    1.20    by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp)
     2.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Sep 03 22:11:49 2011 +0200
     2.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Sep 03 23:38:06 2011 +0200
     2.3 @@ -32,7 +32,7 @@
     2.4  (* an auxiliary constant for the decision procedure involving *) 
     2.5  (* permutations (to avoid loops when using perm-compositions)  *)
     2.6  definition
     2.7 -  "perm_aux pi x \<equiv> pi\<bullet>x"
     2.8 +  "perm_aux pi x = pi\<bullet>x"
     2.9  
    2.10  (* overloaded permutation operations *)
    2.11  overloading
    2.12 @@ -51,61 +51,42 @@
    2.13  begin
    2.14  
    2.15  definition
    2.16 -  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    2.17 -
    2.18 -fun
    2.19 -  perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool"
    2.20 -where
    2.21 +  perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    2.22 +
    2.23 +primrec perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    2.24    true_eqvt:  "perm_bool pi True  = True"
    2.25  | false_eqvt: "perm_bool pi False = False"
    2.26  
    2.27 -fun
    2.28 -  perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" 
    2.29 -where 
    2.30 +primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    2.31    "perm_unit pi () = ()"
    2.32    
    2.33 -fun
    2.34 -  perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"
    2.35 -where
    2.36 +primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    2.37    "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)"
    2.38  
    2.39 -fun
    2.40 -  perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.41 -where
    2.42 +primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.43    nil_eqvt:  "perm_list pi []     = []"
    2.44  | cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    2.45  
    2.46 -fun
    2.47 -  perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option"
    2.48 -where
    2.49 +primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where
    2.50    some_eqvt:  "perm_option pi (Some x) = Some (pi\<bullet>x)"
    2.51  | none_eqvt:  "perm_option pi None     = None"
    2.52  
    2.53 -definition
    2.54 -  perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char"
    2.55 -where
    2.56 -  perm_char_def: "perm_char pi c \<equiv> c"
    2.57 -
    2.58 -definition
    2.59 -  perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat"
    2.60 -where
    2.61 -  perm_nat_def: "perm_nat pi i \<equiv> i"
    2.62 -
    2.63 -definition
    2.64 -  perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int"
    2.65 -where
    2.66 -  perm_int_def: "perm_int pi i \<equiv> i"
    2.67 -
    2.68 -fun
    2.69 -  perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"
    2.70 -where
    2.71 +definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    2.72 +  perm_char_def: "perm_char pi c = c"
    2.73 +
    2.74 +definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    2.75 +  perm_nat_def: "perm_nat pi i = i"
    2.76 +
    2.77 +definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    2.78 +  perm_int_def: "perm_int pi i = i"
    2.79 +
    2.80 +primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    2.81    nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    2.82  | nnone_eqvt:  "perm_noption pi nNone     = nNone"
    2.83  
    2.84 -fun
    2.85 -  perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod"
    2.86 -where
    2.87 +primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where
    2.88    "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
    2.89 +
    2.90  end
    2.91  
    2.92  
    2.93 @@ -188,18 +169,18 @@
    2.94  (*==============================*)
    2.95  
    2.96  definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where
    2.97 -  "pi1 \<triangleq> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
    2.98 +  "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)"
    2.99  
   2.100  section {* Support, Freshness and Supports*}
   2.101  (*========================================*)
   2.102  definition supp :: "'a \<Rightarrow> ('x set)" where  
   2.103 -   "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   2.104 +   "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   2.105  
   2.106  definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where
   2.107 -   "a \<sharp> x \<equiv> a \<notin> supp x"
   2.108 +   "a \<sharp> x \<longleftrightarrow> a \<notin> supp x"
   2.109  
   2.110  definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where
   2.111 -   "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
   2.112 +   "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))"
   2.113  
   2.114  (* lemmas about supp *)
   2.115  lemma supp_fresh_iff: 
   2.116 @@ -1731,7 +1712,7 @@
   2.117    hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
   2.118      by (force dest: Diff_infinite_finite)
   2.119    hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
   2.120 -    by (metis Collect_def finite_set set_empty2)
   2.121 +    by (metis finite_set set_empty2)
   2.122    hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
   2.123    then obtain c 
   2.124      where eq1: "[(a,c)]\<bullet>x = x" 
     3.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 22:11:49 2011 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Sep 03 23:38:06 2011 +0200
     3.3 @@ -714,48 +714,48 @@
     3.4               fold (fn ak_name => fn thy =>
     3.5               let
     3.6                 val qu_class = Sign.full_bname thy ("pt_"^ak_name);
     3.7 -               val simp_s = HOL_basic_ss addsimps [defn];
     3.8 +               val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
     3.9                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    3.10               in 
    3.11 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    3.12 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
    3.13               end) ak_names;
    3.14  
    3.15            fun discrete_fs_inst discrete_ty defn = 
    3.16               fold (fn ak_name => fn thy =>
    3.17               let
    3.18                 val qu_class = Sign.full_bname thy ("fs_"^ak_name);
    3.19 -               val supp_def = @{thm "Nominal.supp_def"};
    3.20 -               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
    3.21 +               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
    3.22 +               val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
    3.23                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
    3.24               in 
    3.25 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    3.26 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
    3.27               end) ak_names;
    3.28  
    3.29            fun discrete_cp_inst discrete_ty defn = 
    3.30               fold (fn ak_name' => (fold (fn ak_name => fn thy =>
    3.31               let
    3.32                 val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
    3.33 -               val supp_def = @{thm "Nominal.supp_def"};
    3.34 -               val simp_s = HOL_ss addsimps [defn];
    3.35 +               val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"};
    3.36 +               val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
    3.37                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
    3.38               in
    3.39 -               AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    3.40 +               AxClass.prove_arity (discrete_ty, [], [qu_class]) proof thy
    3.41               end) ak_names)) ak_names;
    3.42  
    3.43          in
    3.44           thy26
    3.45 -         |> discrete_pt_inst @{type_name nat}  @{thm "perm_nat_def"}
    3.46 -         |> discrete_fs_inst @{type_name nat}  @{thm "perm_nat_def"}
    3.47 -         |> discrete_cp_inst @{type_name nat}  @{thm "perm_nat_def"}
    3.48 -         |> discrete_pt_inst @{type_name bool} @{thm "perm_bool"}
    3.49 -         |> discrete_fs_inst @{type_name bool} @{thm "perm_bool"}
    3.50 -         |> discrete_cp_inst @{type_name bool} @{thm "perm_bool"}
    3.51 -         |> discrete_pt_inst @{type_name int} @{thm "perm_int_def"}
    3.52 -         |> discrete_fs_inst @{type_name int} @{thm "perm_int_def"}
    3.53 -         |> discrete_cp_inst @{type_name int} @{thm "perm_int_def"}
    3.54 -         |> discrete_pt_inst @{type_name char} @{thm "perm_char_def"}
    3.55 -         |> discrete_fs_inst @{type_name char} @{thm "perm_char_def"}
    3.56 -         |> discrete_cp_inst @{type_name char} @{thm "perm_char_def"}
    3.57 +         |> discrete_pt_inst @{type_name nat} @{thm perm_nat_def}
    3.58 +         |> discrete_fs_inst @{type_name nat} @{thm perm_nat_def}
    3.59 +         |> discrete_cp_inst @{type_name nat} @{thm perm_nat_def}
    3.60 +         |> discrete_pt_inst @{type_name bool} @{thm perm_bool}
    3.61 +         |> discrete_fs_inst @{type_name bool} @{thm perm_bool}
    3.62 +         |> discrete_cp_inst @{type_name bool} @{thm perm_bool}
    3.63 +         |> discrete_pt_inst @{type_name int} @{thm perm_int_def}
    3.64 +         |> discrete_fs_inst @{type_name int} @{thm perm_int_def}
    3.65 +         |> discrete_cp_inst @{type_name int} @{thm perm_int_def}
    3.66 +         |> discrete_pt_inst @{type_name char} @{thm perm_char_def}
    3.67 +         |> discrete_fs_inst @{type_name char} @{thm perm_char_def}
    3.68 +         |> discrete_cp_inst @{type_name char} @{thm perm_char_def}
    3.69          end;
    3.70  
    3.71  
     4.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 22:11:49 2011 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 23:38:06 2011 +0200
     4.3 @@ -155,9 +155,9 @@
     4.4  val supp_prod = @{thm supp_prod};
     4.5  val fresh_prod = @{thm fresh_prod};
     4.6  val supports_fresh = @{thm supports_fresh};
     4.7 -val supports_def = @{thm Nominal.supports_def};
     4.8 -val fresh_def = @{thm fresh_def};
     4.9 -val supp_def = @{thm supp_def};
    4.10 +val supports_def = Simpdata.mk_eq @{thm Nominal.supports_def};
    4.11 +val fresh_def = Simpdata.mk_eq @{thm fresh_def};
    4.12 +val supp_def = Simpdata.mk_eq @{thm supp_def};
    4.13  val rev_simps = @{thms rev.simps};
    4.14  val app_simps = @{thms append.simps};
    4.15  val at_fin_set_supp = @{thm at_fin_set_supp};
    4.16 @@ -306,7 +306,7 @@
    4.17      val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
    4.18  
    4.19      val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
    4.20 -    val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
    4.21 +    val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
    4.22  
    4.23      val unfolded_perm_eq_thms =
    4.24        if length descr = length new_type_names then []
     5.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 22:11:49 2011 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Sep 03 23:38:06 2011 +0200
     5.3 @@ -56,10 +56,10 @@
     5.4  val finite_Un     = @{thm "finite_Un"};
     5.5  val conj_absorb   = @{thm "conj_absorb"};
     5.6  val not_false     = @{thm "not_False_eq_True"}
     5.7 -val perm_fun_def  = @{thm "Nominal.perm_fun_def"};
     5.8 +val perm_fun_def  = Simpdata.mk_eq @{thm "Nominal.perm_fun_def"};
     5.9  val perm_eq_app   = @{thm "Nominal.pt_fun_app_eq"};
    5.10 -val supports_def  = @{thm "Nominal.supports_def"};
    5.11 -val fresh_def     = @{thm "Nominal.fresh_def"};
    5.12 +val supports_def  = Simpdata.mk_eq @{thm "Nominal.supports_def"};
    5.13 +val fresh_def     = Simpdata.mk_eq @{thm "Nominal.fresh_def"};
    5.14  val fresh_prod    = @{thm "Nominal.fresh_prod"};
    5.15  val fresh_unit    = @{thm "Nominal.fresh_unit"};
    5.16  val supports_rule = @{thm "supports_finite"};
    5.17 @@ -130,7 +130,7 @@
    5.18       case redex of 
    5.19         (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
    5.20         (Const("Nominal.perm",_) $ pi $ f)  => 
    5.21 -          (if (applicable_fun f) then SOME (perm_fun_def) else NONE)
    5.22 +          (if (applicable_fun f) then SOME perm_fun_def else NONE)
    5.23        | _ => NONE
    5.24     end
    5.25