--- a/src/HOL/Library/Dlist.thy Wed Aug 18 12:05:44 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Wed Aug 18 12:26:15 2010 +0200
@@ -15,8 +15,8 @@
qed
lemma dlist_ext:
- assumes "list_of_dlist xs = list_of_dlist ys"
- shows "xs = ys"
+ assumes "list_of_dlist dxs = list_of_dlist dys"
+ shows "dxs = dys"
using assms by (simp add: list_of_dlist_inject)
@@ -107,6 +107,19 @@
by simp
+text {* Equality *}
+
+instantiation dlist :: (eq) eq
+begin
+
+definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+
+instance proof
+qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+
+end
+
+
section {* Induction principle and case distinction *}
lemma dlist_induct [case_names empty insert, induct type: dlist]:
@@ -283,6 +296,7 @@
end
+
hide_const (open) member fold foldr empty insert remove map filter null member length fold
end
--- a/src/ZF/Inductive_ZF.thy Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/Inductive_ZF.thy Wed Aug 18 12:26:15 2010 +0200
@@ -31,8 +31,8 @@
lemma refl_thin: "!!P. a = a ==> P ==> P" .
use "ind_syntax.ML"
+use "Tools/ind_cases.ML"
use "Tools/cartprod.ML"
-use "Tools/ind_cases.ML"
use "Tools/inductive_package.ML"
use "Tools/induct_tacs.ML"
use "Tools/primrec_package.ML"
--- a/src/ZF/Sum.thy Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/Sum.thy Wed Aug 18 12:26:15 2010 +0200
@@ -9,8 +9,6 @@
text{*And the "Part" primitive for simultaneous recursive type definitions*}
-global
-
definition sum :: "[i,i]=>i" (infixr "+" 65) where
"A+B == {0}*A Un {1}*B"
@@ -27,8 +25,6 @@
definition Part :: "[i,i=>i] => i" where
"Part(A,h) == {x: A. EX z. x = h(z)}"
-local
-
subsection{*Rules for the @{term Part} Primitive*}
lemma Part_iff:
--- a/src/ZF/Tools/primrec_package.ML Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Wed Aug 18 12:26:15 2010 +0200
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const ("0", Ind_Syntax.iT),
- #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
+ (Const (@{const_name 0}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/ZF.thy Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/ZF.thy Wed Aug 18 12:26:15 2010 +0200
@@ -12,8 +12,6 @@
ML {* Unsynchronized.reset eta_contract *}
-global
-
typedecl i
arities i :: "term"
@@ -209,8 +207,6 @@
subset_def: "A <= B == \<forall>x\<in>A. x\<in>B"
-local
-
axioms
(* ZF axioms -- see Suppes p.238
--- a/src/ZF/arith_data.ML Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/arith_data.ML Wed Aug 18 12:26:15 2010 +0200
@@ -24,12 +24,12 @@
val iT = Ind_Syntax.iT;
-val zero = Const("0", iT);
-val succ = Const("succ", iT --> iT);
+val zero = Const(@{const_name 0}, iT);
+val succ = Const(@{const_name succ}, iT --> iT);
fun mk_succ t = succ $ t;
val one = mk_succ zero;
-val mk_plus = FOLogic.mk_binop "Arith.add";
+val mk_plus = FOLogic.mk_binop @{const_name Arith.add};
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
fun mk_sum [] = zero
@@ -40,13 +40,13 @@
fun long_mk_sum [] = zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-val dest_plus = FOLogic.dest_bin "Arith.add" iT;
+val dest_plus = FOLogic.dest_bin @{const_name Arith.add} iT;
(* dest_sum *)
-fun dest_sum (Const("0",_)) = []
- | dest_sum (Const("succ",_) $ t) = one :: dest_sum t
- | dest_sum (Const("Arith.add",_) $ t $ u) = dest_sum t @ dest_sum u
+fun dest_sum (Const(@{const_name 0},_)) = []
+ | dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
+ | dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
| dest_sum tm = [tm];
(*Apply the given rewrite (if present) just once*)
@@ -83,14 +83,14 @@
(*** Use CancelNumerals simproc without binary numerals,
just for cancellation ***)
-val mk_times = FOLogic.mk_binop "Arith.mult";
+val mk_times = FOLogic.mk_binop @{const_name Arith.mult};
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 "Arith.mult" iT;
+val dest_times = FOLogic.dest_bin @{const_name Arith.mult} iT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -174,8 +174,8 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
- val mk_bal = FOLogic.mk_binrel "Ordinal.lt"
- val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
+ val mk_bal = FOLogic.mk_binrel @{const_name Ordinal.lt}
+ val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
fun trans_tac _ = gen_trans_tac @{thm iff_trans}
@@ -187,8 +187,8 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natdiff_cancel_numerals"
- val mk_bal = FOLogic.mk_binop "Arith.diff"
- val dest_bal = FOLogic.dest_bin "Arith.diff" iT
+ val mk_bal = FOLogic.mk_binop @{const_name Arith.diff}
+ val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
fun trans_tac _ = gen_trans_tac @{thm trans}
--- a/src/ZF/ind_syntax.ML Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/ind_syntax.ML Wed Aug 18 12:26:15 2010 +0200
@@ -18,7 +18,7 @@
(** Abstract syntax definitions for ZF **)
-val iT = Type("i",[]);
+val iT = Type(@{type_name i}, []);
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
--- a/src/ZF/simpdata.ML Wed Aug 18 12:05:44 2010 +0200
+++ b/src/ZF/simpdata.ML Wed Aug 18 12:26:15 2010 +0200
@@ -19,27 +19,27 @@
| NONE => [th])
| _ => [th]
in case concl_of th of
- Const("Trueprop",_) $ P =>
+ Const(@{const_name Trueprop},_) $ P =>
(case P of
Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
- | Const("True",_) => []
- | Const("False",_) => []
+ | Const(@{const_name True},_) => []
+ | Const(@{const_name False},_) => []
| A => tryrules conn_pairs A)
| _ => [th]
end;
(*Analyse a rigid formula*)
val ZF_conn_pairs =
- [("Ball", [@{thm bspec}]),
- ("All", [@{thm spec}]),
- ("op -->", [@{thm mp}]),
- ("op &", [@{thm conjunct1}, @{thm conjunct2}])];
+ [(@{const_name Ball}, [@{thm bspec}]),
+ (@{const_name All}, [@{thm spec}]),
+ (@{const_name "op -->"}, [@{thm mp}]),
+ (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =
- [("Collect", [@{thm CollectD1}, @{thm CollectD2}]),
- (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
- (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
+ [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
+ (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
+ (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);