src/HOL/Tools/datatype_realizer.ML
changeset 13725 12404b452034
parent 13708 a3a410782c95
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Nov 25 20:32:29 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Nov 27 17:06:47 2002 +0100
     1.3 @@ -36,6 +36,9 @@
     1.4  
     1.5  fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
     1.6  
     1.7 +fun tname_of (Type (s, _)) = s
     1.8 +  | tname_of _ = "";
     1.9 +
    1.10  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
    1.11  
    1.12  fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) (is, thy) =
    1.13 @@ -135,19 +138,15 @@
    1.14          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
    1.15        |>> Theory.add_path (NameSpace.pack (if_none path []));
    1.16  
    1.17 -    val inst = map (fn ((((i, _), s), T), U) => ((s, 0), if i mem is then
    1.18 -        Abs ("r", U, Abs ("x", T, mk_realizes U $ Bound 1 $
    1.19 -          (Var ((s, 0), T --> HOLogic.boolT) $ Bound 0)))
    1.20 -      else Abs ("x", T, mk_realizes Extraction.nullT $ Extraction.nullt $
    1.21 -        (Var ((s, 0), T --> HOLogic.boolT) $
    1.22 -          Bound 0)))) (descr ~~ pnames ~~ map Type.varifyT recTs ~~
    1.23 -            map Type.varifyT rec_result_Ts);
    1.24 +    val ivs = Drule.vars_of_terms
    1.25 +      [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
    1.26 +    val rvs = Drule.vars_of_terms [prop_of thm'];
    1.27 +    val ivs1 = map Var (filter_out (fn (_, T) =>
    1.28 +      tname_of (body_type T) mem ["set", "bool"]) ivs);
    1.29 +    val ivs2 = map (fn (ixn, _) => Var (ixn, the (assoc (rvs, ixn)))) ivs;
    1.30  
    1.31 -    val ivs = map Var (Drule.vars_of_terms
    1.32 -      [Logic.varify (DatatypeProp.make_ind [descr] sorts)]);
    1.33 -
    1.34 -    val prf = foldr forall_intr_prf (ivs,
    1.35 -      prf_subst_vars inst (foldr (fn ((f, p), prf) =>
    1.36 +    val prf = foldr forall_intr_prf (ivs2,
    1.37 +      foldr (fn ((f, p), prf) =>
    1.38          (case head_of (strip_abs_body f) of
    1.39             Free (s, T) =>
    1.40               let val T' = Type.varifyT T
    1.41 @@ -156,10 +155,10 @@
    1.42               end
    1.43           | _ => AbsP ("H", Some p, prf)))
    1.44             (rec_fns ~~ prems_of thm, Proofterm.proof_combP
    1.45 -             (prf_of thm', map PBound (length prems - 1 downto 0)))));
    1.46 +             (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.47  
    1.48      val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
    1.49 -      (map Logic.unvarify ivs @ filter_out is_unit
    1.50 +      (map Logic.unvarify ivs1 @ filter_out is_unit
    1.51          (map (head_of o strip_abs_body) rec_fns), r));
    1.52  
    1.53    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    1.54 @@ -211,24 +210,19 @@
    1.55        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
    1.56        |>> Theory.add_path (NameSpace.pack (if_none path []));
    1.57  
    1.58 -    val P = Var (("P", 0), HOLogic.boolT);
    1.59 +    val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.60      val prf = forall_intr_prf (y, forall_intr_prf (P,
    1.61 -      prf_subst_vars [(("P", 0), Abs ("r", rT',
    1.62 -        mk_realizes rT' $ Bound 0 $ P))] (foldr (fn ((p, r), prf) =>
    1.63 -          forall_intr_prf (Logic.varify r, AbsP ("H", Some (Logic.varify p),
    1.64 -            prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
    1.65 -              map PBound (length prems - 1 downto 0))))));
    1.66 +      foldr (fn ((p, r), prf) =>
    1.67 +        forall_intr_prf (Logic.varify r, AbsP ("H", Some (Logic.varify p),
    1.68 +          prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
    1.69 +            map PBound (length prems - 1 downto 0)))));
    1.70      val r' = Logic.varify (Abs ("y", Type.varifyT T,
    1.71 -      Abs ("P", HOLogic.boolT, list_abs (map dest_Free rs, list_comb (r,
    1.72 -        map Bound ((length rs - 1 downto 0) @ [length rs + 1]))))));
    1.73 -
    1.74 -    val prf' = forall_intr_prf (y, forall_intr_prf (P, prf_subst_vars
    1.75 -      [(("P", 0), mk_realizes Extraction.nullT $ Extraction.nullt $ P)]
    1.76 -        (prf_of exhaustion)));
    1.77 +      list_abs (map dest_Free rs, list_comb (r,
    1.78 +        map Bound ((length rs - 1 downto 0) @ [length rs])))));
    1.79  
    1.80    in Extraction.add_realizers_i
    1.81      [(exh_name, (["P"], r', prf)),
    1.82 -     (exh_name, ([], Extraction.nullt, prf'))] thy'
    1.83 +     (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
    1.84    end;
    1.85  
    1.86