# HG changeset patch
# User blanchet
# Date 1409585643 -7200
# Node ID 3ec65a7f2b50c21225ba338310eac0fbfbac7843
# Parent  43a1ba26a8cbdf197569a18d01515d29ceec1492
ported Refute to use new datatypes when possible

diff -r 43a1ba26a8cb -r 3ec65a7f2b50 src/HOL/Library/refute.ML
--- 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
diff -r 43a1ba26a8cb -r 3ec65a7f2b50 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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);
diff -r 43a1ba26a8cb -r 3ec65a7f2b50 src/HOL/ex/Refute_Examples.thy
--- 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