rearranged
authorhaftmann
Thu Mar 20 12:01:17 2008 +0100 (2008-03-20)
changeset 2635446c7d00dd4b4
parent 26353 537ff6997149
child 26355 9276633fdc24
rearranged
src/Pure/Isar/code_unit.ML
     1.1 --- a/src/Pure/Isar/code_unit.ML	Thu Mar 20 12:01:16 2008 +0100
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Thu Mar 20 12:01:17 2008 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val constrain_thm: sort -> thm -> thm
     1.5  
     1.6    (*constants*)
     1.7 -  val add_const_ident: thm -> theory -> theory
     1.8 +  val add_const_alias: thm -> theory -> theory
     1.9    val string_of_typ: theory -> typ -> string
    1.10    val string_of_const: theory -> string -> string
    1.11    val no_args: theory -> string -> int
    1.12 @@ -66,27 +66,204 @@
    1.13  
    1.14  fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;
    1.15  
    1.16 +
    1.17 +(* utilities *)
    1.18 +
    1.19 +fun inst_thm tvars' thm =
    1.20 +  let
    1.21 +    val thy = Thm.theory_of_thm thm;
    1.22 +    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    1.23 +    fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v
    1.24 +     of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort)))
    1.25 +      | NONE => NONE;
    1.26 +    val insts = map_filter mk_inst tvars;
    1.27 +  in Thm.instantiate (insts, []) thm end;
    1.28 +
    1.29 +fun constrain_thm sort thm =
    1.30 +  let
    1.31 +    val thy = Thm.theory_of_thm thm;
    1.32 +    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort
    1.33 +    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    1.34 +    fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v)
    1.35 +      (sort, constrain sort)
    1.36 +    val insts = map mk_inst tvars;
    1.37 +  in Thm.instantiate (insts, []) thm end;
    1.38 +
    1.39 +fun expand_eta k thm =
    1.40 +  let
    1.41 +    val thy = Thm.theory_of_thm thm;
    1.42 +    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    1.43 +    val (head, args) = strip_comb lhs;
    1.44 +    val l = if k = ~1
    1.45 +      then (length o fst o strip_abs) rhs
    1.46 +      else Int.max (0, k - length args);
    1.47 +    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
    1.48 +    fun get_name _ 0 = pair []
    1.49 +      | get_name (Abs (v, ty, t)) k =
    1.50 +          Name.variants [v]
    1.51 +          ##>> get_name t (k - 1)
    1.52 +          #>> (fn ([v'], vs') => (v', ty) :: vs')
    1.53 +      | get_name t k = 
    1.54 +          let
    1.55 +            val (tys, _) = (strip_type o fastype_of) t
    1.56 +          in case tys
    1.57 +           of [] => raise TERM ("expand_eta", [t])
    1.58 +            | ty :: _ =>
    1.59 +                Name.variants [""]
    1.60 +                #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
    1.61 +                #>> (fn vs' => (v, ty) :: vs'))
    1.62 +          end;
    1.63 +    val (vs, _) = get_name rhs l used;
    1.64 +    fun expand (v, ty) thm = Drule.fun_cong_rule thm
    1.65 +      (Thm.cterm_of thy (Var ((v, 0), ty)));
    1.66 +  in
    1.67 +    thm
    1.68 +    |> fold expand vs
    1.69 +    |> Conv.fconv_rule Drule.beta_eta_conversion
    1.70 +  end;
    1.71 +
    1.72 +fun func_conv conv =
    1.73 +  let
    1.74 +    fun lhs_conv ct = if can Thm.dest_comb ct
    1.75 +      then (Conv.combination_conv lhs_conv conv) ct
    1.76 +      else Conv.all_conv ct;
    1.77 +  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
    1.78 +
    1.79 +fun head_conv conv =
    1.80 +  let
    1.81 +    fun lhs_conv ct = if can Thm.dest_comb ct
    1.82 +      then (Conv.fun_conv lhs_conv) ct
    1.83 +      else conv ct;
    1.84 +  in Conv.fun_conv (Conv.arg_conv lhs_conv) end;
    1.85 +
    1.86 +val rewrite_func = Conv.fconv_rule o func_conv o MetaSimplifier.rewrite false;
    1.87 +
    1.88 +val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false;
    1.89 +
    1.90 +fun norm_args thms =
    1.91 +  let
    1.92 +    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    1.93 +    val k = fold (curry Int.max o num_args_of o Thm.plain_prop_of) thms 0;
    1.94 +  in
    1.95 +    thms
    1.96 +    |> map (expand_eta k)
    1.97 +    |> map (Conv.fconv_rule Drule.beta_eta_conversion)
    1.98 +  end;
    1.99 +
   1.100 +fun canonical_tvars purify_tvar thm =
   1.101 +  let
   1.102 +    val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm);
   1.103 +    fun tvars_subst_for thm = (fold_types o fold_atyps)
   1.104 +      (fn TVar (v_i as (v, _), sort) => let
   1.105 +            val v' = purify_tvar v
   1.106 +          in if v = v' then I
   1.107 +          else insert (op =) (v_i, (v', sort)) end
   1.108 +        | _ => I) (prop_of thm) [];
   1.109 +    fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
   1.110 +      let
   1.111 +        val ty = TVar (v_i, sort)
   1.112 +      in
   1.113 +        (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
   1.114 +      end;
   1.115 +    val maxidx = Thm.maxidx_of thm + 1;
   1.116 +    val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
   1.117 +  in Thm.instantiate (inst, []) thm end;
   1.118 +
   1.119 +fun canonical_vars purify_var thm =
   1.120 +  let
   1.121 +    val cterm = Thm.cterm_of (Thm.theory_of_thm thm);
   1.122 +    fun vars_subst_for thm = fold_aterms
   1.123 +      (fn Var (v_i as (v, _), ty) => let
   1.124 +            val v' = purify_var v
   1.125 +          in if v = v' then I
   1.126 +          else insert (op =) (v_i, (v', ty)) end
   1.127 +        | _ => I) (prop_of thm) [];
   1.128 +    fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
   1.129 +      let
   1.130 +        val t = Var (v_i, ty)
   1.131 +      in
   1.132 +        (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
   1.133 +      end;
   1.134 +    val maxidx = Thm.maxidx_of thm + 1;
   1.135 +    val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
   1.136 +  in Thm.instantiate ([], inst) thm end;
   1.137 +
   1.138 +fun canonical_absvars purify_var thm =
   1.139 +  let
   1.140 +    val t = Thm.plain_prop_of thm;
   1.141 +    val t' = Term.map_abs_vars purify_var t;
   1.142 +  in Thm.rename_boundvars t t' thm end;
   1.143 +
   1.144 +fun norm_varnames purify_tvar purify_var thms =
   1.145 +  let
   1.146 +    fun burrow_thms f [] = []
   1.147 +      | burrow_thms f thms =
   1.148 +          thms
   1.149 +          |> Conjunction.intr_balanced
   1.150 +          |> f
   1.151 +          |> Conjunction.elim_balanced (length thms)
   1.152 +  in
   1.153 +    thms
   1.154 +    |> burrow_thms (canonical_tvars purify_tvar)
   1.155 +    |> map (canonical_vars purify_var)
   1.156 +    |> map (canonical_absvars purify_var)
   1.157 +    |> map Drule.zero_var_indexes
   1.158 +  end;
   1.159 +
   1.160 +(* const aliasses *)
   1.161 +
   1.162 +structure ConstAlias = TheoryDataFun
   1.163 +(
   1.164 +  type T = ((string * string) * thm) list;
   1.165 +  val empty = [];
   1.166 +  val copy = I;
   1.167 +  val extend = copy;
   1.168 +  fun merge _ = Library.merge (eq_snd Thm.eq_thm_prop);
   1.169 +);
   1.170 +
   1.171 +fun add_const_alias thm =
   1.172 +  let
   1.173 +    val t = Thm.prop_of thm;
   1.174 +    val thy = Thm.theory_of_thm thm;
   1.175 +    val lhs_rhs = case try Logic.dest_equals t
   1.176 +     of SOME lhs_rhs => lhs_rhs
   1.177 +      | _ => error ("Not an equation: " ^ Display.string_of_thm thm);
   1.178 +    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
   1.179 +     of SOME c_c' => c_c'
   1.180 +      | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm);
   1.181 +  in ConstAlias.map (cons (c_c', thm)) end;
   1.182 +
   1.183 +fun rew_alias thm =
   1.184 +  let
   1.185 +    val thy = Thm.theory_of_thm thm;
   1.186 +  in rewrite_head (map snd (ConstAlias.get thy)) thm end;
   1.187 +
   1.188 +fun subst_alias thy c = ConstAlias.get thy
   1.189 +  |> get_first (fn ((c', c''), _) => if c = c' then SOME c'' else NONE)
   1.190 +  |> the_default c;
   1.191 +
   1.192  (* reading constants as terms and wildcards pattern *)
   1.193  
   1.194  fun check_bare_const thy t = case try dest_Const t
   1.195   of SOME c_ty => c_ty
   1.196    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t);
   1.197  
   1.198 -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
   1.199 +fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o check_bare_const thy;
   1.200  
   1.201  fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
   1.202  
   1.203 -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
   1.204 +fun read_const thy = subst_alias thy o AxClass.unoverload_const thy o read_bare_const thy;
   1.205  
   1.206  local
   1.207  
   1.208  fun consts_of thy some_thyname =
   1.209    let
   1.210      val this_thy = Option.map theory some_thyname |> the_default thy;
   1.211 -    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   1.212 +    val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   1.213        ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
   1.214 +    val cs = map (subst_alias thy) raw_cs;
   1.215      fun belongs_here thyname c =
   1.216 -          not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
   1.217 +      not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
   1.218    in case some_thyname
   1.219     of NONE => cs
   1.220      | SOME thyname => filter (belongs_here thyname) cs
   1.221 @@ -189,30 +366,6 @@
   1.222  
   1.223  (* defining equations *)
   1.224  
   1.225 -structure ConstIdent = TheoryDataFun
   1.226 -(
   1.227 -  type T = thm list;
   1.228 -  val empty = [];
   1.229 -  val copy = I;
   1.230 -  val extend = copy;
   1.231 -  fun merge _ = Library.merge Thm.eq_thm_prop;
   1.232 -);
   1.233 -
   1.234 -fun add_const_ident thm =
   1.235 -  let
   1.236 -    val t = Thm.prop_of thm;
   1.237 -    val lhs_rhs = case try Logic.dest_equals t
   1.238 -     of SOME lhs_rhs => lhs_rhs
   1.239 -      | _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
   1.240 -    val _ = if can (pairself dest_Const) lhs_rhs then ()
   1.241 -      else bad_thm ("Not an equation with two constants: " ^ Display.string_of_thm thm);
   1.242 -  in ConstIdent.map (cons thm) end;
   1.243 -
   1.244 -fun apply_ident thm =
   1.245 -  let
   1.246 -    val thy = Thm.theory_of_thm thm;
   1.247 -  in MetaSimplifier.rewrite_rule (ConstIdent.get thy) thm end;
   1.248 -
   1.249  fun assert_func thm =
   1.250    let
   1.251      val thy = Thm.theory_of_thm thm;
   1.252 @@ -244,7 +397,7 @@
   1.253      val _ = map (check 0) args;
   1.254    in thm end;
   1.255  
   1.256 -val mk_func = apply_ident o assert_func o mk_rew;
   1.257 +val mk_func = rew_alias o assert_func o mk_rew;
   1.258  
   1.259  fun head_func thm =
   1.260    let
   1.261 @@ -254,141 +407,6 @@
   1.262    in (c, ty) end;
   1.263  
   1.264  
   1.265 -(* utilities *)
   1.266 -
   1.267 -fun inst_thm tvars' thm =
   1.268 -  let
   1.269 -    val thy = Thm.theory_of_thm thm;
   1.270 -    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
   1.271 -    fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v
   1.272 -     of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort)))
   1.273 -      | NONE => NONE;
   1.274 -    val insts = map_filter mk_inst tvars;
   1.275 -  in Thm.instantiate (insts, []) thm end;
   1.276 -
   1.277 -fun constrain_thm sort thm =
   1.278 -  let
   1.279 -    val thy = Thm.theory_of_thm thm;
   1.280 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort
   1.281 -    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
   1.282 -    fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v)
   1.283 -      (sort, constrain sort)
   1.284 -    val insts = map mk_inst tvars;
   1.285 -  in Thm.instantiate (insts, []) thm end;
   1.286 -
   1.287 -fun expand_eta k thm =
   1.288 -  let
   1.289 -    val thy = Thm.theory_of_thm thm;
   1.290 -    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
   1.291 -    val (head, args) = strip_comb lhs;
   1.292 -    val l = if k = ~1
   1.293 -      then (length o fst o strip_abs) rhs
   1.294 -      else Int.max (0, k - length args);
   1.295 -    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
   1.296 -    fun get_name _ 0 = pair []
   1.297 -      | get_name (Abs (v, ty, t)) k =
   1.298 -          Name.variants [v]
   1.299 -          ##>> get_name t (k - 1)
   1.300 -          #>> (fn ([v'], vs') => (v', ty) :: vs')
   1.301 -      | get_name t k = 
   1.302 -          let
   1.303 -            val (tys, _) = (strip_type o fastype_of) t
   1.304 -          in case tys
   1.305 -           of [] => raise TERM ("expand_eta", [t])
   1.306 -            | ty :: _ =>
   1.307 -                Name.variants [""]
   1.308 -                #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
   1.309 -                #>> (fn vs' => (v, ty) :: vs'))
   1.310 -          end;
   1.311 -    val (vs, _) = get_name rhs l used;
   1.312 -    fun expand (v, ty) thm = Drule.fun_cong_rule thm
   1.313 -      (Thm.cterm_of thy (Var ((v, 0), ty)));
   1.314 -  in
   1.315 -    thm
   1.316 -    |> fold expand vs
   1.317 -    |> Conv.fconv_rule Drule.beta_eta_conversion
   1.318 -  end;
   1.319 -
   1.320 -fun func_conv conv =
   1.321 -  let
   1.322 -    fun lhs_conv ct = if can Thm.dest_comb ct
   1.323 -      then (Conv.combination_conv lhs_conv conv) ct
   1.324 -      else Conv.all_conv ct;
   1.325 -  in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end;
   1.326 -
   1.327 -val rewrite_func = Conv.fconv_rule o func_conv o MetaSimplifier.rewrite false;
   1.328 -
   1.329 -fun norm_args thms =
   1.330 -  let
   1.331 -    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
   1.332 -    val k = fold (curry Int.max o num_args_of o Thm.plain_prop_of) thms 0;
   1.333 -  in
   1.334 -    thms
   1.335 -    |> map (expand_eta k)
   1.336 -    |> map (Conv.fconv_rule Drule.beta_eta_conversion)
   1.337 -  end;
   1.338 -
   1.339 -fun canonical_tvars purify_tvar thm =
   1.340 -  let
   1.341 -    val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm);
   1.342 -    fun tvars_subst_for thm = (fold_types o fold_atyps)
   1.343 -      (fn TVar (v_i as (v, _), sort) => let
   1.344 -            val v' = purify_tvar v
   1.345 -          in if v = v' then I
   1.346 -          else insert (op =) (v_i, (v', sort)) end
   1.347 -        | _ => I) (prop_of thm) [];
   1.348 -    fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
   1.349 -      let
   1.350 -        val ty = TVar (v_i, sort)
   1.351 -      in
   1.352 -        (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
   1.353 -      end;
   1.354 -    val maxidx = Thm.maxidx_of thm + 1;
   1.355 -    val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
   1.356 -  in Thm.instantiate (inst, []) thm end;
   1.357 -
   1.358 -fun canonical_vars purify_var thm =
   1.359 -  let
   1.360 -    val cterm = Thm.cterm_of (Thm.theory_of_thm thm);
   1.361 -    fun vars_subst_for thm = fold_aterms
   1.362 -      (fn Var (v_i as (v, _), ty) => let
   1.363 -            val v' = purify_var v
   1.364 -          in if v = v' then I
   1.365 -          else insert (op =) (v_i, (v', ty)) end
   1.366 -        | _ => I) (prop_of thm) [];
   1.367 -    fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
   1.368 -      let
   1.369 -        val t = Var (v_i, ty)
   1.370 -      in
   1.371 -        (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
   1.372 -      end;
   1.373 -    val maxidx = Thm.maxidx_of thm + 1;
   1.374 -    val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
   1.375 -  in Thm.instantiate ([], inst) thm end;
   1.376 -
   1.377 -fun canonical_absvars purify_var thm =
   1.378 -  let
   1.379 -    val t = Thm.plain_prop_of thm;
   1.380 -    val t' = Term.map_abs_vars purify_var t;
   1.381 -  in Thm.rename_boundvars t t' thm end;
   1.382 -
   1.383 -fun norm_varnames purify_tvar purify_var thms =
   1.384 -  let
   1.385 -    fun burrow_thms f [] = []
   1.386 -      | burrow_thms f thms =
   1.387 -          thms
   1.388 -          |> Conjunction.intr_balanced
   1.389 -          |> f
   1.390 -          |> Conjunction.elim_balanced (length thms)
   1.391 -  in
   1.392 -    thms
   1.393 -    |> burrow_thms (canonical_tvars purify_tvar)
   1.394 -    |> map (canonical_vars purify_var)
   1.395 -    |> map (canonical_absvars purify_var)
   1.396 -    |> map Drule.zero_var_indexes
   1.397 -  end;
   1.398 -
   1.399 -
   1.400  (* case cerificates *)
   1.401  
   1.402  fun case_certificate thm =