# HG changeset patch
# User wenzelm
# Date 1127165031 -7200
# Node ID 714c95aab8bc742da64029741f492a2cf0a7294b
# Parent  2bd5a6e26e1e350b50dd18ecaa013f98ca316865
shrink: compress terms and types;
prefer member/insert over polymorphic mem/ins;

diff -r 2bd5a6e26e1e -r 714c95aab8bc src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Sep 19 23:22:51 2005 +0200
+++ b/src/Pure/proofterm.ML	Mon Sep 19 23:23:51 2005 +0200
@@ -145,7 +145,7 @@
       | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
           case Symtab.lookup thms name of
             NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras)
-          | SOME ps => if prop mem ps then tabs else
+          | SOME ps => if member (op =) ps prop then tabs else
               oras_of prf (Symtab.update (name, prop::ps) thms, oras))
       | oras_of (Oracle (s, prop, _)) =
           apsnd (OrdList.insert string_term_ord (s, prop))
@@ -375,17 +375,17 @@
   | prf_loose_Pbvar1 _ _ = false;
 
 fun prf_add_loose_bnos plev tlev (PBound i) (is, js) =
-      if i < plev then (is, js) else ((i-plev) ins is, js)
+      if i < plev then (is, js) else (insert (op =) (i-plev) is, js)
   | prf_add_loose_bnos plev tlev (prf1 %% prf2) p =
       prf_add_loose_bnos plev tlev prf2
         (prf_add_loose_bnos plev tlev prf1 p)
   | prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
       prf_add_loose_bnos plev tlev prf (case opt of
-          NONE => (is, ~1 ins js)
+          NONE => (is, insert (op =) ~1 js)
         | SOME t => (is, add_loose_bnos (t, tlev, js)))
   | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
       prf_add_loose_bnos (plev+1) tlev prf (case opt of
-          NONE => (is, ~1 ins js)
+          NONE => (is, insert (op =) ~1 js)
         | SOME t => (is, add_loose_bnos (t, tlev, js)))
   | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
       prf_add_loose_bnos plev (tlev+1) prf p
@@ -784,12 +784,11 @@
 
 (***** axioms and theorems *****)
 
-fun vars_of t = rev (fold_aterms
-  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
+fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
 
 fun test_args _ [] = true
   | test_args is (Bound i :: ts) =
-      not (i mem is) andalso test_args (i :: is) ts
+      not (member (op =) is i) andalso test_args (i :: is) ts
   | test_args _ _ = false;
 
 fun is_fun (Type ("fun", _)) = true
@@ -841,7 +840,7 @@
   let
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
-        if ixn mem nvs then SOME v else NONE) (vars_of prop) @
+        if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
       map SOME (sort Term.term_ord (term_frees prop));
   in
     proof_combt' (c (name, prop, NONE), args)
@@ -855,55 +854,62 @@
   if !proofs = 0 then Oracle (name, dummy, NONE)
   else gen_axm_proof Oracle name prop;
 
