# HG changeset patch # User webertj # Date 1192406270 -7200 # Node ID f7095d7cb9a339b410c746e4ec9186db48fbcb56 # Parent 4d1271cc42eaaf0d24474064def843238c1b52a3 interpreter for List.append added again diff -r 4d1271cc42ea -r f7095d7cb9a3 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Mon Oct 15 01:36:22 2007 +0200 +++ b/src/HOL/Tools/refute.ML Mon Oct 15 01:57:50 2007 +0200 @@ -705,7 +705,7 @@ Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t - (*| Const ("List.", _) => t*) + | Const ("List.append", _) => t | Const ("Lfp.lfp", _) => t | Const ("Gfp.gfp", _) => t | Const ("fst", _) => t @@ -896,7 +896,7 @@ | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []), Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => collect_type_axioms (axs, T) - (*| Const ("List.append", T) => collect_type_axioms (axs, T)*) + | Const ("List.append", T) => collect_type_axioms (axs, T) | Const ("Lfp.lfp", T) => collect_type_axioms (axs, T) | Const ("Gfp.gfp", T) => collect_type_axioms (axs, T) | Const ("fst", T) => collect_type_axioms (axs, T) @@ -2838,13 +2838,13 @@ (* int -> int -> interpretation *) fun plus m n = let - val element = (m+n)+1 + val element = m + n in - if element > size_of_nat then + if element > size_of_nat - 1 then Leaf (replicate size_of_nat False) else - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_of_nat - element) False)) + Leaf ((replicate element False) @ True :: + (replicate (size_of_nat - element - 1) False)) end in SOME (Node (map (fn m => Node (map (plus m) (0 upto size_of_nat-1))) @@ -2869,10 +2869,10 @@ (* int -> int -> interpretation *) fun minus m n = let - val element = Int.max (m-n, 0) + 1 + val element = Int.max (m-n, 0) in - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_of_nat - element) False)) + Leaf ((replicate element False) @ True :: + (replicate (size_of_nat - element - 1) False)) end in SOME (Node (map (fn m => Node (map (minus m) (0 upto size_of_nat-1))) @@ -2897,13 +2897,13 @@ (* nat -> nat -> interpretation *) fun mult m n = let - val element = (m*n)+1 + val element = m * n in - if element > size_of_nat then + if element > size_of_nat - 1 then Leaf (replicate size_of_nat False) else - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_of_nat - element) False)) + Leaf ((replicate element False) @ True :: + (replicate (size_of_nat - element - 1) False)) end in SOME (Node (map (fn m => Node (map (mult m) (0 upto size_of_nat-1))) @@ -2919,47 +2919,92 @@ (* interpreters available already (using its definition), but the code *) (* below is more efficient *) -(* TODO: invalidated by the change in the order in which we enumerate elements - of recursive datatypes fun List_append_interpreter thy model args t = case t of Const ("List.append", Type ("fun", [Type ("List.list", [T]), Type ("fun", [Type ("List.list", [_]), Type ("List.list", [_])])])) => let - val size_elem = size_of_type thy model T - val size_list = size_of_type thy model (Type ("List.list", [T])) - (* log (a, b) computes floor(log_a(b)), i.e. the largest integer x *) - (* s.t. a^x <= b, for a>=2, b>=1 *) - (* int * int -> int *) - fun log (a, b) = + val size_elem = size_of_type thy model T + val size_list = size_of_type thy model (Type ("List.list", [T])) + (* maximal length of lists; 0 if we only consider the empty list *) + val list_length = let + (* int -> int -> int -> int *) + fun list_length_acc len lists total = + if lists = total then + len + else if lists < total then + list_length_acc (len+1) (lists*size_elem) (total-lists) + else + raise REFUTE ("List_append_interpreter", + "size_list not equal to 1 + size_elem + ... + " ^ + "size_elem^len, for some len") + in + list_length_acc 0 1 size_list + end + val elements = 0 upto (size_list-1) + (* FIXME: there should be a nice formula, which computes the same as *) + (* the following, but without all this intermediate tree *) + (* length/offset stuff *) + (* associate each list with its length and offset in a complete tree *) + (* of width 'size_elem' and depth 'length_list' (with 'size_list' *) + (* nodes total) *) + (* (int * (int * int)) list *) + val (_, lenoff_lists) = foldl_map (fn ((offsets, off), elem) => + (* corresponds to a pre-order traversal of the tree *) let - fun logloop (ax, x) = - if ax > b then x-1 else logloop (a * ax, x+1) + val len = length offsets + (* associate the given element with len/off *) + val assoc = (elem, (len, off)) in - logloop (1, 0) - end + if len < list_length then + (* go to first child node *) + ((off :: offsets, off * size_elem), assoc) + else if off mod size_elem < size_elem - 1 then + (* go to next sibling node *) + ((offsets, off + 1), assoc) + else + (* go back up the stack until we find a level where we can go *) + (* to the next sibling node *) + let + val offsets' = Library.dropwhile + (fn off' => off' mod size_elem = size_elem - 1) offsets + in + case offsets' of + [] => + (* we're at the last node in the tree; the next value *) + (* won't be used anyway *) + (([], 0), assoc) + | off'::offs' => + (* go to next sibling node *) + ((offs', off' + 1), assoc) + end + end) (([], 0), elements) + (* we also need the reverse association (from length/offset to *) + (* index) *) + val lenoff'_lists = map Library.swap lenoff_lists + (* returns the interpretation for "(list no. m) @ (list no. n)" *) (* nat -> nat -> interpretation *) fun append m n = let - (* The following formula depends on the order in which lists are *) - (* enumerated by the 'IDT_constructor_interpreter'. It took me *) - (* a little while to come up with this formula. *) - val element = n + m * (if size_elem = 1 then 1 - else power (size_elem, log (size_elem, n+1))) + 1 + val (len_m, off_m) = lookup lenoff_lists m + val (len_n, off_n) = lookup lenoff_lists n + val len_elem = len_m + len_n + val off_elem = off_m * power (size_elem, len_n) + off_n in - if element > size_list then + case AList.lookup op= lenoff'_lists (len_elem, off_elem) of + NONE => + (* undefined *) Leaf (replicate size_list False) - else - Leaf ((replicate (element-1) False) @ True :: - (replicate (size_list - element) False)) + | SOME element => + Leaf ((replicate element False) @ True :: + (replicate (size_list - element - 1) False)) end in - SOME (Node (map (fn m => Node (map (append m) (0 upto size_list-1))) - (0 upto size_list-1)), model, args) + SOME (Node (map (fn m => Node (map (append m) elements)) elements), + model, args) end | _ => NONE; -*) (* theory -> model -> arguments -> Term.term -> (interpretation * model * arguments) option *) @@ -3343,7 +3388,7 @@ add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> add_interpreter "Nat_HOL.times" Nat_times_interpreter #> - (*add_interpreter "List.append" List_append_interpreter #>*) + add_interpreter "List.append" List_append_interpreter #> add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #> add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #> add_interpreter "fst" Product_Type_fst_interpreter #> diff -r 4d1271cc42ea -r f7095d7cb9a3 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Mon Oct 15 01:36:22 2007 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Mon Oct 15 01:57:50 2007 +0200 @@ -1400,7 +1400,6 @@ refute oops -(* TODO: an efficient interpreter for @ is needed here lemma "xs @ [] = ys @ []" refute oops @@ -1408,7 +1407,6 @@ lemma "xs @ ys = ys @ xs" refute oops -*) lemma "f (lfp f) = lfp f" refute