# HG changeset patch # User wenzelm # Date 1202761932 -3600 # Node ID b67a225b50fd6050ce490eca926395805aa1c701 # Parent 279016aebc411cdd582377fd81c57d4ebd138eaa removed unnecessary theory qualifiers; diff -r 279016aebc41 -r b67a225b50fd src/ZF/Induct/Primrec.thy --- a/src/ZF/Induct/Primrec.thy Mon Feb 11 21:32:11 2008 +0100 +++ b/src/ZF/Induct/Primrec.thy Mon Feb 11 21:32:12 2008 +0100 @@ -31,7 +31,7 @@ definition COMP :: "[i,i]=>i" where - "COMP(g,fs) == \l \ list(nat). g ` List_ZF.map(\f. f`l, fs)" + "COMP(g,fs) == \l \ list(nat). g ` map(\f. f`l, fs)" definition PREC :: "[i,i]=>i" where @@ -93,7 +93,7 @@ monos list_mono con_defs SC_def CONSTANT_def PROJ_def COMP_def PREC_def type_intros nat_typechecks list.intros - lam_type list_case_type drop_type List_ZF.map_type + lam_type list_case_type drop_type map_type apply_type rec_type diff -r 279016aebc41 -r b67a225b50fd src/ZF/Induct/Term.thy --- a/src/ZF/Induct/Term.thy Mon Feb 11 21:32:11 2008 +0100 +++ b/src/ZF/Induct/Term.thy Mon Feb 11 21:32:12 2008 +0100 @@ -235,7 +235,7 @@ \medskip Theorems about @{text term_map}. *} -declare List_ZF.map_compose [simp] +declare map_compose [simp] lemma term_map_ident: "t \ term(A) ==> term_map(\u. u, t) = t" by (induct rule: term_induct_eqn) simp diff -r 279016aebc41 -r b67a225b50fd src/ZF/UNITY/Monotonicity.thy --- a/src/ZF/UNITY/Monotonicity.thy Mon Feb 11 21:32:11 2008 +0100 +++ b/src/ZF/UNITY/Monotonicity.thy Mon Feb 11 21:32:12 2008 +0100 @@ -69,7 +69,7 @@ lemma take_mono_left: "[| i le j; xs \ list(A); j \ nat |] ==> \ prefix(A)" -by (blast intro: Nat_ZF.le_in_nat take_mono_left_lemma) +by (blast intro: le_in_nat take_mono_left_lemma) lemma take_mono_right: "[| \ prefix(A); i \ nat |] diff -r 279016aebc41 -r b67a225b50fd src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Mon Feb 11 21:32:11 2008 +0100 +++ b/src/ZF/ind_syntax.ML Mon Feb 11 21:32:12 2008 +0100 @@ -127,7 +127,7 @@ (fn t => "Datatype set not previously declared as constant: " ^ Sign.string_of_term @{theory IFOL} t); val rec_names = (*nat doesn't have to be added*) - @{const_name "Nat_ZF.nat"} :: map (#1 o dest_Const) rec_hds + @{const_name "nat"} :: map (#1 o dest_Const) rec_hds val u = if co then quniv else univ val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t diff -r 279016aebc41 -r b67a225b50fd src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Mon Feb 11 21:32:11 2008 +0100 +++ b/src/ZF/int_arith.ML Mon Feb 11 21:32:12 2008 +0100 @@ -111,11 +111,11 @@ | find_first_numeral past [] = raise TERM("find_first_numeral", []); val zero = mk_numeral 0; -val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"}; +val mk_plus = FOLogic.mk_binop @{const_name "zadd"}; val iT = Ind_Syntax.iT; -val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT); +val zminus_const = Const (@{const_name "zminus"}, iT --> iT); (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*) fun mk_sum [] = zero @@ -126,30 +126,30 @@ fun long_mk_sum [] = zero | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); -val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT; +val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT; (*decompose additions AND subtractions as a sum*) -fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) = +fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) = dest_summing (pos, t, dest_summing (pos, u, ts)) - | dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) = + | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) = dest_summing (pos, t, dest_summing (not pos, u, ts)) | dest_summing (pos, t, ts) = if pos then t::ts else zminus_const$t :: ts; fun dest_sum t = dest_summing (true, t, []); -val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"}; -val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT; +val mk_diff = FOLogic.mk_binop @{const_name "zdiff"}; +val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT; val one = mk_numeral 1; -val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"}; +val mk_times = FOLogic.mk_binop @{const_name "zmult"}; fun mk_prod [] = one | mk_prod [t] = t | mk_prod (t :: ts) = if t = one then mk_prod ts else mk_times (t, mk_prod ts); -val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT; +val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT; fun dest_prod t = let val (t,u) = dest_times t @@ -160,7 +160,7 @@ fun mk_coeff (k, t) = mk_times (mk_numeral k, t); (*Express t as a product of (possibly) a numeral with other sorted terms*) -fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t +fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t | dest_coeff sign t = let val ts = sort Term.term_ord (dest_prod t) val (n, ts') = find_first_numeral [] ts @@ -254,8 +254,8 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = ArithData.prove_conv "intless_cancel_numerals" - val mk_bal = FOLogic.mk_binrel @{const_name "Int_ZF.zless"} - val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT + val mk_bal = FOLogic.mk_binrel @{const_name "zless"} + val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT val bal_add1 = less_add_iff1 RS iff_trans val bal_add2 = less_add_iff2 RS iff_trans ); @@ -263,8 +263,8 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon val prove_conv = ArithData.prove_conv "intle_cancel_numerals" - val mk_bal = FOLogic.mk_binrel @{const_name "Int_ZF.zle"} - val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT + val mk_bal = FOLogic.mk_binrel @{const_name "zle"} + val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT val bal_add1 = le_add_iff1 RS iff_trans val bal_add2 = le_add_iff2 RS iff_trans );