src/HOL/Tools/inductive_realizer.ML
 changeset 37236 739d8b9c59da parent 37136 e0c9d3e49e15 parent 37233 b78f31ca4675 child 37678 0040bafffdef
```     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:18:51 2010 +0200
1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 01 11:30:57 2010 +0200
1.3 @@ -21,18 +21,12 @@
1.4      [name] => name
1.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
1.6
1.7 -val all_simps = map (Thm.symmetric o mk_meta_eq) @{thms HOL.all_simps};
1.8 -
1.9  fun prf_of thm =
1.10    let
1.11      val thy = Thm.theory_of_thm thm;
1.12      val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
1.13    in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
1.14
1.15 -fun forall_intr_prf t prf =
1.16 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
1.17 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
1.18 -
1.19  fun subsets [] = [[]]
1.20    | subsets (x::xs) =
1.21        let val ys = subsets xs
1.22 @@ -55,15 +49,19 @@
1.23        (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q))
1.24    | strip_one _ (Const ("==>", _) \$ P \$ Q) = (P, Q);
1.25
1.26 -fun relevant_vars prop = List.foldr (fn
1.27 -      (Var ((a, i), T), vs) => (case strip_type T of
1.28 +fun relevant_vars prop = fold (fn ((a, i), T) => fn vs =>
1.29 +     (case strip_type T of
1.30          (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
1.31 -      | _ => vs)
1.32 -    | (_, vs) => vs) [] (OldTerm.term_vars prop);
1.33 +      | _ => vs)) (Term.add_vars prop []) [];
1.34 +
1.35 +val attach_typeS = map_types (map_atyps
1.36 +  (fn TFree (s, []) => TFree (s, HOLogic.typeS)
1.37 +    | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
1.38 +    | T => T));
1.39
1.40  fun dt_of_intrs thy vs nparms intrs =
1.41    let
1.42 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
1.43 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
1.44      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
1.45        (Logic.strip_imp_concl (prop_of (hd intrs))));
1.46      val params = map dest_Var (take nparms ts);
1.47 @@ -84,7 +82,7 @@
1.48  fun gen_rvar vs (t as Var ((a, 0), T)) =
1.49        if body_type T <> HOLogic.boolT then t else
1.50          let
1.51 -          val U = TVar (("'" ^ a, 0), HOLogic.typeS)
1.52 +          val U = TVar (("'" ^ a, 0), [])
1.53            val Ts = binder_types T;
1.54            val i = length Ts;
1.55            val xs = map (pair "x") Ts;
1.56 @@ -98,8 +96,9 @@
1.57
1.58  fun mk_realizes_eqn n vs nparms intrs =
1.59    let
1.60 -    val concl = HOLogic.dest_Trueprop (concl_of (hd intrs));
1.61 -    val iTs = OldTerm.term_tvars concl;
1.62 +    val intr = map_types Type.strip_sorts (prop_of (hd intrs));
1.63 +    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
1.64 +    val iTs = rev (Term.add_tvars intr []);
1.65      val Tvs = map TVar iTs;
1.66      val (h as Const (s, T), us) = strip_comb concl;
1.67      val params = List.take (us, nparms);
1.68 @@ -110,7 +109,7 @@
1.69        (Name.variant_list used (replicate (length elTs) "x") ~~ elTs);
1.70      val rT = if n then Extraction.nullT
1.71        else Type (space_implode "_" (s ^ "T" :: vs),
1.72 -        map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
1.73 +        map (fn a => TVar (("'" ^ a, 0), [])) vs @ Tvs);
1.74      val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
1.75      val S = list_comb (h, params @ xs);
1.76      val rvs = relevant_vars S;
1.77 @@ -121,7 +120,7 @@
1.78        let val T = (the o AList.lookup (op =) rvs) v
1.79        in (Const ("typeof", T --> Type ("Type", [])) \$ Var ((v, 0), T),
1.80          Extraction.mk_typ (if n then Extraction.nullT
1.81 -          else TVar (("'" ^ v, 0), HOLogic.typeS)))
1.82 +          else TVar (("'" ^ v, 0), [])))
1.83        end;
1.84
1.85      val prems = map (mk_Tprem true) vs' @ map (mk_Tprem false) vs;
1.86 @@ -261,12 +260,12 @@
1.87      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
1.88      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
1.89      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
1.90 -    val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
1.91 -    val rlz'' = fold_rev Logic.all vs2 rlz
1.92 +    val rlz' = fold_rev Logic.all rs (prop_of rrule)
1.93    in (name, (vs,
1.94      if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
1.95 -    ProofRewriteRules.un_hhf_proof rlz' rlz''
1.96 -      (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
1.97 +    Extraction.abs_corr_shyps thy rule vs vs2
1.98 +      (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
1.99 +         (fold_rev Proofterm.forall_intr_proof' rs (prf_of rrule)))))
1.100    end;
1.101
1.102  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
1.103 @@ -275,7 +274,7 @@
1.104    let
1.105      val qualifier = Long_Name.qualifier (name_of_thm induct);
1.106      val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
1.107 -    val iTs = OldTerm.term_tvars (prop_of (hd intrs));
1.108 +    val iTs = rev (Term.add_tvars (prop_of (hd intrs)) []);
1.109      val ar = length vs + length iTs;
1.110      val params = Inductive.params_of raw_induct;
1.111      val arities = Inductive.arities_of raw_induct;
1.112 @@ -297,8 +296,6 @@
1.113      val thy1' = thy1 |>
1.114        Theory.copy |>
1.115        Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
1.116 -      fold (fn s => AxClass.axiomatize_arity
1.117 -        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
1.119      val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
1.120        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
1.121 @@ -328,10 +325,10 @@
1.122          end
1.123        else (replicate (length rs) Extraction.nullt, (recs, dummies)))
1.125 -    val rintrs = map (fn (intr, c) => Envir.eta_contract
1.126 +    val rintrs = map (fn (intr, c) => attach_typeS (Envir.eta_contract
1.127        (Extraction.realizes_of thy2 vs
1.128          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
1.129 -          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr)))
1.130 +          (subtract (op =) params' (Term.add_vars (prop_of intr) []))))) (prop_of intr))))
1.132      val (rlzpreds, rlzpreds') =
1.133        rintrs |> map (fn rintr =>
1.134 @@ -390,7 +387,9 @@
1.135          val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
1.136            (fn (_, _ \$ P, _ \$ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
1.137          val rews = map mk_meta_eq (@{thm fst_conv} :: @{thm snd_conv} :: rec_thms);
1.138 -        val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
1.139 +        val thm = Goal.prove_global thy []
1.140 +          (map attach_typeS prems) (attach_typeS concl)
1.141 +          (fn {prems, ...} => EVERY
1.142            [rtac (#raw_induct ind_info) 1,
1.143             rewrite_goals_tac rews,
1.144             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
1.145 @@ -408,10 +407,10 @@
1.146        in
1.148            (map (fn (((ind, corr), rlz), r) =>
1.149 -              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
1.150 +              mk_realizer thy'' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
1.151              realizers @ (case realizers of
1.152               [(((ind, corr), rlz), r)] =>
1.153 -               [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
1.154 +               [mk_realizer thy'' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
1.155                    ind, corr, rlz, r)]
1.156             | _ => [])) thy''
1.157        end;
1.158 @@ -445,7 +444,7 @@
1.159              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
1.160              [Bound (length prems)]));
1.161          val rlz = Extraction.realizes_of thy (vs @ Ps) r (prop_of elim);
1.162 -        val rlz' = strip_all (Logic.unvarify_global rlz);
1.163 +        val rlz' = attach_typeS (strip_all (Logic.unvarify_global rlz));
1.164          val rews = map mk_meta_eq case_thms;
1.165          val thm = Goal.prove_global thy []
1.166            (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
1.167 @@ -488,7 +487,7 @@
1.168      val vss = sort (int_ord o pairself length)
1.169        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
1.170    in
1.171 -    fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
1.172 +    fold_rev (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
1.173    end
1.174
1.175  fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
```