Finished implementation of uniqueness proof for recursion combinator.
authorberghofe
Mon Aug 14 11:25:08 2006 +0200 (2006-08-14)
changeset 2037653b31f7c1d87
parent 20375 e91be828ce4e
child 20377 3baf326b2b5f
Finished implementation of uniqueness proof for recursion combinator.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Aug 14 11:16:20 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Aug 14 11:25:08 2006 +0200
     1.3 @@ -137,6 +137,13 @@
     1.4    |> map (standard #> RuleCases.save rule);
     1.5  
     1.6  val supp_prod = thm "supp_prod";
     1.7 +val fresh_prod = thm "fresh_prod";
     1.8 +val supports_fresh = thm "supports_fresh";
     1.9 +val supports_def = thm "Nominal.op supports_def";
    1.10 +val fresh_def = thm "fresh_def";
    1.11 +val supp_def = thm "supp_def";
    1.12 +val rev_simps = thms "rev.simps";
    1.13 +val app_simps = thms "op @.simps";
    1.14  
    1.15  fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
    1.16    let
    1.17 @@ -871,8 +878,6 @@
    1.18      val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
    1.19      val alpha = PureThy.get_thms thy8 (Name "alpha");
    1.20      val abs_fresh = PureThy.get_thms thy8 (Name "abs_fresh");
    1.21 -    val fresh_def = PureThy.get_thm thy8 (Name "fresh_def");
    1.22 -    val supp_def = PureThy.get_thm thy8 (Name "supp_def");
    1.23  
    1.24      val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
    1.25        let val T = nth_dtyp' i
    1.26 @@ -916,11 +921,6 @@
    1.27  
    1.28      (** equations for support and freshness **)
    1.29  
    1.30 -    val Un_assoc = PureThy.get_thm thy8 (Name "Un_assoc");
    1.31 -    val de_Morgan_conj = PureThy.get_thm thy8 (Name "de_Morgan_conj");
    1.32 -    val Collect_disj_eq = PureThy.get_thm thy8 (Name "Collect_disj_eq");
    1.33 -    val finite_Un = PureThy.get_thm thy8 (Name "finite_Un");
    1.34 -
    1.35      val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
    1.36        (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
    1.37        let val T = nth_dtyp' i
    1.38 @@ -1411,9 +1411,9 @@
    1.39            HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
    1.40          val prems5 = mk_fresh3 (recs ~~ frees'') frees';
    1.41          val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
    1.42 -        val rec_freshs = map (fn p as (_, T) =>
    1.43 +        val result_freshs = map (fn p as (_, T) =>
    1.44            Const ("Nominal.fresh", T --> fastype_of result --> HOLogic.boolT) $
    1.45 -            Free p $ result) (List.concat (map (fst o snd) recs));
    1.46 +            Free p $ result) (List.concat (map fst frees'));
    1.47          val P = HOLogic.mk_Trueprop (p $ result)
    1.48        in
    1.49          (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
    1.50 @@ -1421,10 +1421,10 @@
    1.51               (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), map Free frees),
    1.52                 result), rec_set)))],
    1.53           rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
    1.54 -         if null rec_freshs then rec_prems'
    1.55 +         if null result_freshs then rec_prems'
    1.56           else rec_prems' @ [list_all_free (frees @ frees'',
    1.57             Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ [P],
    1.58 -             HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_freshs)))],
    1.59 +             HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj result_freshs)))],
    1.60           l + 1)
    1.61        end;
    1.62  
    1.63 @@ -1502,13 +1502,95 @@
    1.64                 (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
    1.65        end) dt_atomTs;
    1.66  
    1.67 -    (** uniqueness **)
    1.68 +    (** freshness **)
    1.69 +
    1.70 +    val perm_fresh_fresh = PureThy.get_thms thy11 (Name "perm_fresh_fresh");
    1.71 +    val perm_swap = PureThy.get_thms thy11 (Name "perm_swap");
    1.72  
    1.73 -    val fresh_prems = List.concat (map (fn aT =>
    1.74 +    fun perm_of_pair (x, y) =
    1.75 +      let
    1.76 +        val T = fastype_of x;
    1.77 +        val pT = mk_permT T
    1.78 +      in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
    1.79 +        HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
    1.80 +      end;
    1.81 +
    1.82 +    val finite_premss = map (fn aT =>
    1.83        map (fn (f, T) => HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.84          (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f,
    1.85           Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT aT)))))
    1.86 -           (rec_fns ~~ rec_fn_Ts)) dt_atomTs);
    1.87 +           (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
    1.88 +
    1.89 +    val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
    1.90 +      let
    1.91 +        val name = Sign.base_name (fst (dest_Type aT));
    1.92 +        val fs_name = PureThy.get_thm thy11 (Name ("fs_" ^ name ^ "1"));
    1.93 +        val a = Free ("a", aT);
    1.94 +        val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
    1.95 +            (Const ("Nominal.fresh", aT --> fT --> HOLogic.boolT) $ a $ f))
    1.96 +          (rec_fns ~~ rec_fn_Ts)
    1.97 +      in
    1.98 +        map (fn (((T, U), R), eqvt_th) =>
    1.99 +          let
   1.100 +            val x = Free ("x", T);
   1.101 +            val y = Free ("y", U);
   1.102 +            val y' = Free ("y'", U)
   1.103 +          in
   1.104 +            standard (Goal.prove (Context.init_proof thy11) [] (finite_prems @
   1.105 +                [HOLogic.mk_Trueprop (HOLogic.mk_mem
   1.106 +                  (HOLogic.mk_prod (x, y), R)),
   1.107 +                 HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
   1.108 +                   HOLogic.mk_imp (HOLogic.mk_mem
   1.109 +                       (HOLogic.mk_prod (x, y'), R),
   1.110 +                     HOLogic.mk_eq (y', y)))),
   1.111 +                 HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.112 +                   aT --> T --> HOLogic.boolT) $ a $ x)] @
   1.113 +              freshs)
   1.114 +              (HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.115 +                 aT --> U --> HOLogic.boolT) $ a $ y))
   1.116 +              (fn {prems, context} =>
   1.117 +                 let
   1.118 +                   val (finite_prems, rec_prem :: unique_prem ::
   1.119 +                     fresh_prems) = chop (length finite_prems) prems;
   1.120 +                   val unique_prem' = unique_prem RS spec RS mp;
   1.121 +                   val unique = [unique_prem', unique_prem' RS sym] MRS trans;
   1.122 +                   val _ $ (_ $ (_ $ S $ _)) $ _ = prop_of supports_fresh;
   1.123 +                   val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns)
   1.124 +                 in EVERY
   1.125 +                   [rtac (Drule.cterm_instantiate
   1.126 +                      [(cterm_of thy11 S,
   1.127 +                        cterm_of thy11 (Const ("Nominal.supp",
   1.128 +                          fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
   1.129 +                      supports_fresh) 1,
   1.130 +                    simp_tac (HOL_basic_ss addsimps
   1.131 +                      [supports_def, symmetric fresh_def, fresh_prod]) 1,
   1.132 +                    REPEAT_DETERM (resolve_tac [allI, impI] 1),
   1.133 +                    REPEAT_DETERM (etac conjE 1),
   1.134 +                    rtac unique 1,
   1.135 +                    SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
   1.136 +                      [cut_facts_tac [rec_prem] 1,
   1.137 +                       rtac (Thm.instantiate ([],
   1.138 +                         [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
   1.139 +                           cterm_of thy11 (perm_of_pair (term_of a, term_of b)))]) eqvt_th) 1,
   1.140 +                       asm_simp_tac (HOL_ss addsimps
   1.141 +                         (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
   1.142 +                    rtac rec_prem 1,
   1.143 +                    simp_tac (HOL_ss addsimps (fs_name ::
   1.144 +                      supp_prod :: finite_Un :: finite_prems)) 1,
   1.145 +                    simp_tac (HOL_ss addsimps (symmetric fresh_def ::
   1.146 +                      fresh_prod :: fresh_prems)) 1]
   1.147 +                 end))
   1.148 +          end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
   1.149 +      end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss);
   1.150 +
   1.151 +    (** uniqueness **)
   1.152 +
   1.153 +    val exists_fresh = PureThy.get_thms thy11 (Name "exists_fresh");
   1.154 +    val fs_atoms = map (fn Type (s, _) => PureThy.get_thm thy11
   1.155 +      (Name ("fs_" ^ Sign.base_name s ^ "1"))) dt_atomTs;
   1.156 +    val fresh_atm = PureThy.get_thms thy11 (Name "fresh_atm");
   1.157 +    val calc_atm = PureThy.get_thms thy11 (Name "calc_atm");
   1.158 +    val fresh_left = PureThy.get_thms thy11 (Name "fresh_left");
   1.159  
   1.160      val fun_tuple = foldr1 HOLogic.mk_prod rec_fns;
   1.161      val fun_tupleT = fastype_of fun_tuple;
   1.162 @@ -1520,6 +1602,7 @@
   1.163          Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
   1.164            Abs ("y", U, HOLogic.mk_mem (HOLogic.pair_const T U $ Free x $ Bound 0, R)))
   1.165        (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
   1.166 +
   1.167      val induct_aux_rec = Drule.cterm_instantiate
   1.168        (map (pairself (cterm_of thy11))
   1.169           (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
   1.170 @@ -1532,17 +1615,38 @@
   1.171            map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
   1.172              rec_unique_frees)) induct_aux;
   1.173  
   1.174 -    val rec_unique = map standard (split_conj_thm (Goal.prove_global thy11 []
   1.175 -      (fresh_prems @ rec_prems @ rec_prems')
   1.176 +    fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
   1.177 +      let
   1.178 +        val p = foldr1 HOLogic.mk_prod (vs @ freshs1);
   1.179 +        val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
   1.180 +            (HOLogic.exists_const T $ Abs ("x", T,
   1.181 +              Const ("Nominal.fresh", T --> fastype_of p --> HOLogic.boolT) $
   1.182 +                Bound 0 $ p)))
   1.183 +          (fn _ => EVERY
   1.184 +            [cut_facts_tac ths 1,
   1.185 +             REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
   1.186 +             resolve_tac exists_fresh 1,
   1.187 +             asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
   1.188 +        val (([cx], ths), ctxt') = Obtain.result
   1.189 +          (fn _ => EVERY
   1.190 +            [etac exE 1,
   1.191 +             full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
   1.192 +             REPEAT (etac conjE 1)])
   1.193 +          [ex] ctxt
   1.194 +      in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
   1.195 +
   1.196 +    val rec_unique = map standard (split_conj_thm (Goal.prove
   1.197 +      (Context.init_proof thy11) []
   1.198 +      (List.concat finite_premss @ rec_prems @ rec_prems')
   1.199        (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))
   1.200 -      (fn ths =>
   1.201 +      (fn {prems, context} =>
   1.202           let
   1.203             val k = length rec_fns;
   1.204 -           val (finite_thss, ths1) = funpow (length dt_atomTs) (fn (xss, ys) =>
   1.205 -             apfst (curry op @ xss o single) (chop k ys)) ([], ths);
   1.206 +           val (finite_thss, ths1) = fold_map (fn T => fn xs =>
   1.207 +             apfst (pair T) (chop k xs)) dt_atomTs prems;
   1.208             val (P_ind_ths, ths2) = chop k ths1;
   1.209             val P_ths = map (fn th => th RS mp) (split_conj_thm
   1.210 -             (Goal.prove (Context.init_proof thy11)
   1.211 +             (Goal.prove context
   1.212                 (map fst (rec_unique_frees @ rec_unique_frees')) []
   1.213                 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.214                    (map (fn (((x, y), S), P) => HOLogic.mk_imp (HOLogic.mk_mem
   1.215 @@ -1550,15 +1654,262 @@
   1.216                        (rec_unique_frees ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))
   1.217                 (fn _ =>
   1.218                    rtac rec_induct 1 THEN
   1.219 -                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))))
   1.220 +                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
   1.221 +           val rec_fin_supp_thms' = map
   1.222 +             (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
   1.223 +             (rec_fin_supp_thms ~~ finite_thss);
   1.224 +           val fcbs = List.concat (map split_conj_thm ths2);
   1.225           in EVERY
   1.226             ([rtac induct_aux_rec 1] @
   1.227 -            List.concat (map (fn finite_ths =>
   1.228 +            List.concat (map (fn (_, finite_ths) =>
   1.229                [cut_facts_tac finite_ths 1,
   1.230                 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1]) finite_thss) @
   1.231 -            [ALLGOALS (full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff])),
   1.232 -             print_tac "after application of induction theorem",
   1.233 -             setmp quick_and_dirty true (SkipProof.cheat_tac thy11) (** FIXME !! **)])
   1.234 +            [ALLGOALS (EVERY'
   1.235 +               [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]),
   1.236 +                REPEAT_DETERM o eresolve_tac [conjE, ex1E],
   1.237 +                rtac ex1I,
   1.238 +                resolve_tac rec_intrs THEN_ALL_NEW atac,
   1.239 +                rotate_tac ~1,
   1.240 +                (DETERM o eresolve_tac rec_elims) THEN_ALL_NEW full_simp_tac
   1.241 +                  (HOL_ss addsimps (Pair_eq :: List.concat distinct_thms)),
   1.242 +                TRY o (etac conjE THEN' hyp_subst_tac)])] @
   1.243 +             map (fn idxs => SUBPROOF
   1.244 +               (fn {asms, concl, prems = prems', params, context = context', ...} =>
   1.245 +                  let
   1.246 +                    val (_, prem) = split_last prems';
   1.247 +                    val _ $ (_ $ lhs $ rhs) = prop_of prem;
   1.248 +                    val _ $ (_ $ lhs' $ rhs') = term_of concl;
   1.249 +                    val rT = fastype_of lhs';
   1.250 +                    val (c, cargsl) = strip_comb lhs;
   1.251 +                    val cargsl' = partition_cargs idxs cargsl;
   1.252 +                    val boundsl = List.concat (map fst cargsl');
   1.253 +                    val (_, cargsr) = strip_comb rhs;
   1.254 +                    val cargsr' = partition_cargs idxs cargsr;
   1.255 +                    val boundsr = List.concat (map fst cargsr');
   1.256 +                    val (params1, _ :: params2) =
   1.257 +                      chop (length params div 2) (map term_of params);
   1.258 +                    val params' = params1 @ params2;
   1.259 +                    val rec_prems = filter (fn th => case prop_of th of
   1.260 +                      _ $ (Const ("op :", _) $ _ $ _) => true | _ => false) prems';
   1.261 +                    val fresh_prems = filter (fn th => case prop_of th of
   1.262 +                        _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
   1.263 +                      | _ $ (Const ("Not", _) $ _) => true
   1.264 +                      | _ => false) prems';
   1.265 +                    val Ts = map fastype_of boundsl;
   1.266 +
   1.267 +                    val _ = warning "step 1: obtaining fresh names";
   1.268 +                    val (freshs1, freshs2, context'') = fold
   1.269 +                      (obtain_fresh_name (rec_fns @ params')
   1.270 +                         (List.concat (map snd finite_thss) @ rec_prems)
   1.271 +                         rec_fin_supp_thms')
   1.272 +                      Ts ([], [], context');
   1.273 +                    val pi1 = map perm_of_pair (boundsl ~~ freshs1);
   1.274 +                    val rpi1 = rev pi1;
   1.275 +                    val pi2 = map perm_of_pair (boundsr ~~ freshs1);
   1.276 +
   1.277 +                    fun mk_not_sym ths = List.concat (map (fn th =>
   1.278 +                      case prop_of th of
   1.279 +                          _ $ (Const ("Not", _) $ _) => [th, th RS not_sym]
   1.280 +                        | _ => [th]) ths);
   1.281 +                    val fresh_prems' = mk_not_sym fresh_prems;
   1.282 +                    val freshs2' = mk_not_sym freshs2;
   1.283 +
   1.284 +                    (** as, bs, cs # K as ts, K bs us **)
   1.285 +                    val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
   1.286 +                    val prove_fresh_ss = HOL_ss addsimps
   1.287 +                      (finite_Diff :: List.concat fresh_thms @
   1.288 +                       fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
   1.289 +                    (* FIXME: avoid asm_full_simp_tac ? *)
   1.290 +                    fun prove_fresh ths y x = Goal.prove context'' [] []
   1.291 +                      (HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.292 +                         fastype_of x --> fastype_of y --> HOLogic.boolT) $ x $ y))
   1.293 +                      (fn _ => cut_facts_tac ths 1 THEN asm_full_simp_tac prove_fresh_ss 1);
   1.294 +                    val constr_fresh_thms =
   1.295 +                      map (prove_fresh fresh_prems lhs) boundsl @
   1.296 +                      map (prove_fresh fresh_prems rhs) boundsr @
   1.297 +                      map (prove_fresh freshs2 lhs) freshs1 @
   1.298 +                      map (prove_fresh freshs2 rhs) freshs1;
   1.299 +
   1.300 +                    (** pi1 o (K as ts) = pi2 o (K bs us) **)
   1.301 +                    val _ = warning "step 3: pi1 o (K as ts) = pi2 o (K bs us)";
   1.302 +                    val pi1_pi2_eq = Goal.prove context'' [] []
   1.303 +                      (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.304 +                        (foldr (mk_perm []) lhs pi1, foldr (mk_perm []) rhs pi2)))
   1.305 +                      (fn _ => EVERY
   1.306 +                         [cut_facts_tac constr_fresh_thms 1,
   1.307 +                          asm_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh) 1,
   1.308 +                          rtac prem 1]);
   1.309 +
   1.310 +                    (** pi1 o ts = pi2 o us **)
   1.311 +                    val _ = warning "step 4: pi1 o ts = pi2 o us";
   1.312 +                    val pi1_pi2_eqs = map (fn (t, u) =>
   1.313 +                      Goal.prove context'' [] []
   1.314 +                        (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.315 +                          (foldr (mk_perm []) t pi1, foldr (mk_perm []) u pi2)))
   1.316 +                        (fn _ => EVERY
   1.317 +                           [cut_facts_tac [pi1_pi2_eq] 1,
   1.318 +                            asm_full_simp_tac (HOL_ss addsimps
   1.319 +                              (calc_atm @ List.concat perm_simps' @
   1.320 +                               fresh_prems' @ freshs2' @ abs_perm @
   1.321 +                               alpha @ List.concat inject_thms)) 1]))
   1.322 +                        (map snd cargsl' ~~ map snd cargsr');
   1.323 +
   1.324 +                    (** pi1^-1 o pi2 o us = ts **)
   1.325 +                    val _ = warning "step 5: pi1^-1 o pi2 o us = ts";
   1.326 +                    val rpi1_pi2_eqs = map (fn ((t, u), eq) =>
   1.327 +                      Goal.prove context'' [] []
   1.328 +                        (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.329 +                          (foldr (mk_perm []) u (rpi1 @ pi2), t)))
   1.330 +                        (fn _ => simp_tac (HOL_ss addsimps
   1.331 +                           ((eq RS sym) :: perm_swap)) 1))
   1.332 +                        (map snd cargsl' ~~ map snd cargsr' ~~ pi1_pi2_eqs);
   1.333 +
   1.334 +                    val (rec_prems1, rec_prems2) =
   1.335 +                      chop (length rec_prems div 2) rec_prems;
   1.336 +
   1.337 +                    (** (ts, pi1^-1 o pi2 o vs) in rec_set **)
   1.338 +                    val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set";
   1.339 +                    val rec_prems' = map (fn th =>
   1.340 +                      let
   1.341 +                        val _ $ (_ $ (_ $ x $ y) $ S) = prop_of th;
   1.342 +                        val k = find_index (equal S) rec_sets;
   1.343 +                        val pi = rpi1 @ pi2;
   1.344 +                        fun mk_pi z = foldr (mk_perm []) z pi;
   1.345 +                        fun eqvt_tac p =
   1.346 +                          let
   1.347 +                            val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
   1.348 +                            val l = find_index (equal T) dt_atomTs;
   1.349 +                            val th = List.nth (List.nth (rec_equiv_thms', l), k);
   1.350 +                            val th' = Thm.instantiate ([],
   1.351 +                              [(cterm_of thy11 (Var (("pi", 0), U)),
   1.352 +                                cterm_of thy11 p)]) th;
   1.353 +                          in rtac th' 1 end;
   1.354 +                        val th' = Goal.prove context'' [] []
   1.355 +                          (HOLogic.mk_Trueprop (HOLogic.mk_mem
   1.356 +                            (HOLogic.mk_prod (mk_pi x, mk_pi y), S)))
   1.357 +                          (fn _ => EVERY
   1.358 +                             (map eqvt_tac pi @
   1.359 +                              [simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @
   1.360 +                                 perm_swap @ perm_fresh_fresh)) 1,
   1.361 +                               rtac th 1]))
   1.362 +                      in
   1.363 +                        Simplifier.simplify
   1.364 +                          (HOL_basic_ss addsimps rpi1_pi2_eqs) th'
   1.365 +                      end) rec_prems2;
   1.366 +
   1.367 +                    val ihs = filter (fn th => case prop_of th of
   1.368 +                      _ $ (Const ("All", _) $ _) => true | _ => false) prems';
   1.369 +
   1.370 +                    (** pi1 o rs = p2 o vs , rs = pi1^-1 o pi2 o vs **)
   1.371 +                    val _ = warning "step 7: pi1 o rs = p2 o vs , rs = pi1^-1 o pi2 o vs";
   1.372 +                    val (rec_eqns1, rec_eqns2) = ListPair.unzip (map (fn (th, ih) =>
   1.373 +                      let
   1.374 +                        val th' = th RS (ih RS spec RS mp) RS sym;
   1.375 +                        val _ $ (_ $ lhs $ rhs) = prop_of th';
   1.376 +                        fun strip_perm (_ $ _ $ t) = strip_perm t
   1.377 +                          | strip_perm t = t;
   1.378 +                      in
   1.379 +                        (Goal.prove context'' [] []
   1.380 +                           (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.381 +                              (foldr (mk_perm []) lhs pi1,
   1.382 +                               foldr (mk_perm []) (strip_perm rhs) pi2)))
   1.383 +                           (fn _ => simp_tac (HOL_basic_ss addsimps
   1.384 +                              (th' :: perm_swap)) 1),
   1.385 +                         th')
   1.386 +                      end) (rec_prems' ~~ ihs));
   1.387 +
   1.388 +                    (** as # rs , bs # vs **)
   1.389 +                    val _ = warning "step 8: as # rs , bs # vs";
   1.390 +                    val (rec_freshs1, rec_freshs2) = ListPair.unzip (List.concat
   1.391 +                      (map (fn (((rec_prem, rec_prem'), eqn), ih) =>
   1.392 +                        let
   1.393 +                          val _ $ (_ $ (_ $ x $ (y as Free (_, T))) $ S) =
   1.394 +                            prop_of rec_prem;
   1.395 +                          val _ $ (_ $ (_ $ _ $ y') $ _) = prop_of rec_prem';
   1.396 +                          val k = find_index (equal S) rec_sets;
   1.397 +                          val atoms = List.concat (List.mapPartial
   1.398 +                            (fn ((bs, z), (bs', _)) =>
   1.399 +                              if z = x then NONE else SOME (bs ~~ bs'))
   1.400 +                            (cargsl' ~~ cargsr'))
   1.401 +                        in
   1.402 +                          map (fn (a as Free (_, aT), b) =>
   1.403 +                            let
   1.404 +                              val l = find_index (equal aT) dt_atomTs;
   1.405 +                              val th = Goal.prove context'' [] []
   1.406 +                                (HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.407 +                                  aT --> T --> HOLogic.boolT) $ a $ y))
   1.408 +                                (fn _ => EVERY
   1.409 +                                   (rtac (List.nth (List.nth (rec_fresh_thms, l), k)) 1 ::
   1.410 +                                    map (fn th => rtac th 1)
   1.411 +                                      (snd (List.nth (finite_thss, l))) @
   1.412 +                                    [rtac rec_prem 1, rtac ih 1,
   1.413 +                                     REPEAT_DETERM (resolve_tac fresh_prems 1)]));
   1.414 +                              val th' = Goal.prove context'' [] []
   1.415 +                                (HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.416 +                                  aT --> T --> HOLogic.boolT) $ b $ y'))
   1.417 +                                (fn _ => cut_facts_tac [th] 1 THEN
   1.418 +                                    asm_full_simp_tac (HOL_ss addsimps (eqn ::
   1.419 +                                      fresh_left @ fresh_prems' @ freshs2' @
   1.420 +                                      rev_simps @ app_simps @ calc_atm)) 1)
   1.421 +                            in (th, th') end) atoms
   1.422 +                        end) (rec_prems1 ~~ rec_prems2 ~~ rec_eqns2 ~~ ihs)));
   1.423 +
   1.424 +                    (** as # fK as ts rs , bs # fK bs us vs **)
   1.425 +                    val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
   1.426 +                    fun prove_fresh_result t (a as Free (_, aT)) =
   1.427 +                      Goal.prove context'' [] []
   1.428 +                        (HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.429 +                          aT --> rT --> HOLogic.boolT) $ a $ t))
   1.430 +                        (fn _ => EVERY
   1.431 +                           [resolve_tac fcbs 1,
   1.432 +                            REPEAT_DETERM (resolve_tac
   1.433 +                              (fresh_prems @ rec_freshs1 @ rec_freshs2) 1),
   1.434 +                            resolve_tac P_ind_ths 1,
   1.435 +                            REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
   1.436 +        
   1.437 +                    val fresh_results =
   1.438 +                      map (prove_fresh_result rhs') (List.concat (map fst cargsl')) @
   1.439 +                      map (prove_fresh_result lhs') (List.concat (map fst cargsr'));
   1.440 +
   1.441 +                    (** cs # fK as ts rs , cs # fK bs us vs **)
   1.442 +                    val _ = warning "step 10: cs # fK as ts rs , cs # fK bs us vs";
   1.443 +                    fun prove_fresh_result' recs t (a as Free (_, aT)) =
   1.444 +                      Goal.prove context'' [] []
   1.445 +                        (HOLogic.mk_Trueprop (Const ("Nominal.fresh",
   1.446 +                          aT --> rT --> HOLogic.boolT) $ a $ t))
   1.447 +                        (fn _ => EVERY
   1.448 +                          [cut_facts_tac recs 1,
   1.449 +                           REPEAT_DETERM (dresolve_tac
   1.450 +                             (the (AList.lookup op = rec_fin_supp_thms' aT)) 1),
   1.451 +                           NominalPermeq.fresh_guess_tac
   1.452 +                             (HOL_ss addsimps (freshs2 @
   1.453 +                                fs_atoms @ fresh_atm @
   1.454 +                                List.concat (map snd finite_thss))) 1]);
   1.455 +
   1.456 +                    val fresh_results' =
   1.457 +                      map (prove_fresh_result' rec_prems1 rhs') freshs1 @
   1.458 +                      map (prove_fresh_result' rec_prems2 lhs') freshs1;
   1.459 +
   1.460 +                    (** pi1 o (fK as ts rs) = pi2 o (fK bs us vs) **)
   1.461 +                    val _ = warning "step 11: pi1 o (fK as ts rs) = pi2 o (fK bs us vs)";
   1.462 +                    val pi1_pi2_result = Goal.prove context'' [] []
   1.463 +                      (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.464 +                        (foldr (mk_perm []) rhs' pi1, foldr (mk_perm []) lhs' pi2)))
   1.465 +                      (fn _ => NominalPermeq.perm_simp_tac (HOL_ss addsimps
   1.466 +                           pi1_pi2_eqs @ rec_eqns1) 1 THEN
   1.467 +                         TRY (simp_tac (HOL_ss addsimps
   1.468 +                           (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
   1.469 +
   1.470 +                    val _ = warning "final result";
   1.471 +                    val final = Goal.prove context'' [] [] (term_of concl)
   1.472 +                      (fn _ => cut_facts_tac [pi1_pi2_result RS sym] 1 THEN
   1.473 +                        full_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh @
   1.474 +                          fresh_results @ fresh_results') 1);
   1.475 +                    val final' = ProofContext.export context'' context' [final];
   1.476 +                    val _ = warning "finished!"
   1.477 +                  in
   1.478 +                    resolve_tac final' 1
   1.479 +                  end) context 1) (filter_out null (List.concat (map snd ndescr))))
   1.480           end)));
   1.481      
   1.482      (* FIXME: theorems are stored in database for testing only *)
   1.483 @@ -1568,6 +1919,7 @@
   1.484          [(("rec_equiv", List.concat rec_equiv_thms), []),
   1.485           (("rec_equiv'", List.concat rec_equiv_thms'), []),
   1.486           (("rec_fin_supp", List.concat rec_fin_supp_thms), []),
   1.487 +         (("rec_fresh", List.concat rec_fresh_thms), []),
   1.488           (("rec_unique", rec_unique), [])] ||>
   1.489        Theory.parent_path;
   1.490