-fun shrink ls lev (prf as Abst (a, T, body)) =
-      let val (b, is, ch, body') = shrink ls (lev+1) body
-      in (b, is, ch, if ch then Abst (a, T, body') else prf) end
-  | shrink ls lev (prf as AbsP (a, t, body)) =
-      let val (b, is, ch, body') = shrink (lev::ls) lev body
-      in (b orelse 0 mem is, List.mapPartial (fn 0 => NONE | i => SOME (i-1)) is,
-        ch, if ch then AbsP (a, t, body') else prf)
-      end
-  | shrink ls lev prf =
-      let val (is, ch, _, prf') = shrink' ls lev [] [] prf
-      in (false, is, ch, prf') end
-and shrink' ls lev ts prfs (prf as prf1 %% prf2) =
-      let
-        val p as (_, is', ch', prf') = shrink ls lev prf2;
-        val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
-      in (is union is', ch orelse ch', ts',
-          if ch orelse ch' then prf'' %% prf' else prf)
-      end
-  | shrink' ls lev ts prfs (prf as prf1 % t) =
-      let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
-      in (is, ch orelse ch', ts', if ch orelse ch' then prf' % t' else prf) end
-  | shrink' ls lev ts prfs (prf as PBound i) =
-      (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
-         orelse not (null (duplicates
-           (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))))
-         orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
-  | shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf)
-  | shrink' ls lev ts prfs (prf as MinProof _) =
-      ([], false, map (pair false) ts, prf)
-  | shrink' ls lev ts prfs prf =
-      let
-        val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
-          | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
-        val vs = vars_of prop;
-        val (ts', ts'') = splitAt (length vs, ts)
-        val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
-        val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
-          ixn ins (case AList.lookup (op =) insts ixn of
-              SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
-            | _ => ixns union ixns'))
-              (needed prop ts'' prfs, add_npvars false true [] ([], prop));
-        val insts' = map
-          (fn (ixn, x as SOME _) => if ixn mem nvs then (false, x) else (true, NONE)
-            | (_, x) => (false, x)) insts
-      in ([], false, insts' @ map (pair false) ts'', prf) end
-and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
-      (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
-  | needed (Var (ixn, _)) (_::_) _ = [ixn]
-  | needed _ _ _ = [];
+fun shrink_proof thy =
+  let
+    val compress_typ = Compress.typ thy;
+    val compress_term = Compress.term thy;
+  
+    fun shrink ls lev (prf as Abst (a, T, body)) =
+          let val (b, is, ch, body') = shrink ls (lev+1) body
+          in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end
+      | shrink ls lev (prf as AbsP (a, t, body)) =
+          let val (b, is, ch, body') = shrink (lev::ls) lev body
+          in (b orelse member (op =) is 0, List.mapPartial (fn 0 => NONE | i => SOME (i-1)) is,
+            ch, if ch then AbsP (a, Option.map compress_term t, body') else prf)
+          end
+      | shrink ls lev prf =
+          let val (is, ch, _, prf') = shrink' ls lev [] [] prf
+          in (false, is, ch, prf') end
+    and shrink' ls lev ts prfs (prf as prf1 %% prf2) =
+          let
+            val p as (_, is', ch', prf') = shrink ls lev prf2;
+            val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1
+          in (is union is', ch orelse ch', ts',
+              if ch orelse ch' then prf'' %% prf' else prf)
+          end
+      | shrink' ls lev ts prfs (prf as prf1 % t) =
+          let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
+          in (is, ch orelse ch', ts',
+              if ch orelse ch' then prf' % Option.map compress_term t' else prf) end
+      | shrink' ls lev ts prfs (prf as PBound i) =
+          (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
+             orelse not (null (duplicates
+               (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))))
+             orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
+      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (compress_term t))
+      | shrink' ls lev ts prfs (prf as MinProof _) =
+          ([], false, map (pair false) ts, prf)
+      | shrink' ls lev ts prfs prf =
+          let
+            val prop = (case prf of PThm (_, _, prop, _) => prop | PAxm (_, prop, _) => prop
+              | Oracle (_, prop, _) => prop | _ => error "shrink: proof not in normal form");
+            val vs = vars_of prop;
+            val (ts', ts'') = splitAt (length vs, ts)
+            val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
+            val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
+              insert (op =) ixn (case AList.lookup (op =) insts ixn of
+                  SOME (SOME t) => if is_proj t then ixns union ixns' else ixns'
+                | _ => ixns union ixns'))
+                  (needed prop ts'' prfs, add_npvars false true [] ([], prop));
+            val insts' = map
+              (fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE)
+                | (_, x) => (false, x)) insts
+          in ([], false, insts' @ map (pair false) ts'', prf) end
+    and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) =
+          (if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs
+      | needed (Var (ixn, _)) (_::_) _ = [ixn]
+      | needed _ _ _ = [];
+  in shrink end;
 
 
 (**** Simple first order matching functions for terms and proofs ****)
@@ -1145,10 +1151,10 @@
     val prop = Logic.list_implies (hyps, prop);
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
-        if ixn mem nvs then SOME v else NONE) (vars_of prop) @
+        if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
       map SOME (sort Term.term_ord (term_frees prop));
     val opt_prf = if ! proofs = 2 then
-        #4 (shrink [] 0 (rewrite_prf fst (ProofData.get thy)
+        #4 (shrink_proof thy [] 0 (rewrite_prf fst (ProofData.get thy)
           (foldr (uncurry implies_intr_proof) prf hyps)))
       else MinProof (mk_min_proof prf ([], [], []));
     val head = (case strip_combt (fst (strip_combP prf)) of