Added strong induction theorem (currently only axiomatized!).
authorberghofe
Mon Nov 07 18:32:54 2005 +0100 (2005-11-07)
changeset 18107ee6b4d3af498
parent 18106 836135c8acb2
child 18108 1e4516e68a58
Added strong induction theorem (currently only axiomatized!).
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Mon Nov 07 15:19:03 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Mon Nov 07 18:32:54 2005 +0100
     1.3 @@ -136,8 +136,10 @@
     1.4  
     1.5      val SOME {descr, ...} = Symtab.lookup
     1.6        (DatatypePackage.get_datatypes thy1) (hd full_new_type_names');
     1.7 -    val typ_of_dtyp = typ_of_dtyp descr sorts';
     1.8 -    fun nth_dtyp i = typ_of_dtyp (DtRec i);
     1.9 +    fun nth_dtyp i = typ_of_dtyp descr sorts' (DtRec i);
    1.10 +
    1.11 +    val dt_atomTs = filter (fn Type (s, []) => s mem atoms | _ => false)
    1.12 +      (get_nonrec_types descr sorts);
    1.13  
    1.14      (**** define permutation functions ****)
    1.15  
    1.16 @@ -156,7 +158,7 @@
    1.17        let val T = nth_dtyp i
    1.18        in map (fn (cname, dts) => 
    1.19          let
    1.20 -          val Ts = map typ_of_dtyp dts;
    1.21 +          val Ts = map (typ_of_dtyp descr sorts') dts;
    1.22            val names = DatatypeProp.make_tnames Ts;
    1.23            val args = map Free (names ~~ Ts);
    1.24            val c = Const (cname, Ts ---> T);
    1.25 @@ -404,9 +406,9 @@
    1.26            let
    1.27              val (dts, dt') = strip_option dt;
    1.28              val (dts', dt'') = strip_dtyp dt';
    1.29 -            val Ts = map typ_of_dtyp dts;
    1.30 -            val Us = map typ_of_dtyp dts';
    1.31 -            val T = typ_of_dtyp dt'';
    1.32 +            val Ts = map (typ_of_dtyp descr sorts') dts;
    1.33 +            val Us = map (typ_of_dtyp descr sorts') dts';
    1.34 +            val T = typ_of_dtyp descr sorts' dt'';
    1.35              val free = mk_Free "x" (Us ---> T) j;
    1.36              val free' = app_bnds free (length Us);
    1.37              fun mk_abs_fun (T, (i, t)) =
    1.38 @@ -594,20 +596,25 @@
    1.39        let val xs = NameSpace.unpack s; 
    1.40        in NameSpace.pack (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    1.41  
    1.42 -    val descr'' = List.mapPartial
    1.43 +    val (descr'', ndescr) = ListPair.unzip (List.mapPartial
    1.44        (fn (i, ("nominal.nOption", _, _)) => NONE
    1.45 -        | (i, (s, dts, constrs)) => SOME (the (AList.lookup op = ty_idxs i),
    1.46 -            (strip_nth_name 1 s,  map reindex dts,
    1.47 -             map (fn (cname, cargs) =>
    1.48 -               (strip_nth_name 2 cname,
    1.49 -                foldl (fn (dt, dts) =>
    1.50 -                  let val (dts', dt') = strip_option dt
    1.51 -                  in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr;
    1.52 +        | (i, (s, dts, constrs)) =>
    1.53 +             let
    1.54 +               val SOME index = AList.lookup op = ty_idxs i;
    1.55 +               val (constrs1, constrs2) = ListPair.unzip
    1.56 +                 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 cname))
    1.57 +                   (foldl_map (fn (dts, dt) =>
    1.58 +                     let val (dts', dt') = strip_option dt
    1.59 +                     in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end)
    1.60 +                       ([], cargs))) constrs)
    1.61 +             in SOME ((index, (strip_nth_name 1 s,  map reindex dts, constrs1)),
    1.62 +               (index, constrs2))
    1.63 +             end) descr);
    1.64  
    1.65      val (descr1, descr2) = splitAt (length new_type_names, descr'');
    1.66      val descr' = [descr1, descr2];
    1.67  
    1.68 -    val typ_of_dtyp' = replace_types' o typ_of_dtyp;
    1.69 +    val typ_of_dtyp' = replace_types' o typ_of_dtyp descr sorts';
    1.70  
    1.71      val rep_names = map (fn s =>
    1.72        Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
    1.73 @@ -617,7 +624,7 @@
    1.74      val recTs' = List.mapPartial
    1.75        (fn ((_, ("nominal.nOption", _, _)), T) => NONE
    1.76          | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
    1.77 -    val recTs = get_rec_types (List.concat descr') sorts';
    1.78 +    val recTs = get_rec_types descr'' sorts';
    1.79      val newTs' = Library.take (length new_type_names, recTs');
    1.80      val newTs = Library.take (length new_type_names, recTs);
    1.81  
    1.82 @@ -640,7 +647,7 @@
    1.83                     foldr mk_abs_fun
    1.84                       (list_abs (map (pair "z" o typ_of_dtyp') dts',
    1.85                         Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
    1.86 -                         typ_of_dtyp dt'') $ app_bnds x (length dts')))
    1.87 +                         typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts')))
    1.88                       xs :: r_args)
    1.89                  else error "nested recursion not (yet) supported"
    1.90              | _ => (j + 1, x' :: l_args, x' :: r_args)
    1.91 @@ -916,9 +923,9 @@
    1.92          end) atoms) constrs)
    1.93        end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
    1.94  
    1.95 -    (**** Induction theorem ****)
    1.96 +    (**** weak induction theorem ****)
    1.97  
    1.98 -    val arities = get_arities (List.concat descr');
    1.99 +    val arities = get_arities descr'';
   1.100  
   1.101      fun mk_funs_inv thm =
   1.102        let
   1.103 @@ -955,7 +962,7 @@
   1.104        end;
   1.105  
   1.106      val (indrule_lemma_prems, indrule_lemma_concls) =
   1.107 -      Library.foldl mk_indrule_lemma (([], []), (List.concat descr' ~~ recTs ~~ recTs'));
   1.108 +      Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
   1.109  
   1.110      val indrule_lemma = standard (Goal.prove thy8 [] []
   1.111        (Logic.mk_implies
   1.112 @@ -986,7 +993,7 @@
   1.113              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   1.114                  (prems ~~ constr_defs))]));
   1.115  
   1.116 -    val case_names_induct = mk_case_names_induct (List.concat descr');
   1.117 +    val case_names_induct = mk_case_names_induct descr'';
   1.118  
   1.119      (**** prove that new datatypes have finite support ****)
   1.120  
   1.121 @@ -1011,6 +1018,56 @@
   1.122           length new_type_names))
   1.123        end) atoms;
   1.124  
   1.125 +    (**** strong induction theorem ****)
   1.126 +
   1.127 +    val pnames = if length descr'' = 1 then ["P"]
   1.128 +      else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
   1.129 +    val ind_sort = map (fn T => Sign.intern_class thy8 ("fs_" ^
   1.130 +      Sign.base_name (fst (dest_Type T)))) dt_atomTs;
   1.131 +    val fsT = TFree ("'n", ind_sort);
   1.132 +
   1.133 +    fun make_pred i T =
   1.134 +      Free (List.nth (pnames, i), T --> fsT --> HOLogic.boolT);
   1.135 +
   1.136 +    fun make_ind_prem k T ((cname, cargs), idxs) =
   1.137 +      let
   1.138 +        val recs = List.filter is_rec_type cargs;
   1.139 +        val Ts = map (typ_of_dtyp descr'' sorts') cargs;
   1.140 +        val recTs' = map (typ_of_dtyp descr'' sorts') recs;
   1.141 +        val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
   1.142 +        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   1.143 +        val frees = tnames ~~ Ts;
   1.144 +        val z = (variant tnames "z", fsT);
   1.145 +
   1.146 +        fun mk_prem ((dt, s), T) =
   1.147 +          let
   1.148 +            val (Us, U) = strip_type T;
   1.149 +            val l = length Us
   1.150 +          in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
   1.151 +            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) l $ Bound l))
   1.152 +          end;
   1.153 +
   1.154 +        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
   1.155 +        val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
   1.156 +            (Const ("nominal.fresh", T --> fsT --> HOLogic.boolT) $
   1.157 +              Free p $ Free z))
   1.158 +          (map (curry List.nth frees) (List.concat (map (fn (m, n) =>
   1.159 +             m upto m + n - 1) idxs)))
   1.160 +
   1.161 +      in list_all_free (z :: frees, Logic.list_implies (prems' @ prems,
   1.162 +        HOLogic.mk_Trueprop (make_pred k T $ 
   1.163 +          list_comb (Const (cname, Ts ---> T), map Free frees) $ Free z)))
   1.164 +      end;
   1.165 +
   1.166 +    val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   1.167 +      map (make_ind_prem i T) (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
   1.168 +    val tnames = DatatypeProp.make_tnames recTs;
   1.169 +    val z = (variant tnames "z", fsT);
   1.170 +    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   1.171 +      (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T) $ Free z)
   1.172 +        (descr'' ~~ recTs ~~ tnames)));
   1.173 +    val induct = Logic.list_implies (ind_prems, ind_concl);
   1.174 +
   1.175      val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
   1.176  
   1.177      val (thy9, _) = thy8 |>
   1.178 @@ -1029,7 +1086,10 @@
   1.179              (fst (dest_Type T),
   1.180                replicate (length sorts) [class], [class])
   1.181              (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
   1.182 -        end) (atoms ~~ finite_supp_thms);
   1.183 +        end) (atoms ~~ finite_supp_thms) |>>
   1.184 +      Theory.add_path big_name |>>>
   1.185 +      PureThy.add_axioms_i [(("induct_test", induct), [case_names_induct])] |>>
   1.186 +      Theory.parent_path;
   1.187  
   1.188    in
   1.189      thy9