removed unnecessary theory qualifiers;
authorwenzelm
Mon Feb 11 21:32:12 2008 +0100 (2008-02-11)
changeset 26059b67a225b50fd
parent 26058 279016aebc41
child 26060 cd89870aa92f
removed unnecessary theory qualifiers;
src/ZF/Induct/Primrec.thy
src/ZF/Induct/Term.thy
src/ZF/UNITY/Monotonicity.thy
src/ZF/ind_syntax.ML
src/ZF/int_arith.ML
     1.1 --- a/src/ZF/Induct/Primrec.thy	Mon Feb 11 21:32:11 2008 +0100
     1.2 +++ b/src/ZF/Induct/Primrec.thy	Mon Feb 11 21:32:12 2008 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  definition
     1.6    COMP :: "[i,i]=>i"  where
     1.7 -  "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List_ZF.map(\<lambda>f. f`l, fs)"
     1.8 +  "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` map(\<lambda>f. f`l, fs)"
     1.9  
    1.10  definition
    1.11    PREC :: "[i,i]=>i"  where
    1.12 @@ -93,7 +93,7 @@
    1.13    monos list_mono
    1.14    con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def
    1.15    type_intros nat_typechecks list.intros
    1.16 -    lam_type list_case_type drop_type List_ZF.map_type
    1.17 +    lam_type list_case_type drop_type map_type
    1.18      apply_type rec_type
    1.19  
    1.20  
     2.1 --- a/src/ZF/Induct/Term.thy	Mon Feb 11 21:32:11 2008 +0100
     2.2 +++ b/src/ZF/Induct/Term.thy	Mon Feb 11 21:32:12 2008 +0100
     2.3 @@ -235,7 +235,7 @@
     2.4    \medskip Theorems about @{text term_map}.
     2.5  *}
     2.6  
     2.7 -declare List_ZF.map_compose [simp]
     2.8 +declare map_compose [simp]
     2.9  
    2.10  lemma term_map_ident: "t \<in> term(A) ==> term_map(\<lambda>u. u, t) = t"
    2.11    by (induct rule: term_induct_eqn) simp
     3.1 --- a/src/ZF/UNITY/Monotonicity.thy	Mon Feb 11 21:32:11 2008 +0100
     3.2 +++ b/src/ZF/UNITY/Monotonicity.thy	Mon Feb 11 21:32:12 2008 +0100
     3.3 @@ -69,7 +69,7 @@
     3.4  lemma take_mono_left:
     3.5       "[| i le j; xs \<in> list(A); j \<in> nat |]
     3.6        ==> <take(i, xs), take(j, xs)> \<in> prefix(A)"
     3.7 -by (blast intro: Nat_ZF.le_in_nat take_mono_left_lemma) 
     3.8 +by (blast intro: le_in_nat take_mono_left_lemma) 
     3.9  
    3.10  lemma take_mono_right:
    3.11       "[| <xs,ys> \<in> prefix(A); i \<in> nat |] 
     4.1 --- a/src/ZF/ind_syntax.ML	Mon Feb 11 21:32:11 2008 +0100
     4.2 +++ b/src/ZF/ind_syntax.ML	Mon Feb 11 21:32:12 2008 +0100
     4.3 @@ -127,7 +127,7 @@
     4.4            (fn t => "Datatype set not previously declared as constant: " ^
     4.5                     Sign.string_of_term @{theory IFOL} t);
     4.6          val rec_names = (*nat doesn't have to be added*)
     4.7 -	    @{const_name "Nat_ZF.nat"} :: map (#1 o dest_Const) rec_hds
     4.8 +	    @{const_name "nat"} :: map (#1 o dest_Const) rec_hds
     4.9  	val u = if co then quniv else univ
    4.10  	val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
    4.11            (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
     5.1 --- a/src/ZF/int_arith.ML	Mon Feb 11 21:32:11 2008 +0100
     5.2 +++ b/src/ZF/int_arith.ML	Mon Feb 11 21:32:12 2008 +0100
     5.3 @@ -111,11 +111,11 @@
     5.4    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
     5.5  
     5.6  val zero = mk_numeral 0;
     5.7 -val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"};
     5.8 +val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
     5.9  
    5.10  val iT = Ind_Syntax.iT;
    5.11  
    5.12 -val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT);
    5.13 +val zminus_const = Const (@{const_name "zminus"}, iT --> iT);
    5.14  
    5.15  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    5.16  fun mk_sum []        = zero
    5.17 @@ -126,30 +126,30 @@
    5.18  fun long_mk_sum []        = zero
    5.19    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    5.20  
    5.21 -val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT;
    5.22 +val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT;
    5.23  
    5.24  (*decompose additions AND subtractions as a sum*)
    5.25 -fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) =
    5.26 +fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
    5.27          dest_summing (pos, t, dest_summing (pos, u, ts))
    5.28 -  | dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) =
    5.29 +  | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
    5.30          dest_summing (pos, t, dest_summing (not pos, u, ts))
    5.31    | dest_summing (pos, t, ts) =
    5.32          if pos then t::ts else zminus_const$t :: ts;
    5.33  
    5.34  fun dest_sum t = dest_summing (true, t, []);
    5.35  
    5.36 -val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"};
    5.37 -val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT;
    5.38 +val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
    5.39 +val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT;
    5.40  
    5.41  val one = mk_numeral 1;
    5.42 -val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"};
    5.43 +val mk_times = FOLogic.mk_binop @{const_name "zmult"};
    5.44  
    5.45  fun mk_prod [] = one
    5.46    | mk_prod [t] = t
    5.47    | mk_prod (t :: ts) = if t = one then mk_prod ts
    5.48                          else mk_times (t, mk_prod ts);
    5.49  
    5.50 -val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT;
    5.51 +val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT;
    5.52  
    5.53  fun dest_prod t =
    5.54        let val (t,u) = dest_times t
    5.55 @@ -160,7 +160,7 @@
    5.56  fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
    5.57  
    5.58  (*Express t as a product of (possibly) a numeral with other sorted terms*)
    5.59 -fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t
    5.60 +fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
    5.61    | dest_coeff sign t =
    5.62      let val ts = sort Term.term_ord (dest_prod t)
    5.63          val (n, ts') = find_first_numeral [] ts
    5.64 @@ -254,8 +254,8 @@
    5.65  structure LessCancelNumerals = CancelNumeralsFun
    5.66   (open CancelNumeralsCommon
    5.67    val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
    5.68 -  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zless"}
    5.69 -  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT
    5.70 +  val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
    5.71 +  val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT
    5.72    val bal_add1 = less_add_iff1 RS iff_trans
    5.73    val bal_add2 = less_add_iff2 RS iff_trans
    5.74  );
    5.75 @@ -263,8 +263,8 @@
    5.76  structure LeCancelNumerals = CancelNumeralsFun
    5.77   (open CancelNumeralsCommon
    5.78    val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
    5.79 -  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zle"}
    5.80 -  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT
    5.81 +  val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
    5.82 +  val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT
    5.83    val bal_add1 = le_add_iff1 RS iff_trans
    5.84    val bal_add2 = le_add_iff2 RS iff_trans
    5.85  );