added params_of, prems_of;
authorwenzelm
Mon Jun 05 21:54:23 2006 +0200 (2006-06-05)
changeset 1977777929c3d2b74
parent 19776 a8c02d8b8b40
child 19778 f0a318495ca4
added params_of, prems_of;
added type witness (from locale.ML);
misc cleanup;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Mon Jun 05 21:54:22 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Jun 05 21:54:23 2006 +0200
     1.3 @@ -2,7 +2,8 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Explicit data structures for some Isar language elements.
     1.8 +Explicit data structures for some Isar language elements, with derived
     1.9 +logical operations.
    1.10  *)
    1.11  
    1.12  signature ELEMENT =
    1.13 @@ -25,28 +26,49 @@
    1.14      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
    1.15      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
    1.16    val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
    1.17 +  val params_of: ('typ, 'term, 'fact) ctxt -> (string * 'typ) list
    1.18 +  val prems_of: ('typ, 'term, 'fact) ctxt -> 'term list
    1.19 +  val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
    1.20 +  val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
    1.21 +  val pretty_statement: Proof.context -> string -> thm -> Pretty.T
    1.22 +
    1.23 +  type witness
    1.24 +  val map_witness: (term * thm -> term * thm) -> witness -> witness
    1.25 +  val witness_prop: witness -> term
    1.26 +  val witness_hyps: witness -> term list
    1.27 +  val assume_witness: theory -> term -> witness
    1.28 +  val prove_witness: theory -> term -> tactic -> witness
    1.29 +  val conclude_witness: witness -> thm
    1.30 +  val mark_witness: term -> term
    1.31 +  val make_witness: term -> thm -> witness
    1.32 +  val refine_witness: Proof.state -> Proof.state
    1.33 +
    1.34    val rename: (string * (string * mixfix option)) list -> string -> string
    1.35    val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
    1.36    val rename_term: (string * (string * mixfix option)) list -> term -> term
    1.37    val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
    1.38 +  val rename_witness: (string * (string * mixfix option)) list -> witness -> witness
    1.39    val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i
    1.40    val instT_type: typ Symtab.table -> typ -> typ
    1.41    val instT_term: typ Symtab.table -> term -> term
    1.42    val instT_thm: theory -> typ Symtab.table -> thm -> thm
    1.43 +  val instT_witness: theory -> typ Symtab.table -> witness -> witness
    1.44    val instT_ctxt: theory -> typ Symtab.table -> context_i -> context_i
    1.45    val inst_term: typ Symtab.table * term Symtab.table -> term -> term
    1.46    val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
    1.47 +  val inst_witness: theory -> typ Symtab.table * term Symtab.table -> witness -> witness
    1.48    val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
    1.49 -  val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list
    1.50 -  val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
    1.51 -  val pretty_statement: ProofContext.context -> string -> thm -> Pretty.T
    1.52 +  val satisfy_thm: witness list -> thm -> thm
    1.53 +  val satisfy_witness: witness list -> witness -> witness
    1.54  end;
    1.55  
    1.56  structure Element: ELEMENT =
    1.57  struct
    1.58  
    1.59  
    1.60 -(** conclusions **)
    1.61 +(** language elements **)
    1.62 +
    1.63 +(* statement *)
    1.64  
    1.65  datatype ('typ, 'term) stmt =
    1.66    Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
    1.67 @@ -56,10 +78,7 @@
    1.68  type statement_i = (typ, term) stmt;
    1.69  
    1.70  
    1.71 -
    1.72 -(** context elements **)
    1.73 -
    1.74 -(* datatype ctxt *)
    1.75 +(* context *)
    1.76  
    1.77  datatype ('typ, 'term, 'fact) ctxt =
    1.78    Fixes of (string * 'typ option * mixfix) list |
    1.79 @@ -86,144 +105,14 @@
    1.80    {name = I, var = I, typ = typ, term = term, fact = map thm,
    1.81      attrib = Args.map_values I typ term thm};
    1.82  
    1.83 -
    1.84 -
    1.85 -(** logical operations **)
    1.86 -
    1.87 -(* derived rules *)
    1.88 -
    1.89 -fun instantiate_tfrees thy subst =
    1.90 -  let
    1.91 -    val certT = Thm.ctyp_of thy;
    1.92 -    fun inst vs (a, T) = AList.lookup (op =) vs a
    1.93 -      |> Option.map (fn v => (certT (TVar v), certT T));
    1.94 -  in
    1.95 -    Drule.tvars_intr_list (map fst subst) #->
    1.96 -    (fn vs => Thm.instantiate (map_filter (inst vs) subst, []))
    1.97 -  end;
    1.98 -
    1.99 -fun instantiate_frees thy subst =
   1.100 -  let val cert = Thm.cterm_of thy in
   1.101 -    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
   1.102 -    Drule.forall_elim_list (map (cert o snd) subst)
   1.103 -  end;
   1.104 -
   1.105 -fun hyps_rule rule th =
   1.106 -  let
   1.107 -    val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1;
   1.108 -    val {hyps, ...} = Thm.crep_thm th;
   1.109 -  in
   1.110 -    Drule.implies_elim_list
   1.111 -      (rule (Drule.implies_intr_list hyps th))
   1.112 -      (map (Thm.assume o cterm_rule) hyps)
   1.113 -  end;
   1.114 -
   1.115 -
   1.116 -(* renaming *)
   1.117 -
   1.118 -fun rename ren x =
   1.119 -  (case AList.lookup (op =) ren (x: string) of
   1.120 -    NONE => x
   1.121 -  | SOME (x', _) => x');
   1.122 -
   1.123 -fun rename_var ren (x, mx) =
   1.124 -  (case (AList.lookup (op =) ren (x: string), mx) of
   1.125 -    (NONE, _) => (x, mx)
   1.126 -  | (SOME (x', NONE), Structure) => (x', mx)
   1.127 -  | (SOME (x', SOME _), Structure) =>
   1.128 -      error ("Attempt to change syntax of structure parameter " ^ quote x)
   1.129 -  | (SOME (x', NONE), _) => (x', NoSyn)
   1.130 -  | (SOME (x', SOME mx'), _) => (x', mx'));
   1.131 -
   1.132 -fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
   1.133 -  | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
   1.134 -  | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
   1.135 -  | rename_term _ a = a;
   1.136 -
   1.137 -fun rename_thm ren th =
   1.138 -  let
   1.139 -    val subst = Drule.frees_of th
   1.140 -      |> map_filter (fn (x, T) =>
   1.141 -        let val x' = rename ren x
   1.142 -        in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end);
   1.143 -  in
   1.144 -    if null subst then th
   1.145 -    else th |> hyps_rule (instantiate_frees (Thm.theory_of_thm th) subst)
   1.146 -  end;
   1.147 -
   1.148 -fun rename_ctxt ren =
   1.149 -  map_ctxt_values I (rename_term ren) (rename_thm ren)
   1.150 -  #> map_ctxt {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
   1.151 +fun params_of (Fixes fixes) = fixes |> map
   1.152 +    (fn (x, SOME T, _) => (x, T)
   1.153 +      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote x, []))
   1.154 +  | params_of _ = [];
   1.155  
   1.156 -
   1.157 -(* type instantiation *)
   1.158 -
   1.159 -fun instT_type env =
   1.160 -  if Symtab.is_empty env then I
   1.161 -  else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x));
   1.162 -
   1.163 -fun instT_term env =
   1.164 -  if Symtab.is_empty env then I
   1.165 -  else Term.map_term_types (instT_type env);
   1.166 -
   1.167 -fun instT_subst env th =
   1.168 -  Drule.tfrees_of th
   1.169 -  |> map_filter (fn (a, S) =>
   1.170 -    let
   1.171 -      val T = TFree (a, S);
   1.172 -      val T' = the_default T (Symtab.lookup env a);
   1.173 -    in if T = T' then NONE else SOME (a, T') end);
   1.174 -
   1.175 -fun instT_thm thy env th =
   1.176 -  if Symtab.is_empty env then th
   1.177 -  else
   1.178 -    let val subst = instT_subst env th
   1.179 -    in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
   1.180 -
   1.181 -fun instT_ctxt thy env =
   1.182 -  map_ctxt_values (instT_type env) (instT_term env) (instT_thm thy env);
   1.183 -
   1.184 -
   1.185 -(* type and term instantiation *)
   1.186 -
   1.187 -fun inst_term (envT, env) =
   1.188 -  if Symtab.is_empty env then instT_term envT
   1.189 -  else
   1.190 -    let
   1.191 -      val instT = instT_type envT;
   1.192 -      fun inst (Const (x, T)) = Const (x, instT T)
   1.193 -        | inst (Free (x, T)) =
   1.194 -            (case Symtab.lookup env x of
   1.195 -              NONE => Free (x, instT T)
   1.196 -            | SOME t => t)
   1.197 -        | inst (Var (xi, T)) = Var (xi, instT T)
   1.198 -        | inst (b as Bound _) = b
   1.199 -        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
   1.200 -        | inst (t $ u) = inst t $ inst u;
   1.201 -    in Envir.beta_norm o inst end;
   1.202 -
   1.203 -fun inst_thm thy (envT, env) th =
   1.204 -  if Symtab.is_empty env then instT_thm thy envT th
   1.205 -  else
   1.206 -    let
   1.207 -      val substT = instT_subst envT th;
   1.208 -      val subst = Drule.frees_of th
   1.209 -        |> map_filter (fn (x, T) =>
   1.210 -          let
   1.211 -            val T' = instT_type envT T;
   1.212 -            val t = Free (x, T');
   1.213 -            val t' = the_default t (Symtab.lookup env x);
   1.214 -          in if t aconv t' then NONE else SOME ((x, T'), t') end);
   1.215 -    in
   1.216 -      if null substT andalso null subst then th
   1.217 -      else th |> hyps_rule
   1.218 -       (instantiate_tfrees thy substT #>
   1.219 -        instantiate_frees thy subst #>
   1.220 -        Drule.fconv_rule (Thm.beta_conversion true))
   1.221 -    end;
   1.222 -
   1.223 -fun inst_ctxt thy envs =
   1.224 -  map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs);
   1.225 +fun prems_of (Assumes asms) = maps (map fst o snd) asms
   1.226 +  | prems_of (Defines defs) = map (fst o snd) defs
   1.227 +  | prems_of _ = [];
   1.228  
   1.229  
   1.230  
   1.231 @@ -357,4 +246,193 @@
   1.232  
   1.233  end;
   1.234  
   1.235 +
   1.236 +
   1.237 +(** logical operations **)
   1.238 +
   1.239 +(* witnesses -- hypotheses as protected facts *)
   1.240 +
   1.241 +datatype witness = Witness of term * thm;
   1.242 +
   1.243 +fun map_witness f (Witness witn) = Witness (f witn);
   1.244 +
   1.245 +fun witness_prop (Witness (t, _)) = t;
   1.246 +fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
   1.247 +
   1.248 +fun assume_witness thy t =
   1.249 +  Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
   1.250 +
   1.251 +fun prove_witness thy t tac =
   1.252 +  Witness (t, Goal.prove thy [] [] (Logic.protect t) (fn _ =>
   1.253 +    Tactic.rtac Drule.protectI 1 THEN tac));
   1.254 +
   1.255 +fun conclude_witness (Witness (_, th)) = Goal.norm_hhf (Goal.conclude th);
   1.256 +
   1.257 +val mark_witness = Logic.protect;
   1.258 +
   1.259 +fun make_witness t th = Witness (t, th);
   1.260 +
   1.261 +val refine_witness =
   1.262 +  Proof.refine (Method.Basic (K (Method.RAW_METHOD
   1.263 +    (K (ALLGOALS
   1.264 +      (PRECISE_CONJUNCTS ~1 (ALLGOALS
   1.265 +        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))))
   1.266 +  #> Seq.hd;
   1.267 +
   1.268 +
   1.269 +(* derived rules *)
   1.270 +
   1.271 +fun instantiate_tfrees thy subst =
   1.272 +  let
   1.273 +    val certT = Thm.ctyp_of thy;
   1.274 +    fun inst vs (a, T) = AList.lookup (op =) vs a
   1.275 +      |> Option.map (fn v => (certT (TVar v), certT T));
   1.276 +  in
   1.277 +    Drule.tvars_intr_list (map fst subst) #->
   1.278 +    (fn vs => Thm.instantiate (map_filter (inst vs) subst, []))
   1.279 +  end;
   1.280 +
   1.281 +fun instantiate_frees thy subst =
   1.282 +  let val cert = Thm.cterm_of thy in
   1.283 +    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
   1.284 +    Drule.forall_elim_list (map (cert o snd) subst)
   1.285 +  end;
   1.286 +
   1.287 +fun hyps_rule rule th =
   1.288 +  let
   1.289 +    val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1;
   1.290 +    val {hyps, ...} = Thm.crep_thm th;
   1.291 +  in
   1.292 +    Drule.implies_elim_list
   1.293 +      (rule (Drule.implies_intr_list hyps th))
   1.294 +      (map (Thm.assume o cterm_rule) hyps)
   1.295 +  end;
   1.296 +
   1.297 +
   1.298 +(* rename *)
   1.299 +
   1.300 +fun rename ren x =
   1.301 +  (case AList.lookup (op =) ren (x: string) of
   1.302 +    NONE => x
   1.303 +  | SOME (x', _) => x');
   1.304 +
   1.305 +fun rename_var ren (x, mx) =
   1.306 +  (case (AList.lookup (op =) ren (x: string), mx) of
   1.307 +    (NONE, _) => (x, mx)
   1.308 +  | (SOME (x', NONE), Structure) => (x', mx)
   1.309 +  | (SOME (x', SOME _), Structure) =>
   1.310 +      error ("Attempt to change syntax of structure parameter " ^ quote x)
   1.311 +  | (SOME (x', NONE), _) => (x', NoSyn)
   1.312 +  | (SOME (x', SOME mx'), _) => (x', mx'));
   1.313 +
   1.314 +fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
   1.315 +  | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
   1.316 +  | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
   1.317 +  | rename_term _ a = a;
   1.318 +
   1.319 +fun rename_thm ren th =
   1.320 +  let
   1.321 +    val subst = Drule.frees_of th
   1.322 +      |> map_filter (fn (x, T) =>
   1.323 +        let val x' = rename ren x
   1.324 +        in if x = x' then NONE else SOME ((x, T), (Free (x', T))) end);
   1.325 +  in
   1.326 +    if null subst then th
   1.327 +    else th |> hyps_rule (instantiate_frees (Thm.theory_of_thm th) subst)
   1.328 +  end;
   1.329 +
   1.330 +fun rename_witness ren =
   1.331 +  map_witness (fn (t, th) => (rename_term ren t, rename_thm ren th));
   1.332 +
   1.333 +fun rename_ctxt ren =
   1.334 +  map_ctxt_values I (rename_term ren) (rename_thm ren)
   1.335 +  #> map_ctxt {name = I, typ = I, term = I, fact = I, attrib = I, var = rename_var ren};
   1.336 +
   1.337 +
   1.338 +(* instantiate types *)
   1.339 +
   1.340 +fun instT_type env =
   1.341 +  if Symtab.is_empty env then I
   1.342 +  else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x));
   1.343 +
   1.344 +fun instT_term env =
   1.345 +  if Symtab.is_empty env then I
   1.346 +  else Term.map_term_types (instT_type env);
   1.347 +
   1.348 +fun instT_subst env th =
   1.349 +  Drule.tfrees_of th
   1.350 +  |> map_filter (fn (a, S) =>
   1.351 +    let
   1.352 +      val T = TFree (a, S);
   1.353 +      val T' = the_default T (Symtab.lookup env a);
   1.354 +    in if T = T' then NONE else SOME (a, T') end);
   1.355 +
   1.356 +fun instT_thm thy env th =
   1.357 +  if Symtab.is_empty env then th
   1.358 +  else
   1.359 +    let val subst = instT_subst env th
   1.360 +    in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
   1.361 +
   1.362 +fun instT_witness thy env =
   1.363 +  map_witness (fn (t, th) => (instT_term env t, instT_thm thy env th));
   1.364 +
   1.365 +fun instT_ctxt thy env =
   1.366 +  map_ctxt_values (instT_type env) (instT_term env) (instT_thm thy env);
   1.367 +
   1.368 +
   1.369 +(* instantiate types and terms *)
   1.370 +
   1.371 +fun inst_term (envT, env) =
   1.372 +  if Symtab.is_empty env then instT_term envT
   1.373 +  else
   1.374 +    let
   1.375 +      val instT = instT_type envT;
   1.376 +      fun inst (Const (x, T)) = Const (x, instT T)
   1.377 +        | inst (Free (x, T)) =
   1.378 +            (case Symtab.lookup env x of
   1.379 +              NONE => Free (x, instT T)
   1.380 +            | SOME t => t)
   1.381 +        | inst (Var (xi, T)) = Var (xi, instT T)
   1.382 +        | inst (b as Bound _) = b
   1.383 +        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
   1.384 +        | inst (t $ u) = inst t $ inst u;
   1.385 +    in Envir.beta_norm o inst end;
   1.386 +
   1.387 +fun inst_thm thy (envT, env) th =
   1.388 +  if Symtab.is_empty env then instT_thm thy envT th
   1.389 +  else
   1.390 +    let
   1.391 +      val substT = instT_subst envT th;
   1.392 +      val subst = Drule.frees_of th
   1.393 +        |> map_filter (fn (x, T) =>
   1.394 +          let
   1.395 +            val T' = instT_type envT T;
   1.396 +            val t = Free (x, T');
   1.397 +            val t' = the_default t (Symtab.lookup env x);
   1.398 +          in if t aconv t' then NONE else SOME ((x, T'), t') end);
   1.399 +    in
   1.400 +      if null substT andalso null subst then th
   1.401 +      else th |> hyps_rule
   1.402 +       (instantiate_tfrees thy substT #>
   1.403 +        instantiate_frees thy subst #>
   1.404 +        Drule.fconv_rule (Thm.beta_conversion true))
   1.405 +    end;
   1.406 +
   1.407 +fun inst_witness thy envs =
   1.408 +  map_witness (fn (t, th) => (inst_term envs t, inst_thm thy envs th));
   1.409 +
   1.410 +fun inst_ctxt thy envs =
   1.411 +  map_ctxt_values (instT_type (#1 envs)) (inst_term envs) (inst_thm thy envs);
   1.412 +
   1.413 +
   1.414 +(* satisfy hypotheses *)
   1.415 +
   1.416 +fun satisfy_thm witns thm = thm |> fold (fn hyp =>
   1.417 +    (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
   1.418 +      NONE => I
   1.419 +    | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> Goal.comp_hhf th))
   1.420 +  (#hyps (Thm.crep_thm thm));
   1.421 +
   1.422 +fun satisfy_witness witns = map_witness (apsnd (satisfy_thm witns));
   1.423 +
   1.424  end;