Implemented proof of weak induction theorem.
authorberghofe
Fri Oct 28 18:22:26 2005 +0200 (2005-10-28)
changeset 180168f3a80033ba4
parent 18015 1cd8174b7df0
child 18017 f6abeac6dcb5
Implemented proof of weak induction theorem.
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 17:59:07 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:22:26 2005 +0200
     1.3 @@ -920,6 +920,38 @@
     1.4  
     1.5  (*=======================================================================*)
     1.6  
     1.7 +(** FIXME: DatatypePackage should export this function **)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +fun dt_recs (DtTFree _) = []
    1.12 +  | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
    1.13 +  | dt_recs (DtRec i) = [i];
    1.14 +
    1.15 +fun dt_cases (descr: descr) (_, args, constrs) =
    1.16 +  let
    1.17 +    fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
    1.18 +    val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
    1.19 +  in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    1.20 +
    1.21 +
    1.22 +fun induct_cases descr =
    1.23 +  DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    1.24 +
    1.25 +fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    1.26 +
    1.27 +in
    1.28 +
    1.29 +fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
    1.30 +
    1.31 +fun mk_case_names_exhausts descr new =
    1.32 +  map (RuleCases.case_names o exhaust_cases descr o #1)
    1.33 +    (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.34 +
    1.35 +end;
    1.36 +
    1.37 +(*******************************)
    1.38 +
    1.39  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    1.40  
    1.41  fun read_typ sign ((Ts, sorts), str) =
    1.42 @@ -1386,8 +1418,12 @@
    1.43  
    1.44      val perm_defs = map snd typedefs;
    1.45      val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
    1.46 +    val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
    1.47      val Rep_thms = map (#Rep o fst) typedefs;
    1.48  
    1.49 +    val big_name = space_implode "_" new_type_names;
    1.50 +
    1.51 +
    1.52      (** prove that new types are in class pt_<name> **)
    1.53  
    1.54      val _ = warning "prove that new types are in class pt_<name> ...";
    1.55 @@ -1428,7 +1464,7 @@
    1.56                  ((Rep RS perm_closed1 RS Abs_inverse) ::
    1.57                   (if atom1 = atom2 then []
    1.58                    else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
    1.59 -              DatatypeAux.cong_tac 1,
    1.60 +              cong_tac 1,
    1.61                rtac refl 1,
    1.62                rtac cp1' 1]) thy)
    1.63          (typedefs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~
    1.64 @@ -1451,6 +1487,33 @@
    1.65            Type ("nominal.nOption", [U])) $ x $ t
    1.66        end;
    1.67  
    1.68 +    val (ty_idxs, _) = foldl
    1.69 +      (fn ((i, ("nominal.nOption", _, _)), p) => p
    1.70 +        | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
    1.71 +
    1.72 +    fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
    1.73 +      | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
    1.74 +      | reindex dt = dt;
    1.75 +
    1.76 +    fun strip_suffix i s = implode (List.take (explode s, size s - i));
    1.77 +
    1.78 +    (** strips the "_Rep" in type names *)
    1.79 +    fun strip_nth_name i s =
    1.80 +      let val xs = NameSpace.unpack s
    1.81 +      in NameSpace.pack (map_nth_elem (length xs - i) (strip_suffix 4) xs) end;
    1.82 +
    1.83 +    val descr'' = List.mapPartial
    1.84 +      (fn (i, ("nominal.nOption", _, _)) => NONE
    1.85 +        | (i, (s, dts, constrs)) => SOME (the (AList.lookup op = ty_idxs i),
    1.86 +            (strip_nth_name 1 s,  map reindex dts,
    1.87 +             map (fn (cname, cargs) =>
    1.88 +               (strip_nth_name 2 cname,
    1.89 +                foldl (fn (dt, dts) =>
    1.90 +                  let val (dts', dt') = strip_option dt
    1.91 +                  in (dts @ dts' @ [reindex dt']) end) [] cargs)) constrs))) descr;
    1.92 +    val (descr1, descr2) = splitAt (length new_type_names, descr'');
    1.93 +    val descr' = [descr1, descr2];
    1.94 +
    1.95      val typ_of_dtyp' = replace_types' o typ_of_dtyp;
    1.96  
    1.97      val rep_names = map (fn s =>
    1.98 @@ -1458,9 +1521,12 @@
    1.99      val abs_names = map (fn s =>
   1.100        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
   1.101  
   1.102 -    val recTs = get_rec_types descr sorts;
   1.103 -    val newTs' = Library.take (length new_type_names, recTs);
   1.104 -    val newTs = map replace_types' newTs';
   1.105 +    val recTs' = List.mapPartial
   1.106 +      (fn ((_, ("nominal.nOption", _, _)), T) => NONE
   1.107 +        | (_, T) => SOME T) (descr ~~ get_rec_types descr sorts');
   1.108 +    val recTs = get_rec_types (List.concat descr') sorts';
   1.109 +    val newTs' = Library.take (length new_type_names, recTs');
   1.110 +    val newTs = Library.take (length new_type_names, recTs);
   1.111  
   1.112      val full_new_type_names = map (Sign.full_name (sign_of thy)) new_type_names;
   1.113  
   1.114 @@ -1568,35 +1634,8 @@
   1.115  
   1.116      (* prove distinctness theorems *)
   1.117  
   1.118 -    fun make_distincts_1 _ [] = []
   1.119 -      | make_distincts_1 tname ((cname, cargs)::constrs) =
   1.120 -          let
   1.121 -            val cname = Sign.intern_const thy8
   1.122 -              (NameSpace.append tname (Sign.base_name cname));
   1.123 -            val (Ts, T) = strip_type (the (Sign.const_type thy8 cname));
   1.124 -            val frees = map Free ((DatatypeProp.make_tnames Ts) ~~ Ts);
   1.125 -            val t = list_comb (Const (cname, Ts ---> T), frees);
   1.126 -
   1.127 -            fun make_distincts' [] = []
   1.128 -              | make_distincts' ((cname', cargs')::constrs') =
   1.129 -                  let
   1.130 -                    val cname' = Sign.intern_const thy8
   1.131 -                      (NameSpace.append tname (Sign.base_name cname'));
   1.132 -                    val Ts' = binder_types (the (Sign.const_type thy8 cname'));
   1.133 -                    val frees' = map Free ((map ((op ^) o (rpair "'"))
   1.134 -                      (DatatypeProp.make_tnames Ts')) ~~ Ts');
   1.135 -                    val t' = list_comb (Const (cname', Ts' ---> T), frees')
   1.136 -                  in
   1.137 -                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
   1.138 -                      (make_distincts' constrs')
   1.139 -                  end
   1.140 -
   1.141 -          in (make_distincts' constrs) @ (make_distincts_1 tname constrs)
   1.142 -          end;
   1.143 -
   1.144 -    val distinct_props = map (fn ((_, (_, _, constrs)), tname) =>
   1.145 -        make_distincts_1 tname constrs)
   1.146 -      (List.take (descr, length new_type_names) ~~ new_type_names);
   1.147 +    val distinct_props = setmp DatatypeProp.dtK 1000
   1.148 +      (DatatypeProp.make_distincts new_type_names descr' sorts') thy8;
   1.149  
   1.150      val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
   1.151        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
   1.152 @@ -1784,7 +1823,82 @@
   1.153          end) atoms) constrs)
   1.154        end) (List.take (descr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
   1.155  
   1.156 +    (**** Induction theorem ****)
   1.157 +
   1.158 +    val arities = get_arities (List.concat descr');
   1.159 +
   1.160 +    fun mk_funs_inv thm =
   1.161 +      let
   1.162 +        val {sign, prop, ...} = rep_thm thm;
   1.163 +        val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
   1.164 +          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
   1.165 +        val used = add_term_tfree_names (a, []);
   1.166 +
   1.167 +        fun mk_thm i =
   1.168 +          let
   1.169 +            val Ts = map (TFree o rpair HOLogic.typeS)
   1.170 +              (variantlist (replicate i "'t", used));
   1.171 +            val f = Free ("f", Ts ---> U)
   1.172 +          in standard (Goal.prove sign [] [] (Logic.mk_implies
   1.173 +            (HOLogic.mk_Trueprop (HOLogic.list_all
   1.174 +               (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
   1.175 +             HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
   1.176 +               r $ (a $ app_bnds f i)), f))))
   1.177 +            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1]))
   1.178 +          end
   1.179 +      in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   1.180 +
   1.181 +    fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
   1.182 +      let
   1.183 +        val Rep_t = Const (List.nth (rep_names, i), T --> U) $
   1.184 +          mk_Free "x" T i;
   1.185 +
   1.186 +        val Abs_t =  Const (List.nth (abs_names, i), U --> T)
   1.187 +
   1.188 +      in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,
   1.189 +            Const (List.nth (rep_set_names, i), HOLogic.mk_setT U)) $
   1.190 +              (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
   1.191 +          concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
   1.192 +      end;
   1.193 +
   1.194 +    val (indrule_lemma_prems, indrule_lemma_concls) =
   1.195 +      Library.foldl mk_indrule_lemma (([], []), (List.concat descr' ~~ recTs ~~ recTs'));
   1.196 +
   1.197 +    val indrule_lemma = standard (Goal.prove thy8 [] []
   1.198 +      (Logic.mk_implies
   1.199 +        (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
   1.200 +         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
   1.201 +           [REPEAT (etac conjE 1),
   1.202 +            REPEAT (EVERY
   1.203 +              [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
   1.204 +               etac mp 1, resolve_tac Rep_thms 1])]));
   1.205 +
   1.206 +    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
   1.207 +    val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
   1.208 +      map (Free o apfst fst o dest_Var) Ps;
   1.209 +    val indrule_lemma' = cterm_instantiate
   1.210 +      (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
   1.211 +
   1.212 +    val Abs_inverse_thms' = List.concat (map mk_funs_inv Abs_inverse_thms);
   1.213 +
   1.214 +    val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
   1.215 +    val dt_induct = standard (Goal.prove thy8 []
   1.216 +      (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   1.217 +      (fn prems => EVERY
   1.218 +        [rtac indrule_lemma' 1,
   1.219 +         (DatatypeAux.indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.220 +         EVERY (map (fn (prem, r) => (EVERY
   1.221 +           [REPEAT (eresolve_tac Abs_inverse_thms' 1),
   1.222 +            simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
   1.223 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   1.224 +                (prems ~~ constr_defs))]));
   1.225 +
   1.226 +    val case_names_induct = mk_case_names_induct descr;
   1.227 +
   1.228      val (thy9, _) = thy8 |>
   1.229 +      Theory.add_path big_name |>
   1.230 +      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
   1.231 +      Theory.parent_path |>>>
   1.232        DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
   1.233        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
   1.234        DatatypeAux.store_thmss "perm" new_type_names perm_simps' |>>>