Reimplemented proof of strong induction theorem.
authorberghofe
Thu Jan 24 11:26:54 2008 +0100 (2008-01-24)
changeset 259516ebe26bfed18
parent 25950 a3067f6f08a2
child 25952 2152b47a87ed
Reimplemented proof of strong induction theorem.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Jan 24 11:23:11 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Jan 24 11:26:54 2008 +0100
     1.3 @@ -122,21 +122,6 @@
     1.4        (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
     1.5    in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
     1.6  
     1.7 -fun mk_subgoal i f st =
     1.8 -  let
     1.9 -    val cg = List.nth (cprems_of st, i - 1);
    1.10 -    val g = term_of cg;
    1.11 -    val revcut_rl' = Thm.lift_rule cg revcut_rl;
    1.12 -    val v = head_of (Logic.strip_assums_concl (hd (prems_of revcut_rl')));
    1.13 -    val ps = Logic.strip_params g;
    1.14 -    val cert = cterm_of (Thm.theory_of_thm st);
    1.15 -  in
    1.16 -    compose_tac (false,
    1.17 -      Thm.instantiate ([], [(cert v, cert (list_abs (ps,
    1.18 -        f (rev ps) (Logic.strip_assums_hyp g) (Logic.strip_assums_concl g))))])
    1.19 -      revcut_rl', 2) i st
    1.20 -  end;
    1.21 -
    1.22  (** simplification procedure for sorting permutations **)
    1.23  
    1.24  val dj_cp = thm "dj_cp";
    1.25 @@ -186,6 +171,9 @@
    1.26  val supp_def = thm "supp_def";
    1.27  val rev_simps = thms "rev.simps";
    1.28  val app_simps = thms "append.simps";
    1.29 +val at_fin_set_supp = thm "at_fin_set_supp";
    1.30 +val at_fin_set_fresh = thm "at_fin_set_fresh";
    1.31 +val abs_fun_eq1 = thm "abs_fun_eq1";
    1.32  
    1.33  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    1.34  
    1.35 @@ -204,7 +192,7 @@
    1.36    end;
    1.37  
    1.38  fun mk_not_sym ths = maps (fn th => case prop_of th of
    1.39 -    _ $ (Const ("Not", _) $ _) => [th, th RS not_sym]
    1.40 +    _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
    1.41    | _ => [th]) ths;
    1.42  
    1.43  fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
    1.44 @@ -585,6 +573,8 @@
    1.45  
    1.46      val _ = warning "proving closure under permutation...";
    1.47  
    1.48 +    val abs_perm = PureThy.get_thms thy4 (Name "abs_perm");
    1.49 +
    1.50      val perm_indnames' = List.mapPartial
    1.51        (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
    1.52        (perm_indnames ~~ descr);
    1.53 @@ -605,7 +595,7 @@
    1.54          (fn _ => EVERY (* CU: added perm_fun_def in the final tactic in order to deal with funs *)
    1.55             [indtac rep_induct [] 1,
    1.56              ALLGOALS (simp_tac (simpset_of thy4 addsimps
    1.57 -              (symmetric perm_fun_def :: PureThy.get_thms thy4 (Name ("abs_perm"))))),
    1.58 +              (symmetric perm_fun_def :: abs_perm))),
    1.59              ALLGOALS (resolve_tac rep_intrs
    1.60                 THEN_ALL_NEW (asm_full_simp_tac (simpset_of thy4 addsimps [perm_fun_def])))])),
    1.61          length new_type_names));
    1.62 @@ -885,8 +875,6 @@
    1.63  
    1.64      (** prove equations for permutation functions **)
    1.65  
    1.66 -    val abs_perm = PureThy.get_thms thy8 (Name "abs_perm"); (* FIXME *)
    1.67 -
    1.68      val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
    1.69        let val T = nth_dtyp' i
    1.70        in List.concat (map (fn (atom, perm_closed_thms) =>
    1.71 @@ -1220,153 +1208,156 @@
    1.72              (Free (tname, T))))
    1.73          (descr'' ~~ recTs ~~ tnames)));
    1.74  
    1.75 -    fun mk_ind_perm i k p l vs j =
    1.76 -      let
    1.77 -        val n = length vs;
    1.78 -        val Ts = map snd vs;
    1.79 -        val T = List.nth (Ts, i - j);
    1.80 -        val pT = NominalAtoms.mk_permT T
    1.81 -      in
    1.82 -        Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
    1.83 -          (HOLogic.pair_const T T $ Bound (l - j) $ fold_rev (mk_perm Ts)
    1.84 -            (map (mk_ind_perm i k p l vs) (j - 1 downto 0) @
    1.85 -             map Bound (n - k - 1 downto n - k - p))
    1.86 -            (Bound (i - j))) $
    1.87 -          Const ("List.list.Nil", pT)
    1.88 -      end;
    1.89 +    val fin_set_supp = map (fn Type (s, _) =>
    1.90 +      PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst")) RS
    1.91 +        at_fin_set_supp) dt_atomTs;
    1.92 +    val fin_set_fresh = map (fn Type (s, _) =>
    1.93 +      PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst")) RS
    1.94 +        at_fin_set_fresh) dt_atomTs;
    1.95 +    val pt1_atoms = map (fn Type (s, _) =>
    1.96 +      PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "1"))) dt_atomTs;
    1.97 +    val pt2_atoms = map (fn Type (s, _) =>
    1.98 +      PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs;
    1.99 +    val exists_fresh' = PureThy.get_thms thy9 (Name "exists_fresh'");
   1.100 +    val fs_atoms = PureThy.get_thms thy9 (Name "fin_supp");
   1.101 +    val abs_supp = PureThy.get_thms thy9 (Name "abs_supp");
   1.102 +    val perm_fresh_fresh = PureThy.get_thms thy9 (Name "perm_fresh_fresh");
   1.103 +    val calc_atm = PureThy.get_thms thy9 (Name "calc_atm");
   1.104 +    val fresh_atm = PureThy.get_thms thy9 (Name "fresh_atm");
   1.105 +    val fresh_left = PureThy.get_thms thy9 (Name "fresh_left");
   1.106 +    val perm_swap = PureThy.get_thms thy9 (Name "perm_swap");
   1.107  
   1.108 -    fun mk_fresh i i' j k p l is vs _ _ =
   1.109 +    fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
   1.110        let
   1.111 -        val n = length vs;
   1.112 -        val Ts = map snd vs;
   1.113 -        val T = List.nth (Ts, n - i - 1 - j);
   1.114 -        val f = the (AList.lookup op = fresh_fs T);
   1.115 -        val U = List.nth (Ts, n - i' - 1);
   1.116 -        val S = HOLogic.mk_setT T;
   1.117 -        val prms' = map Bound (n - k downto n - k - p + 1);
   1.118 -        val prms = map (mk_ind_perm (n - i) k p (n - l) (("a", T) :: vs))
   1.119 -            (j - 1 downto 0) @ prms';
   1.120 -        val bs = rev (List.mapPartial
   1.121 -          (fn ((_, T'), i) => if T = T' then SOME (Bound i) else NONE)
   1.122 -          (List.take (vs, n - k - p - 1) ~~ (1 upto n - k - p - 1)));
   1.123 -        val ts = map (fn i =>
   1.124 -          Const ("Nominal.supp", List.nth (Ts, n - i - 1) --> S) $
   1.125 -            fold_rev (mk_perm (T :: Ts)) prms' (Bound (n - i))) is
   1.126 +        val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
   1.127 +        val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
   1.128 +            (HOLogic.exists_const T $ Abs ("x", T,
   1.129 +              fresh_const T (fastype_of p) $
   1.130 +                Bound 0 $ p)))
   1.131 +          (fn _ => EVERY
   1.132 +            [resolve_tac exists_fresh' 1,
   1.133 +             simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
   1.134 +               fin_set_supp @ ths)) 1]);
   1.135 +        val (([cx], ths), ctxt') = Obtain.result
   1.136 +          (fn _ => EVERY
   1.137 +            [etac exE 1,
   1.138 +             full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
   1.139 +             REPEAT (etac conjE 1)])
   1.140 +          [ex] ctxt
   1.141 +      in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
   1.142 +
   1.143 +    fun fresh_fresh_inst thy a b =
   1.144 +      let
   1.145 +        val T = fastype_of a;
   1.146 +        val SOME th = find_first (fn th => case prop_of th of
   1.147 +            _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
   1.148 +          | _ => false) perm_fresh_fresh
   1.149        in
   1.150 -        HOLogic.mk_Trueprop (Const ("Ex", (T --> HOLogic.boolT) --> HOLogic.boolT) $
   1.151 -          Abs ("a", T, HOLogic.Not $
   1.152 -            (Const ("op :", T --> S --> HOLogic.boolT) $ Bound 0 $
   1.153 -              (foldr (fn (t, u) => Const ("insert", T --> S --> S) $ t $ u)
   1.154 -                (foldl (fn (t, u) => Const ("op Un", S --> S --> S) $ u $ t)
   1.155 -                  (f $ Bound (n - k - p))
   1.156 -                  (Const ("Nominal.supp", U --> S) $
   1.157 -                     fold_rev (mk_perm (T :: Ts)) prms (Bound (n - i')) :: ts))
   1.158 -                (fold_rev (mk_perm (T :: Ts)) prms (Bound (n - i - j)) :: bs)))))
   1.159 +        Drule.instantiate' []
   1.160 +          [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th
   1.161        end;
   1.162  
   1.163 -    fun mk_fresh_constr is p vs _ concl =
   1.164 -      let
   1.165 -        val n = length vs;
   1.166 -        val Ts = map snd vs;
   1.167 -        val _ $ (_ $ _ $ t) = concl;
   1.168 -        val c = head_of t;
   1.169 -        val T = body_type (fastype_of c);
   1.170 -        val k = foldr op + 0 (map (fn (_, i) => i + 1) is);
   1.171 -        val ps = map Bound (n - k - 1 downto n - k - p);
   1.172 -        val (_, _, ts, us) = foldl (fn ((_, i), (m, n, ts, us)) =>
   1.173 -          (m - i - 1, n - i,
   1.174 -           ts @ map Bound (n downto n - i + 1) @ [fold_rev (mk_perm Ts)
   1.175 -             (map (mk_ind_perm m k p n vs) (i - 1 downto 0) @ ps)
   1.176 -             (Bound (m - i))],
   1.177 -           us @ map (fn j => fold_rev (mk_perm Ts) ps (Bound j)) (m downto m - i)))
   1.178 -          (n - 1, n - k - p - 2, [], []) is
   1.179 -      in
   1.180 -        HOLogic.mk_Trueprop (HOLogic.eq_const T $ list_comb (c, ts) $ list_comb (c, us))
   1.181 -      end;
   1.182 -
   1.183 -    val abs_fun_finite_supp = PureThy.get_thm thy9 (Name "abs_fun_finite_supp");
   1.184 -
   1.185 -    val at_finite_select = PureThy.get_thm thy9 (Name "at_finite_select");
   1.186 -
   1.187 -    val induct_aux_lemmas = List.concat (map (fn Type (s, _) =>
   1.188 -      [PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "_inst")),
   1.189 -       PureThy.get_thm thy9 (Name ("fs_" ^ Sign.base_name s ^ "1")),
   1.190 -       PureThy.get_thm thy9 (Name ("at_" ^ Sign.base_name s ^ "_inst"))]) dt_atomTs);
   1.191 -
   1.192 -    val induct_aux_lemmas' = map (fn Type (s, _) =>
   1.193 -      PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs;
   1.194 -
   1.195 -    val fresh_aux = PureThy.get_thms thy9 (Name "fresh_aux");
   1.196 -
   1.197      (**********************************************************************
   1.198        The subgoals occurring in the proof of induct_aux have the
   1.199        following parameters:
   1.200  
   1.201 -        x_1 ... x_k p_1 ... p_m z b_1 ... b_n
   1.202 +        x_1 ... x_k p_1 ... p_m z
   1.203  
   1.204        where
   1.205  
   1.206          x_i : constructor arguments (introduced by weak induction rule)
   1.207          p_i : permutations (one for each atom type in the data type)
   1.208          z   : freshness context
   1.209 -        b_i : newly introduced names for binders (sufficiently fresh)
   1.210      ***********************************************************************)
   1.211  
   1.212      val _ = warning "proving strong induction theorem ...";
   1.213  
   1.214 -    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl'
   1.215 -      (fn prems => EVERY
   1.216 -        ([mk_subgoal 1 (K (K (K aux_ind_concl))),
   1.217 -          indtac dt_induct tnames 1] @
   1.218 -         List.concat (map (fn ((_, (_, _, constrs)), (_, constrs')) =>
   1.219 -           List.concat (map (fn ((cname, cargs), is) =>
   1.220 -             [simp_tac (HOL_basic_ss addsimps List.concat perm_simps') 1,
   1.221 -              REPEAT (rtac allI 1)] @
   1.222 -             List.concat (map
   1.223 -               (fn ((_, 0), _) => []
   1.224 -                 | ((i, j), k) => List.concat (map (fn j' =>
   1.225 +    val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn prems =>
   1.226 +      let
   1.227 +        val (prems1, prems2) = chop (length dt_atomTs) prems;
   1.228 +        val ind_ss2 = HOL_ss addsimps
   1.229 +          finite_Diff :: abs_fresh @ abs_supp @ fs_atoms;
   1.230 +        val ind_ss1 = ind_ss2 addsimps fresh_left @ calc_atm @
   1.231 +          fresh_atm @ rev_simps @ app_simps;
   1.232 +        val ind_ss3 = HOL_ss addsimps abs_fun_eq1 ::
   1.233 +          abs_perm @ calc_atm @ perm_swap;
   1.234 +        val ind_ss4 = HOL_basic_ss addsimps fresh_left @ prems1 @
   1.235 +          fin_set_fresh @ calc_atm;
   1.236 +        val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
   1.237 +        val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
   1.238 +        val th = Goal.prove (ProofContext.init thy9) [] [] aux_ind_concl
   1.239 +          (fn {context = context1, ...} =>
   1.240 +             EVERY (indtac dt_induct tnames 1 ::
   1.241 +               maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
   1.242 +                 map (fn ((cname, cargs), is) =>
   1.243 +                   REPEAT (rtac allI 1) THEN
   1.244 +                   SUBPROOF (fn {prems = iprems, params, concl,
   1.245 +                       context = context2, ...} =>
   1.246                       let
   1.247 -                       val DtType (tname, _) = List.nth (cargs, i + j');
   1.248 -                       val atom = Sign.base_name tname
   1.249 +                       val concl' = term_of concl;
   1.250 +                       val _ $ (_ $ _ $ u) = concl';
   1.251 +                       val U = fastype_of u;
   1.252 +                       val (xs, params') =
   1.253 +                         chop (length cargs) (map term_of params);
   1.254 +                       val Ts = map fastype_of xs;
   1.255 +                       val cnstr = Const (cname, Ts ---> U);
   1.256 +                       val (pis, z) = split_last params';
   1.257 +                       val mk_pi = fold_rev (mk_perm []) pis;
   1.258 +                       val xs' = partition_cargs is xs;
   1.259 +                       val xs'' = map (fn (ts, u) => (map mk_pi ts, mk_pi u)) xs';
   1.260 +                       val ts = maps (fn (ts, u) => ts @ [u]) xs'';
   1.261 +                       val (freshs1, freshs2, context3) = fold (fn t =>
   1.262 +                         let val T = fastype_of t
   1.263 +                         in obtain_fresh_name' prems1
   1.264 +                           (the (AList.lookup op = fresh_fs T) $ z :: ts) T
   1.265 +                         end) (maps fst xs') ([], [], context2);
   1.266 +                       val freshs1' = unflat (map fst xs') freshs1;
   1.267 +                       val freshs2' = map (Simplifier.simplify ind_ss4)
   1.268 +                         (mk_not_sym freshs2);
   1.269 +                       val ind_ss1' = ind_ss1 addsimps freshs2';
   1.270 +                       val ind_ss3' = ind_ss3 addsimps freshs2';
   1.271 +                       val rename_eq =
   1.272 +                         if forall (null o fst) xs' then []
   1.273 +                         else [Goal.prove context3 [] []
   1.274 +                           (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.275 +                             (list_comb (cnstr, ts),
   1.276 +                              list_comb (cnstr, maps (fn ((bs, t), cs) =>
   1.277 +                                cs @ [fold_rev (mk_perm []) (map perm_of_pair
   1.278 +                                  (bs ~~ cs)) t]) (xs'' ~~ freshs1')))))
   1.279 +                           (fn _ => EVERY
   1.280 +                              (simp_tac (HOL_ss addsimps flat inject_thms) 1 ::
   1.281 +                               REPEAT (FIRSTGOAL (rtac conjI)) ::
   1.282 +                               maps (fn ((bs, t), cs) =>
   1.283 +                                 if null bs then []
   1.284 +                                 else rtac sym 1 :: maps (fn (b, c) =>
   1.285 +                                   [rtac trans 1, rtac sym 1,
   1.286 +                                    rtac (fresh_fresh_inst thy9 b c) 1,
   1.287 +                                    simp_tac ind_ss1' 1,
   1.288 +                                    simp_tac ind_ss2 1,
   1.289 +                                    simp_tac ind_ss3' 1]) (bs ~~ cs))
   1.290 +                                 (xs'' ~~ freshs1')))];
   1.291 +                       val th = Goal.prove context3 [] [] concl' (fn _ => EVERY
   1.292 +                         [simp_tac (ind_ss6 addsimps rename_eq) 1,
   1.293 +                          cut_facts_tac iprems 1,
   1.294 +                          (resolve_tac prems THEN_ALL_NEW
   1.295 +                            SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
   1.296 +                                _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
   1.297 +                                  simp_tac ind_ss1' i
   1.298 +                              | _ $ (Const ("Not", _) $ _) =>
   1.299 +                                  resolve_tac freshs2' i
   1.300 +                              | _ => asm_simp_tac (HOL_basic_ss addsimps
   1.301 +                                  pt2_atoms addsimprocs [perm_simproc]) i)) 1])
   1.302 +                       val final = ProofContext.export context3 context2 [th]
   1.303                       in
   1.304 -                       [mk_subgoal 1 (mk_fresh i (i + j) j'
   1.305 -                          (length cargs) (length dt_atomTs)
   1.306 -                          (length cargs + length dt_atomTs + 1 + i - k)
   1.307 -                          (List.mapPartial (fn (i', j) =>
   1.308 -                             if i = i' then NONE else SOME (i' + j)) is)),
   1.309 -                        rtac at_finite_select 1,
   1.310 -                        rtac (PureThy.get_thm thy9 (Name ("at_" ^ atom ^ "_inst"))) 1,
   1.311 -                        asm_full_simp_tac (simpset_of thy9 addsimps
   1.312 -                          [PureThy.get_thm thy9 (Name ("fs_" ^ atom ^ "1"))]) 1,
   1.313 -                        resolve_tac prems 1,
   1.314 -                        etac exE 1,
   1.315 -                        asm_full_simp_tac (simpset_of thy9 addsimps
   1.316 -                          [symmetric fresh_def]) 1]
   1.317 -                     end) (0 upto j - 1))) (is ~~ (0 upto length is - 1))) @
   1.318 -             (if exists (not o equal 0 o snd) is then
   1.319 -                [mk_subgoal 1 (mk_fresh_constr is (length dt_atomTs)),
   1.320 -                 asm_full_simp_tac (simpset_of thy9 addsimps
   1.321 -                   (List.concat inject_thms @
   1.322 -                    alpha @ abs_perm @ abs_fresh @ [abs_fun_finite_supp] @
   1.323 -                    induct_aux_lemmas)) 1,
   1.324 -                 dtac sym 1,
   1.325 -                 asm_full_simp_tac (simpset_of thy9) 1,
   1.326 -                 REPEAT (etac conjE 1)]
   1.327 -              else
   1.328 -                []) @
   1.329 -             [(resolve_tac prems THEN_ALL_NEW
   1.330 -                (atac ORELSE'
   1.331 -                  SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
   1.332 -                      _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
   1.333 -                        asm_simp_tac (simpset_of thy9 addsimps fresh_aux) i
   1.334 -                    | _ =>
   1.335 -                        asm_simp_tac (simpset_of thy9
   1.336 -                        addsimps induct_aux_lemmas'
   1.337 -                        addsimprocs [perm_simproc]) i))) 1])
   1.338 -               (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @
   1.339 -         [REPEAT (eresolve_tac [conjE, allE_Nil] 1),
   1.340 -          REPEAT (etac allE 1),
   1.341 -          REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac (simpset_of thy9) 1)]));
   1.342 +                       resolve_tac final 1
   1.343 +                     end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr)))
   1.344 +      in
   1.345 +        EVERY
   1.346 +          [cut_facts_tac [th] 1,
   1.347 +           REPEAT (eresolve_tac [conjE, allE_Nil] 1),
   1.348 +           REPEAT (etac allE 1),
   1.349 +           REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
   1.350 +      end);
   1.351  
   1.352      val induct_aux' = Thm.instantiate ([],
   1.353        map (fn (s, T) =>
   1.354 @@ -1382,7 +1373,7 @@
   1.355      val induct = Goal.prove_global thy9 [] ind_prems ind_concl
   1.356        (fn prems => EVERY
   1.357           [rtac induct_aux' 1,
   1.358 -          REPEAT (resolve_tac induct_aux_lemmas 1),
   1.359 +          REPEAT (resolve_tac fs_atoms 1),
   1.360            REPEAT ((resolve_tac prems THEN_ALL_NEW
   1.361              (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
   1.362  
   1.363 @@ -1569,9 +1560,6 @@
   1.364  
   1.365      (** freshness **)
   1.366  
   1.367 -    val perm_fresh_fresh = PureThy.get_thms thy11 (Name "perm_fresh_fresh");
   1.368 -    val perm_swap = PureThy.get_thms thy11 (Name "perm_swap");
   1.369 -
   1.370      val finite_premss = map (fn aT =>
   1.371        map (fn (f, T) => HOLogic.mk_Trueprop
   1.372          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
   1.373 @@ -1636,13 +1624,6 @@
   1.374  
   1.375      (** uniqueness **)
   1.376  
   1.377 -    val exists_fresh' = PureThy.get_thms thy11 (Name "exists_fresh'");
   1.378 -    val fs_atoms = map (fn Type (s, _) => PureThy.get_thm thy11
   1.379 -      (Name ("fs_" ^ Sign.base_name s ^ "1"))) dt_atomTs;
   1.380 -    val fresh_atm = PureThy.get_thms thy11 (Name "fresh_atm");
   1.381 -    val calc_atm = PureThy.get_thms thy11 (Name "calc_atm");
   1.382 -    val fresh_left = PureThy.get_thms thy11 (Name "fresh_left");
   1.383 -
   1.384      val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
   1.385      val fun_tupleT = fastype_of fun_tuple;
   1.386      val rec_unique_frees =