term_pat vs. prop_pat;
authorwenzelm
Thu Nov 19 11:46:24 1998 +0100 (1998-11-19)
changeset 59356a82c8a1808f
parent 5934 ecc224b81f7f
child 5936 406eb27fe53c
term_pat vs. prop_pat;
added bind_propp(_i);
assume: propp;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Nov 19 11:45:26 1998 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Nov 19 11:46:24 1998 +0100
     1.3 @@ -28,7 +28,8 @@
     1.4    val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
     1.5    val read_term: context -> string -> term
     1.6    val read_prop: context -> string -> term
     1.7 -  val read_pat: context -> string -> term
     1.8 +  val read_term_pat: context -> string -> term
     1.9 +  val read_prop_pat: context -> string -> term
    1.10    val cert_term: context -> term -> term
    1.11    val cert_prop: context -> term -> term
    1.12    val declare_term: term -> context -> context
    1.13 @@ -36,8 +37,10 @@
    1.14    val declare_thm: thm -> context -> context
    1.15    val add_binds: (indexname * string) list -> context -> context
    1.16    val add_binds_i: (indexname * term) list -> context -> context
    1.17 -  val match_binds: (string * string) list -> context -> context
    1.18 -  val match_binds_i: (term * term) list -> context -> context
    1.19 +  val match_binds: (string list * string) list -> context -> context
    1.20 +  val match_binds_i: (term list * term) list -> context -> context
    1.21 +  val bind_propp: context * (string * string list) -> context * term
    1.22 +  val bind_propp_i: context * (term * term list) -> context * term
    1.23    val thms_closure: context -> xstring -> tthm list option
    1.24    val get_tthm: context -> string -> tthm
    1.25    val get_tthms: context -> string -> tthm list
    1.26 @@ -49,9 +52,9 @@
    1.27      -> (tthm list * context attribute list) list -> context -> context * (string * tthm list)
    1.28    val assumptions: context -> tthm list
    1.29    val fixed_names: context -> string list
    1.30 -  val assume: string -> context attribute list -> string list -> context
    1.31 +  val assume: string -> context attribute list -> (string * string list) list -> context
    1.32      -> context * (string * tthm list)
    1.33 -  val assume_i: string -> context attribute list -> term list -> context
    1.34 +  val assume_i: string -> context attribute list -> (term * term list) list -> context
    1.35      -> context * (string * tthm list)
    1.36    val fix: (string * string option) list -> context -> context
    1.37    val fix_i: (string * typ) list -> context -> context
    1.38 @@ -402,7 +405,8 @@
    1.39  val read_termTs = gen_read (read_def_termTs false) (apfst o map) false;
    1.40  val read_term = gen_read read_term_sg I false;
    1.41  val read_prop = gen_read read_prop_sg I false;
    1.42 -val read_pat = gen_read read_term_sg I true;
    1.43 +val read_term_pat = gen_read read_term_sg I true;
    1.44 +val read_prop_pat = gen_read read_prop_sg I true;
    1.45  
    1.46  
    1.47  (* certify terms *)
    1.48 @@ -414,7 +418,8 @@
    1.49  
    1.50  val cert_term = gen_cert cert_term_sg false;
    1.51  val cert_prop = gen_cert cert_prop_sg false;
    1.52 -val cert_pat = gen_cert cert_term_sg true;
    1.53 +val cert_term_pat = gen_cert cert_term_sg true;
    1.54 +val cert_prop_pat = gen_cert cert_prop_sg true;
    1.55  
    1.56  
    1.57  (* declare terms *)
    1.58 @@ -453,10 +458,6 @@
    1.59    let val {prop, hyps, ...} = Thm.rep_thm thm
    1.60    in ctxt |> declare_terms (prop :: hyps) end;
    1.61  
    1.62 -fun prep_declare prep (ctxt, s) =
    1.63 -  let val t = prep ctxt s
    1.64 -  in (ctxt |> declare_term t, t) end;
    1.65 -
    1.66  
    1.67  
    1.68  (** bindings **)
    1.69 @@ -492,25 +493,37 @@
    1.70  
    1.71  (* match_binds(_i) -- parallel *)
    1.72  
    1.73 -fun prep_pair prep_pat prep (ctxt, (raw_pat, raw_t)) =
    1.74 -  let
    1.75 -    val pat = prep_pat ctxt raw_pat;
    1.76 -    val (ctxt', t) = prep_declare prep (ctxt, raw_t);
    1.77 -  in (ctxt', (pat, t)) end;
    1.78 -
    1.79 -fun gen_match_binds prep_pat prep raw_pairs ctxt =
    1.80 +fun prep_declare_match (prep_pat, prep) (ctxt, (raw_pats, raw_t)) =
    1.81    let
    1.82 -    val (ctxt', pairs) = foldl_map (prep_pair prep_pat prep) (ctxt, raw_pairs);
    1.83 -    val Context {defs = (_, _, maxidx, _), ...} = ctxt';
    1.84 -    val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs);
    1.85 -    val env =
    1.86 -      (case Seq.pull envs of
    1.87 -        None => raise CONTEXT ("Pattern match failed!", ctxt')
    1.88 -      | Some (env, _) => env);
    1.89 -  in ctxt' |> update_binds_env env end;
    1.90 +    val pats = map (prep_pat ctxt) raw_pats;		(* FIXME seq / par / simult (??) *)
    1.91 +    val t = prep ctxt raw_t;
    1.92 +  in (ctxt |> declare_term t, (map (rpair t) pats, t)) end;
    1.93  
    1.94 -val match_binds = gen_match_binds read_pat read_term;
    1.95 -val match_binds_i = gen_match_binds cert_pat cert_term;
    1.96 +fun gen_match_binds _ [] ctxt = ctxt
    1.97 +  | gen_match_binds prepp raw_pairs ctxt =
    1.98 +      let
    1.99 +        val (ctxt', matches) = foldl_map (prep_declare_match prepp) (ctxt, raw_pairs);
   1.100 +        val pairs = flat (map #1 matches);
   1.101 +        val Context {defs = (_, _, maxidx, _), ...} = ctxt';
   1.102 +        val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs);
   1.103 +        val env =
   1.104 +          (case Seq.pull envs of
   1.105 +            None => raise CONTEXT ("Pattern match failed!", ctxt')
   1.106 +          | Some (env, _) => env);
   1.107 +      in ctxt' |> update_binds_env env end;
   1.108 +
   1.109 +val match_binds = gen_match_binds (read_term_pat, read_term);
   1.110 +val match_binds_i = gen_match_binds (cert_term_pat, cert_term);
   1.111 +
   1.112 +
   1.113 +(* bind proposition patterns *)
   1.114 +
   1.115 +fun gen_bind_propp prepp (ctxt, (raw_prop, raw_pats)) =
   1.116 +  let val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop))
   1.117 +  in (ctxt' |> match_binds_i (map (apfst single) pairs), prop) end;
   1.118 +
   1.119 +val bind_propp = gen_bind_propp (read_prop_pat, read_prop);
   1.120 +val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop);
   1.121  
   1.122  
   1.123  
   1.124 @@ -579,9 +592,9 @@
   1.125  
   1.126  (* assume *)
   1.127  
   1.128 -fun gen_assume prep name attrs raw_props ctxt =
   1.129 +fun gen_assume prepp name attrs raw_prop_pats ctxt =
   1.130    let
   1.131 -    val (ctxt', props) = foldl_map prep (ctxt, raw_props);
   1.132 +    val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
   1.133      val sign = sign_of ctxt';
   1.134  
   1.135      val asms = map (Attribute.tthm_of o Thm.assume o Thm.cterm_of sign) props;
   1.136 @@ -597,8 +610,8 @@
   1.137          (thy, data, (assumes @ [(name, asms)], fixes), binds, thms, defs));
   1.138    in (ctxt''', (name, tthms)) end;
   1.139  
   1.140 -val assume = gen_assume (prep_declare read_prop);
   1.141 -val assume_i = gen_assume (prep_declare cert_prop);
   1.142 +val assume = gen_assume bind_propp;
   1.143 +val assume_i = gen_assume bind_propp_i;
   1.144  
   1.145  
   1.146  (* fix *)