ported Refute to use new datatypes when possible
authorblanchet
Mon Sep 01 17:34:03 2014 +0200 (2014-09-01)
changeset 581293ec65a7f2b50
parent 58128 43a1ba26a8cb
child 58130 5e9170812356
ported Refute to use new datatypes when possible
src/HOL/Library/refute.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Library/refute.ML	Mon Sep 01 16:34:40 2014 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Mon Sep 01 17:34:03 2014 +0200
     1.3 @@ -402,7 +402,7 @@
     1.4  fun is_IDT_constructor thy (s, T) =
     1.5    (case body_type T of
     1.6      Type (s', _) =>
     1.7 -      (case Old_Datatype_Data.get_constrs thy s' of
     1.8 +      (case BNF_LFP_Compat.get_constrs thy s' of
     1.9          SOME constrs =>
    1.10            List.exists (fn (cname, cty) =>
    1.11              cname = s andalso Sign.typ_instance thy (T, cty)) constrs
    1.12 @@ -417,7 +417,7 @@
    1.13  fun is_IDT_recursor thy (s, _) =
    1.14    let
    1.15      val rec_names = Symtab.fold (append o #rec_names o snd)
    1.16 -      (Old_Datatype_Data.get_all thy) []
    1.17 +      (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) []
    1.18    in
    1.19      (* I'm not quite sure if checking the name 's' is sufficient, *)
    1.20      (* or if we should also check the type 'T'.                   *)
    1.21 @@ -643,7 +643,6 @@
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt
    1.24      val _ = tracing "Adding axioms..."
    1.25 -    val axioms = Theory.all_axioms_of thy
    1.26      fun collect_this_axiom (axname, ax) axs =
    1.27        let
    1.28          val ax' = unfold_defs thy ax
    1.29 @@ -691,7 +690,7 @@
    1.30        (* axiomatic type classes *)
    1.31        | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    1.32        | Type (s, Ts) =>
    1.33 -        (case Old_Datatype_Data.get_info thy s of
    1.34 +        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.35            SOME _ =>  (* inductive datatype *)
    1.36              (* only collect relevant type axioms for the argument types *)
    1.37              fold collect_type_axioms Ts axs
    1.38 @@ -820,7 +819,7 @@
    1.39        | Type (@{type_name prop}, []) => acc
    1.40        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    1.41        | Type (s, Ts) =>
    1.42 -          (case Old_Datatype_Data.get_info thy s of
    1.43 +          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.44              SOME info =>  (* inductive datatype *)
    1.45                let
    1.46                  val index = #index info
    1.47 @@ -1015,7 +1014,7 @@
    1.48          (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
    1.49          val maybe_spurious = Library.exists (fn
    1.50              Type (s, _) =>
    1.51 -              (case Old_Datatype_Data.get_info thy s of
    1.52 +              (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.53                  SOME info =>  (* inductive datatype *)
    1.54                    let
    1.55                      val index           = #index info
    1.56 @@ -1741,7 +1740,7 @@
    1.57      val thy = Proof_Context.theory_of ctxt
    1.58      val (typs, terms) = model
    1.59      fun interpret_term (Type (s, Ts)) =
    1.60 -          (case Old_Datatype_Data.get_info thy s of
    1.61 +          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.62              SOME info =>  (* inductive datatype *)
    1.63                let
    1.64                  (* only recursive IDTs have an associated depth *)
    1.65 @@ -1866,7 +1865,7 @@
    1.66                  HOLogic_empty_set) pairss
    1.67              end
    1.68        | Type (s, Ts) =>
    1.69 -          (case Old_Datatype_Data.get_info thy s of
    1.70 +          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.71              SOME info =>
    1.72                (case AList.lookup (op =) typs T of
    1.73                  SOME 0 =>
    1.74 @@ -1932,7 +1931,7 @@
    1.75            Const (s, T) =>
    1.76              (case body_type T of
    1.77                Type (s', Ts') =>
    1.78 -                (case Old_Datatype_Data.get_info thy s' of
    1.79 +                (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s' of
    1.80                    SOME info =>  (* body type is an inductive datatype *)
    1.81                      let
    1.82                        val index               = #index info
    1.83 @@ -2404,7 +2403,7 @@
    1.84                  end
    1.85                else
    1.86                  NONE  (* not a recursion operator of this datatype *)
    1.87 -          ) (Old_Datatype_Data.get_all thy) NONE
    1.88 +          ) (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) NONE
    1.89      | _ =>  (* head of term is not a constant *)
    1.90        NONE
    1.91    end;
    1.92 @@ -2838,7 +2837,7 @@
    1.93    in
    1.94      (case T of
    1.95        Type (s, Ts) =>
    1.96 -        (case Old_Datatype_Data.get_info thy s of
    1.97 +        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    1.98            SOME info =>  (* inductive datatype *)
    1.99              let
   1.100                val (typs, _)           = model
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 16:34:40 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 01 17:34:03 2014 +0200
     2.3 @@ -15,12 +15,11 @@
     2.4    val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
     2.5    val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
     2.6    val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
     2.7 -  val the_spec: theory -> nesting_preference -> string ->
     2.8 -    (string * sort) list * (string * typ list) list
     2.9 +  val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
    2.10    val the_descr: theory -> nesting_preference -> string list ->
    2.11      Old_Datatype_Aux.descr * (string * sort) list * string list * string
    2.12      * (string list * string list) * (typ list * typ list)
    2.13 -  val get_constrs: theory -> nesting_preference -> string -> (string * typ) list option
    2.14 +  val get_constrs: theory -> string -> (string * typ) list option
    2.15    val interpretation: nesting_preference ->
    2.16      (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
    2.17    val datatype_compat: string list -> local_theory -> local_theory
    2.18 @@ -178,7 +177,9 @@
    2.19        #5 (mk_infos_of_mutually_recursive_new_datatypes nesting_pref false subset [fpT_name] lthy);
    2.20    in
    2.21      infos_of nesting_pref
    2.22 -    handle ERROR _ => if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else []
    2.23 +    handle ERROR _ =>
    2.24 +      (if nesting_pref = Unfold_Nesting then infos_of Keep_Nesting else [])
    2.25 +      handle ERROR _ => []
    2.26    end;
    2.27  
    2.28  fun get_all thy nesting_pref =
    2.29 @@ -213,13 +214,13 @@
    2.30      SOME info => info
    2.31    | NONE => error ("Unknown datatype " ^ quote T_name));
    2.32  
    2.33 -fun the_spec thy nesting_pref T_name =
    2.34 +fun the_spec thy T_name =
    2.35    let
    2.36 -    val {descr, index, ...} = the_info thy nesting_pref T_name;
    2.37 +    val {descr, index, ...} = the_info thy Keep_Nesting T_name;
    2.38      val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
    2.39 -    val Ts = map Old_Datatype_Aux.dest_DtTFree Ds;
    2.40 +    val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
    2.41      val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
    2.42 -  in (Ts, ctrs) end;
    2.43 +  in (tfrees, ctrs) end;
    2.44  
    2.45  fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
    2.46    let
    2.47 @@ -253,8 +254,8 @@
    2.48      (descr, vs, T_names, prefix, (names, auxnames), (Ts, Us))
    2.49    end;
    2.50  
    2.51 -fun get_constrs thy nesting_pref T_name =
    2.52 -  try (the_spec thy nesting_pref) T_name
    2.53 +fun get_constrs thy T_name =
    2.54 +  try (the_spec thy) T_name
    2.55    |> Option.map (fn (tfrees, ctrs) =>
    2.56      let
    2.57        fun varify_tfree (s, S) = TVar ((s, 0), S);
     3.1 --- a/src/HOL/ex/Refute_Examples.thy	Mon Sep 01 16:34:40 2014 +0200
     3.2 +++ b/src/HOL/ex/Refute_Examples.thy	Mon Sep 01 17:34:03 2014 +0200
     3.3 @@ -609,7 +609,7 @@
     3.4  
     3.5  text {* Non-recursive datatypes *}
     3.6  
     3.7 -datatype T1 = A | B
     3.8 +datatype_new T1 = A | B
     3.9  
    3.10  lemma "P (x::T1)"
    3.11  refute [expect = genuine]
    3.12 @@ -643,7 +643,7 @@
    3.13  refute [expect = genuine]
    3.14  oops
    3.15  
    3.16 -datatype 'a T2 = C T1 | D 'a
    3.17 +datatype_new 'a T2 = C T1 | D 'a
    3.18  
    3.19  lemma "P (x::'a T2)"
    3.20  refute [expect = genuine]
    3.21 @@ -673,7 +673,7 @@
    3.22  refute [expect = genuine]
    3.23  oops
    3.24  
    3.25 -datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
    3.26 +datatype_new ('a,'b) T3 = E "'a \<Rightarrow> 'b"
    3.27  
    3.28  lemma "P (x::('a,'b) T3)"
    3.29  refute [expect = genuine]
    3.30 @@ -776,7 +776,7 @@
    3.31  refute [expect = potential]
    3.32  oops
    3.33  
    3.34 -datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
    3.35 +datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
    3.36  
    3.37  lemma "P (x::BitList)"
    3.38  refute [expect = potential]
    3.39 @@ -806,7 +806,7 @@
    3.40  refute [expect = potential]
    3.41  oops
    3.42  
    3.43 -datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
    3.44 +datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
    3.45  
    3.46  lemma "P (x::'a BinTree)"
    3.47  refute [expect = potential]
    3.48 @@ -842,8 +842,9 @@
    3.49  
    3.50  text {* Mutually recursive datatypes *}
    3.51  
    3.52 -datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
    3.53 -     and 'a bexp = Equal "'a aexp" "'a aexp"
    3.54 +datatype_new
    3.55 +  'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and
    3.56 +  'a bexp = Equal "'a aexp" "'a aexp"
    3.57  
    3.58  lemma "P (x::'a aexp)"
    3.59  refute [expect = potential]
    3.60 @@ -865,15 +866,15 @@
    3.61  refute [expect = potential]
    3.62  oops
    3.63  
    3.64 -lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
    3.65 +lemma "rec_aexp number ite equal (Number x) = number x"
    3.66  refute [maxsize = 1, expect = none]
    3.67  by simp
    3.68  
    3.69 -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)"
    3.70 +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)"
    3.71  refute [maxsize = 1, expect = none]
    3.72  by simp
    3.73  
    3.74 -lemma "P (rec_aexp_bexp_1 number ite equal x)"
    3.75 +lemma "P (rec_aexp number ite equal x)"
    3.76  refute [expect = potential]
    3.77  oops
    3.78  
    3.79 @@ -881,11 +882,11 @@
    3.80  refute [expect = potential]
    3.81  oops
    3.82  
    3.83 -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)"
    3.84 +lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
    3.85  refute [maxsize = 1, expect = none]
    3.86  by simp
    3.87  
    3.88 -lemma "P (rec_aexp_bexp_2 number ite equal x)"
    3.89 +lemma "P (rec_bexp number ite equal x)"
    3.90  refute [expect = potential]
    3.91  oops
    3.92  
    3.93 @@ -893,8 +894,9 @@
    3.94  refute [expect = potential]
    3.95  oops
    3.96  
    3.97 -datatype X = A | B X | C Y
    3.98 -     and Y = D X | E Y | F
    3.99 +datatype_new
   3.100 +  X = A | B X | C Y and
   3.101 +  Y = D X | E Y | F
   3.102  
   3.103  lemma "P (x::X)"
   3.104  refute [expect = potential]
   3.105 @@ -940,35 +942,35 @@
   3.106  refute [expect = potential]
   3.107  oops
   3.108  
   3.109 -lemma "rec_X_Y_1 a b c d e f A = a"
   3.110 +lemma "rec_X a b c d e f A = a"
   3.111  refute [maxsize = 3, expect = none]
   3.112  by simp
   3.113  
   3.114 -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)"
   3.115 +lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
   3.116  refute [maxsize = 1, expect = none]
   3.117  by simp
   3.118  
   3.119 -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)"
   3.120 +lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
   3.121  refute [maxsize = 1, expect = none]
   3.122  by simp
   3.123  
   3.124 -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)"
   3.125 +lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
   3.126  refute [maxsize = 1, expect = none]
   3.127  by simp
   3.128  
   3.129 -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)"
   3.130 +lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
   3.131  refute [maxsize = 1, expect = none]
   3.132  by simp
   3.133  
   3.134 -lemma "rec_X_Y_2 a b c d e f F = f"
   3.135 +lemma "rec_Y a b c d e f F = f"
   3.136  refute [maxsize = 3, expect = none]
   3.137  by simp
   3.138  
   3.139 -lemma "P (rec_X_Y_1 a b c d e f x)"
   3.140 +lemma "P (rec_X a b c d e f x)"
   3.141  refute [expect = potential]
   3.142  oops
   3.143  
   3.144 -lemma "P (rec_X_Y_2 a b c d e f y)"
   3.145 +lemma "P (rec_Y a b c d e f y)"
   3.146  refute [expect = potential]
   3.147  oops
   3.148  
   3.149 @@ -1060,7 +1062,11 @@
   3.150  refute [expect = potential]
   3.151  oops
   3.152  
   3.153 -datatype Trie = TR "Trie list"
   3.154 +datatype_new Trie = TR "Trie list"
   3.155 +datatype_compat Trie
   3.156 +
   3.157 +abbreviation "rec_Trie_1 \<equiv> compat_Trie.n2m_Trie_rec"
   3.158 +abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.n2m_Trie_list_rec"
   3.159  
   3.160  lemma "P (x::Trie)"
   3.161  refute [expect = potential]
   3.162 @@ -1241,19 +1247,6 @@
   3.163  refute
   3.164  oops
   3.165  
   3.166 -inductive_set
   3.167 -  even :: "nat set"
   3.168 -  and odd  :: "nat set"
   3.169 -where
   3.170 -  "0 : even"
   3.171 -| "n : even \<Longrightarrow> Suc n : odd"
   3.172 -| "n : odd \<Longrightarrow> Suc n : even"
   3.173 -
   3.174 -lemma "n : odd"
   3.175 -(* refute *)  (* TODO: there seems to be an issue here with undefined terms
   3.176 -                       because of the recursive datatype "nat" *)
   3.177 -oops
   3.178 -
   3.179  consts f :: "'a \<Rightarrow> 'a"
   3.180  
   3.181  inductive_set