--- a/src/HOL/Library/refute.ML Mon Sep 01 16:34:40 2014 +0200
+++ b/src/HOL/Library/refute.ML Mon Sep 01 17:34:03 2014 +0200
@@ -402,7 +402,7 @@
fun is_IDT_constructor thy (s, T) =
(case body_type T of
Type (s', _) =>
- (case Old_Datatype_Data.get_constrs thy s' of
+ (case BNF_LFP_Compat.get_constrs thy s' of
SOME constrs =>
List.exists (fn (cname, cty) =>
cname = s andalso Sign.typ_instance thy (T, cty)) constrs
@@ -417,7 +417,7 @@
fun is_IDT_recursor thy (s, _) =
let
val rec_names = Symtab.fold (append o #rec_names o snd)
- (Old_Datatype_Data.get_all thy) []
+ (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) []
in
(* I'm not quite sure if checking the name 's' is sufficient, *)
(* or if we should also check the type 'T'. *)
@@ -643,7 +643,6 @@
let
val thy = Proof_Context.theory_of ctxt
val _ = tracing "Adding axioms..."
- val axioms = Theory.all_axioms_of thy
fun collect_this_axiom (axname, ax) axs =
let
val ax' = unfold_defs thy ax
@@ -691,7 +690,7 @@
(* axiomatic type classes *)
| Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
| Type (s, Ts) =>
- (case Old_Datatype_Data.get_info thy s of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
SOME _ => (* inductive datatype *)
(* only collect relevant type axioms for the argument types *)
fold collect_type_axioms Ts axs
@@ -820,7 +819,7 @@
| Type (@{type_name prop}, []) => acc
| Type (@{type_name set}, [T1]) => collect_types T1 acc
| Type (s, Ts) =>
- (case Old_Datatype_Data.get_info thy s of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
SOME info => (* inductive datatype *)
let
val index = #index info
@@ -1015,7 +1014,7 @@
(* TODO: no warning needed for /positive/ occurrences of IDTs *)
val maybe_spurious = Library.exists (fn
Type (s, _) =>
- (case Old_Datatype_Data.get_info thy s of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
SOME info => (* inductive datatype *)
let
val index = #index info
@@ -1741,7 +1740,7 @@
val thy = Proof_Context.theory_of ctxt
val (typs, terms) = model
fun interpret_term (Type (s, Ts)) =
- (case Old_Datatype_Data.get_info thy s of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
SOME info => (* inductive datatype *)
let
(* only recursive IDTs have an associated depth *)
@@ -1866,7 +1865,7 @@
HOLogic_empty_set) pairss
end
| Type (s, Ts) =>
- (case Old_Datatype_Data.get_info thy s of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
SOME info =>
(case AList.lookup (op =) typs T of
SOME 0 =>
@@ -1932,7 +1931,7 @@
Const (s, T) =>
(case body_type T of
Type (s', Ts') =>
- (case Old_Datatype_Data.get_info thy s' of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s' of
SOME info => (* body type is an inductive datatype *)
let
val index = #index info
@@ -2404,7 +2403,7 @@
end
else
NONE (* not a recursion operator of this datatype *)
- ) (Old_Datatype_Data.get_all thy) NONE
+ ) (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) NONE
| _ => (* head of term is not a constant *)
NONE
end;
@@ -2838,7 +2837,7 @@
in
(case T of
Type (s, Ts) =>
- (case Old_Datatype_Data.get_info thy s of
+ (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
SOME info => (* inductive datatype *)
let
val (typs, _) = model
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:34:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 17:34:03 2014 +0200
@@ -15,12 +15,11 @@
val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
- val the_spec: theory -> nesting_preference -> string ->
- (string * sort) list * (string * typ list) list
+ val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
val the_descr: theory -> nesting_preference -> string list ->
Old_Datatype_Aux.descr * (string * sort) list * string list * string
* (string list * string list) * (typ list * typ list)
- val get_constrs: theory -> nesting_preference -> string -> (string * typ) list option
+ val get_constrs: theory -> string -> (string * typ) list option
val interpretation: nesting_preference ->
(Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
val datatype_compat: string list -> local_theory -> local_theory
@@ -178,7 +177,9 @@
#5 (mk_infos_of_mutually_recursive_new_datatypes nesting_pref false subset [fpT_name] lthy);
in
infos_of nesting_pref
- handle ERROR _ => if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else []
+ handle ERROR _ =>
+ (if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else [])
+ handle ERROR _ => []
end;
fun get_all thy nesting_pref =
@@ -213,13 +214,13 @@
SOME info => info
| NONE => error ("Unknown datatype " ^ quote T_name));
-fun the_spec thy nesting_pref T_name =
+fun the_spec thy T_name =
let
- val {descr, index, ...} = the_info thy nesting_pref T_name;
+ val {descr, index, ...} = the_info thy Keep_Nesting T_name;
val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
- val Ts = map Old_Datatype_Aux.dest_DtTFree Ds;
+ val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
- in (Ts, ctrs) end;
+ in (tfrees, ctrs) end;
fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
let
@@ -253,8 +254,8 @@
(descr, vs, T_names, prefix, (names, auxnames), (Ts, Us))
end;
-fun get_constrs thy nesting_pref T_name =
- try (the_spec thy nesting_pref) T_name
+fun get_constrs thy T_name =
+ try (the_spec thy) T_name
|> Option.map (fn (tfrees, ctrs) =>
let
fun varify_tfree (s, S) = TVar ((s, 0), S);
--- a/src/HOL/ex/Refute_Examples.thy Mon Sep 01 16:34:40 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Mon Sep 01 17:34:03 2014 +0200
@@ -609,7 +609,7 @@
text {* Non-recursive datatypes *}
-datatype T1 = A | B
+datatype_new T1 = A | B
lemma "P (x::T1)"
refute [expect = genuine]
@@ -643,7 +643,7 @@
refute [expect = genuine]
oops
-datatype 'a T2 = C T1 | D 'a
+datatype_new 'a T2 = C T1 | D 'a
lemma "P (x::'a T2)"
refute [expect = genuine]
@@ -673,7 +673,7 @@
refute [expect = genuine]
oops
-datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
+datatype_new ('a,'b) T3 = E "'a \<Rightarrow> 'b"
lemma "P (x::('a,'b) T3)"
refute [expect = genuine]
@@ -776,7 +776,7 @@
refute [expect = potential]
oops
-datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
+datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
lemma "P (x::BitList)"
refute [expect = potential]
@@ -806,7 +806,7 @@
refute [expect = potential]
oops
-datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
+datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
lemma "P (x::'a BinTree)"
refute [expect = potential]
@@ -842,8 +842,9 @@
text {* Mutually recursive datatypes *}
-datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
- and 'a bexp = Equal "'a aexp" "'a aexp"
+datatype_new
+ 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and
+ 'a bexp = Equal "'a aexp" "'a aexp"
lemma "P (x::'a aexp)"
refute [expect = potential]
@@ -865,15 +866,15 @@
refute [expect = potential]
oops
-lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
+lemma "rec_aexp number ite equal (Number x) = number x"
refute [maxsize = 1, expect = none]
by simp
-lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
+lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
refute [maxsize = 1, expect = none]
by simp
-lemma "P (rec_aexp_bexp_1 number ite equal x)"
+lemma "P (rec_aexp number ite equal x)"
refute [expect = potential]
oops
@@ -881,11 +882,11 @@
refute [expect = potential]
oops
-lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
+lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
refute [maxsize = 1, expect = none]
by simp
-lemma "P (rec_aexp_bexp_2 number ite equal x)"
+lemma "P (rec_bexp number ite equal x)"
refute [expect = potential]
oops
@@ -893,8 +894,9 @@
refute [expect = potential]
oops
-datatype X = A | B X | C Y
- and Y = D X | E Y | F
+datatype_new
+ X = A | B X | C Y and
+ Y = D X | E Y | F
lemma "P (x::X)"
refute [expect = potential]
@@ -940,35 +942,35 @@
refute [expect = potential]
oops
-lemma "rec_X_Y_1 a b c d e f A = a"
+lemma "rec_X a b c d e f A = a"
refute [maxsize = 3, expect = none]
by simp
-lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
+lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
refute [maxsize = 1, expect = none]
by simp
-lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
+lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
refute [maxsize = 1, expect = none]
by simp
-lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
+lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
refute [maxsize = 1, expect = none]
by simp
-lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)"
+lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
refute [maxsize = 1, expect = none]
by simp
-lemma "rec_X_Y_2 a b c d e f F = f"
+lemma "rec_Y a b c d e f F = f"
refute [maxsize = 3, expect = none]
by simp
-lemma "P (rec_X_Y_1 a b c d e f x)"
+lemma "P (rec_X a b c d e f x)"
refute [expect = potential]
oops
-lemma "P (rec_X_Y_2 a b c d e f y)"
+lemma "P (rec_Y a b c d e f y)"
refute [expect = potential]
oops
@@ -1060,7 +1062,11 @@
refute [expect = potential]
oops
-datatype Trie = TR "Trie list"
+datatype_new Trie = TR "Trie list"
+datatype_compat Trie
+
+abbreviation "rec_Trie_1 \<equiv> compat_Trie.n2m_Trie_rec"
+abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.n2m_Trie_list_rec"
lemma "P (x::Trie)"
refute [expect = potential]
@@ -1241,19 +1247,6 @@
refute
oops
-inductive_set
- even :: "nat set"
- and odd :: "nat set"
-where
- "0 : even"
-| "n : even \<Longrightarrow> Suc n : odd"
-| "n : odd \<Longrightarrow> Suc n : even"
-
-lemma "n : odd"
-(* refute *) (* TODO: there seems to be an issue here with undefined terms
- because of the recursive datatype "nat" *)
-oops
-
consts f :: "'a \<Rightarrow> 'a"
inductive_set