Extended strong induction rule with additional
authorberghofe
Wed May 24 10:02:36 2006 +0200 (2006-05-24)
changeset 19710ee9c7fa80d21
parent 19709 78cd5f6af8e8
child 19711 2401b1a3087f
Extended strong induction rule with additional
freshness constraints.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed May 24 01:47:25 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed May 24 10:02:36 2006 +0200
     1.3 @@ -677,6 +677,9 @@
     1.4      val (descr1, descr2) = chop (length new_type_names) descr'';
     1.5      val descr' = [descr1, descr2];
     1.6  
     1.7 +    fun partition_cargs idxs xs = map (fn (i, j) =>
     1.8 +      (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
     1.9 +
    1.10      val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts';
    1.11  
    1.12      val rep_names = map (fn s =>
    1.13 @@ -1119,6 +1122,7 @@
    1.14          val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
    1.15          val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
    1.16          val frees = tnames ~~ Ts;
    1.17 +        val frees' = partition_cargs idxs frees;
    1.18          val z = (variant tnames "z", fsT);
    1.19  
    1.20          fun mk_prem ((dt, s), T) =
    1.21 @@ -1129,11 +1133,24 @@
    1.22              (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
    1.23            end;
    1.24  
    1.25 +        fun mk_fresh1 xs [] = []
    1.26 +          | mk_fresh1 xs ((y as (_, T)):: ys) = map (fn x => HOLogic.mk_Trueprop
    1.27 +                (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
    1.28 +                  (filter (fn (_, U) => T = U) (rev xs)) @
    1.29 +              mk_fresh1 (y :: xs) ys;
    1.30 +
    1.31 +        fun mk_fresh2 xss [] = []
    1.32 +          | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
    1.33 +                map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
    1.34 +                  (Const ("Nominal.fresh", T --> U --> HOLogic.boolT) $ Free y $ Free x))
    1.35 +                    (rev xss @ yss)) ys) @
    1.36 +              mk_fresh2 (p :: xss) yss;
    1.37 +
    1.38          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
    1.39          val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
    1.40 -            (f T (Free p) (Free z)))
    1.41 -          (map (curry List.nth frees) (List.concat (map (fn (m, n) =>
    1.42 -             m upto m + n - 1) idxs)))
    1.43 +            (f T (Free p) (Free z))) (List.concat (map fst frees')) @
    1.44 +          mk_fresh1 [] (List.concat (map fst frees')) @
    1.45 +          mk_fresh2 [] frees'
    1.46  
    1.47        in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
    1.48          HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
    1.49 @@ -1198,7 +1215,7 @@
    1.50            Const ("List.list.Nil", pT)
    1.51        end;
    1.52  
    1.53 -    fun mk_fresh i i' j k p l vs _ _ =
    1.54 +    fun mk_fresh i i' j k p l is vs _ _ =
    1.55        let
    1.56          val n = length vs;
    1.57          val Ts = map snd vs;
    1.58 @@ -1206,18 +1223,25 @@
    1.59          val f = the (AList.lookup op = fresh_fs T);
    1.60          val U = List.nth (Ts, n - i' - 1);
    1.61          val S = HOLogic.mk_setT T;
    1.62 +        val prms' = map Bound (n - k downto n - k - p + 1);
    1.63          val prms = map (mk_ind_perm (n - i) k p (n - l) (("a", T) :: vs))
    1.64 -            (j - 1 downto 0) @
    1.65 -          map Bound (n - k downto n - k - p + 1)
    1.66 +            (j - 1 downto 0) @ prms';
    1.67 +        val bs = rev (List.mapPartial
    1.68 +          (fn ((_, T'), i) => if T = T' then SOME (Bound i) else NONE)
    1.69 +          (List.take (vs, n - k - p - 1) ~~ (1 upto n - k - p - 1)));
    1.70 +        val ts = map (fn i =>
    1.71 +          Const ("Nominal.supp", List.nth (Ts, n - i - 1) --> S) $
    1.72 +            foldr (mk_perm (T :: Ts)) (Bound (n - i)) prms') is
    1.73        in
    1.74          HOLogic.mk_Trueprop (Const ("Ex", (T --> HOLogic.boolT) --> HOLogic.boolT) $
    1.75            Abs ("a", T, HOLogic.Not $
    1.76              (Const ("op :", T --> S --> HOLogic.boolT) $ Bound 0 $
    1.77 -              (Const ("insert", T --> S --> S) $
    1.78 -                (foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms) $
    1.79 -                (Const ("op Un", S --> S --> S) $ (f $ Bound (n - k - p)) $
    1.80 -                   (Const ("Nominal.supp", U --> S) $
    1.81 -                     foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms))))))
    1.82 +              (foldr (fn (t, u) => Const ("insert", T --> S --> S) $ t $ u)
    1.83 +                (foldl (fn (t, u) => Const ("op Un", S --> S --> S) $ u $ t)
    1.84 +                  (f $ Bound (n - k - p))
    1.85 +                  (Const ("Nominal.supp", U --> S) $
    1.86 +                     foldr (mk_perm (T :: Ts)) (Bound (n - i')) prms :: ts))
    1.87 +                (foldr (mk_perm (T :: Ts)) (Bound (n - i - j)) prms :: bs)))))
    1.88        end;
    1.89  
    1.90      fun mk_fresh_constr is p vs _ concl =
    1.91 @@ -1252,6 +1276,24 @@
    1.92      val induct_aux_lemmas' = map (fn Type (s, _) =>
    1.93        PureThy.get_thm thy9 (Name ("pt_" ^ Sign.base_name s ^ "2")) RS sym) dt_atomTs;
    1.94  
    1.95 +    val fresh_aux = PureThy.get_thms thy9 (Name "fresh_aux");
    1.96 +
    1.97 +    (**********************************************************************
    1.98 +      The subgoals occurring in the proof of induct_aux have the
    1.99 +      following parameters:
   1.100 +
   1.101 +        x_1 ... x_k p_1 ... p_m z b_1 ... b_n
   1.102 +
   1.103 +      where
   1.104 +
   1.105 +        x_i : constructor arguments (introduced by weak induction rule)
   1.106 +        p_i : permutations (one for each atom type in the data type)
   1.107 +        z   : freshness context
   1.108 +        b_i : newly introduced names for binders (sufficiently fresh)
   1.109 +    ***********************************************************************)
   1.110 +
   1.111 +    val _ = warning "proving strong induction theorem ...";
   1.112 +
   1.113      val induct_aux = standard (Goal.prove thy9 [] ind_prems' ind_concl'
   1.114        (fn prems => EVERY
   1.115          ([mk_subgoal 1 (K (K (K aux_ind_concl))),
   1.116 @@ -1269,7 +1311,9 @@
   1.117                       in
   1.118                         [mk_subgoal 1 (mk_fresh i (i + j) j'
   1.119                            (length cargs) (length dt_atomTs)
   1.120 -                          (length cargs + length dt_atomTs + 1 + i - k)),
   1.121 +                          (length cargs + length dt_atomTs + 1 + i - k)
   1.122 +                          (List.mapPartial (fn (i', j) =>
   1.123 +                             if i = i' then NONE else SOME (i' + j)) is)),
   1.124                          rtac at_finite_select 1,
   1.125                          rtac (PureThy.get_thm thy9 (Name ("at_" ^ atom ^ "_inst"))) 1,
   1.126                          asm_full_simp_tac (simpset_of thy9 addsimps
   1.127 @@ -1286,14 +1330,19 @@
   1.128                      alpha @ abs_perm @ abs_fresh @ [abs_fun_finite_supp] @
   1.129                      induct_aux_lemmas)) 1,
   1.130                   dtac sym 1,
   1.131 -                 asm_full_simp_tac (simpset_of thy9
   1.132 -                   addsimps induct_aux_lemmas'
   1.133 -                   addsimprocs [perm_simproc]) 1,
   1.134 +                 asm_full_simp_tac (simpset_of thy9) 1,
   1.135                   REPEAT (etac conjE 1)]
   1.136                else
   1.137                  []) @
   1.138               [(resolve_tac prems THEN_ALL_NEW
   1.139 -                (atac ORELSE' ((REPEAT o etac allE) THEN' atac))) 1])
   1.140 +                (atac ORELSE'
   1.141 +                  SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
   1.142 +                      _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
   1.143 +                        asm_simp_tac (simpset_of thy9 addsimps fresh_aux) i
   1.144 +                    | _ =>
   1.145 +                        asm_simp_tac (simpset_of thy9
   1.146 +                        addsimps induct_aux_lemmas'
   1.147 +                        addsimprocs [perm_simproc]) i))) 1])
   1.148                 (constrs ~~ constrs'))) (descr'' ~~ ndescr)) @
   1.149           [REPEAT (eresolve_tac [conjE, allE_Nil] 1),
   1.150            REPEAT (etac allE 1),
   1.151 @@ -1352,9 +1401,6 @@
   1.152  
   1.153      (* introduction rules for graph of recursion function *)
   1.154  
   1.155 -    fun partition_cargs idxs xs = map (fn (i, j) =>
   1.156 -      (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
   1.157 -
   1.158      fun mk_fresh_fun (a, t) = Const ("Nominal.fresh_fun",
   1.159        (fastype_of a --> fastype_of t) --> fastype_of t) $ lambda a t;
   1.160