more uniform operations for structured statements;
authorwenzelm
Tue Apr 26 19:37:47 2016 +0200 (2016-04-26 ago)
changeset 6305750802acac277
parent 63056 9b95ae9ec671
child 63058 8804faa80bc9
more uniform operations for structured statements;
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Apr 26 16:20:28 2016 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Apr 26 19:37:47 2016 +0200
     1.3 @@ -193,13 +193,13 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_obtain prep_statement prep_att that_binding raw_vars raw_asms int state =
     1.8 +fun gen_obtain prep_stmt prep_att that_binding raw_vars raw_asms int state =
     1.9    let
    1.10      val _ = Proof.assert_forward_or_chain state;
    1.11  
    1.12      val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
    1.13      val ((vars, propss, binds, binds'), params_ctxt) =
    1.14 -      prep_statement raw_vars (map #2 raw_asms) thesis_ctxt;
    1.15 +      prep_stmt raw_vars (map #2 raw_asms) thesis_ctxt;
    1.16      val params = map #2 vars;
    1.17      val that_prop =
    1.18        Logic.list_rename_params (map #1 params)
    1.19 @@ -229,8 +229,8 @@
    1.20  
    1.21  in
    1.22  
    1.23 -val obtain = gen_obtain Proof_Context.cert_statement (K I);
    1.24 -val obtain_cmd = gen_obtain Proof_Context.read_statement Attrib.attribute_cmd;
    1.25 +val obtain = gen_obtain Proof_Context.cert_stmt (K I);
    1.26 +val obtain_cmd = gen_obtain Proof_Context.read_stmt Attrib.attribute_cmd;
    1.27  
    1.28  end;
    1.29  
     2.1 --- a/src/Pure/Isar/proof.ML	Tue Apr 26 16:20:28 2016 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Tue Apr 26 19:37:47 2016 +0200
     2.3 @@ -641,61 +641,17 @@
     2.4  end;
     2.5  
     2.6  
     2.7 -(* structured clause *)
     2.8 -
     2.9 -fun export_binds ctxt' ctxt binds =
    2.10 -  let
    2.11 -    val rhss =
    2.12 -      map (the_list o snd) binds
    2.13 -      |> burrow (Variable.export_terms ctxt' ctxt)
    2.14 -      |> map (try the_single);
    2.15 -  in map fst binds ~~ rhss end;
    2.16 -
    2.17 -fun prep_clause prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
    2.18 -  let
    2.19 -    (*fixed variables*)
    2.20 -    val ((xs', vars), fix_ctxt) = ctxt
    2.21 -      |> fold_map prep_var raw_fixes
    2.22 -      |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
    2.23 -
    2.24 -    (*propositions with term bindings*)
    2.25 -    val (all_propss, binds) = prep_propp fix_ctxt (raw_assumes @ raw_shows);
    2.26 -    val (assumes_propss, shows_propss) = chop (length raw_assumes) all_propss;
    2.27 -
    2.28 -    (*params*)
    2.29 -    val (ps, params_ctxt) = fix_ctxt
    2.30 -      |> (fold o fold) Variable.declare_term all_propss
    2.31 -      |> fold Variable.bind_term binds
    2.32 -      |> fold_map Proof_Context.inferred_param xs';
    2.33 -    val xs = map (Variable.check_name o #1) vars;
    2.34 -    val params = xs ~~ map Free ps;
    2.35 -
    2.36 -    val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
    2.37 -
    2.38 -    (*result term bindings*)
    2.39 -    val shows_props = flat shows_propss;
    2.40 -    val binds' =
    2.41 -      (case try List.last shows_props of
    2.42 -        NONE => []
    2.43 -      | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
    2.44 -    val result_binds =
    2.45 -      (Auto_Bind.facts params_ctxt shows_props @ binds')
    2.46 -      |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
    2.47 -      |> export_binds params_ctxt ctxt;
    2.48 -  in ((params, assumes_propss, shows_propss, result_binds), params_ctxt) end;
    2.49 -
    2.50 -
    2.51  (* assume *)
    2.52  
    2.53  local
    2.54  
    2.55 -fun gen_assume prep_var prep_propp prep_att export raw_fixes raw_prems raw_concls state =
    2.56 +fun gen_assume prep_statement prep_att export raw_fixes raw_prems raw_concls state =
    2.57    let
    2.58      val ctxt = context_of state;
    2.59  
    2.60      val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
    2.61      val ((params, prems_propss, concl_propss, result_binds), _) =
    2.62 -      prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt;
    2.63 +      prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
    2.64      val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
    2.65    in
    2.66      state
    2.67 @@ -712,8 +668,8 @@
    2.68  
    2.69  in
    2.70  
    2.71 -val assm = gen_assume Proof_Context.cert_var Proof_Context.cert_propp (K I);
    2.72 -val assm_cmd = gen_assume Proof_Context.read_var Proof_Context.read_propp Attrib.attribute_cmd;
    2.73 +val assm = gen_assume Proof_Context.cert_statement (K I);
    2.74 +val assm_cmd = gen_assume Proof_Context.read_statement Attrib.attribute_cmd;
    2.75  
    2.76  val assume = assm Assumption.assume_export;
    2.77  val assume_cmd = assm_cmd Assumption.assume_export;
    2.78 @@ -889,14 +845,14 @@
    2.79  
    2.80  local
    2.81  
    2.82 -fun gen_define prep_statement prep_att raw_decls raw_fixes raw_defs state =
    2.83 +fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state =
    2.84    let
    2.85      val _ = assert_forward state;
    2.86      val ctxt = context_of state;
    2.87  
    2.88      (*vars*)
    2.89      val ((vars, propss, _, binds'), vars_ctxt) =
    2.90 -      prep_statement (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
    2.91 +      prep_stmt (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
    2.92      val (decls, fixes) = chop (length raw_decls) vars;
    2.93      val show_term = Syntax.string_of_term vars_ctxt;
    2.94  
    2.95 @@ -935,8 +891,8 @@
    2.96  
    2.97  in
    2.98  
    2.99 -val define = gen_define Proof_Context.cert_statement (K I);
   2.100 -val define_cmd = gen_define Proof_Context.read_statement Attrib.attribute_cmd;
   2.101 +val define = gen_define Proof_Context.cert_stmt (K I);
   2.102 +val define_cmd = gen_define Proof_Context.read_stmt Attrib.attribute_cmd;
   2.103  
   2.104  end;
   2.105  
   2.106 @@ -1116,7 +1072,7 @@
   2.107  
   2.108  (* local goals *)
   2.109  
   2.110 -fun local_goal print_results prep_att prep_propp prep_var strict_asm
   2.111 +fun local_goal print_results prep_statement prep_att strict_asm
   2.112      kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
   2.113    let
   2.114      val ctxt = context_of state;
   2.115 @@ -1127,7 +1083,7 @@
   2.116  
   2.117      (*params*)
   2.118      val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
   2.119 -      |> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows);
   2.120 +      |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
   2.121  
   2.122      (*prems*)
   2.123      val (assumes_bindings, shows_bindings) =
   2.124 @@ -1242,18 +1198,16 @@
   2.125  (* common goal statements *)
   2.126  
   2.127  fun internal_goal print_results mode =
   2.128 -  local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
   2.129 -    Proof_Context.cert_var;
   2.130 +  local_goal print_results
   2.131 +    (fn a => fn b => fn c => Proof_Context.cert_statement a b c o Proof_Context.set_mode mode) (K I);
   2.132  
   2.133  local
   2.134  
   2.135 -fun gen_have prep_att prep_propp prep_var
   2.136 -    strict_asm before_qed after_qed fixes assumes shows int =
   2.137 +fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
   2.138    local_goal (Proof_Display.print_results int (Position.thread_data ()))
   2.139 -    prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows;
   2.140 +    prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows;
   2.141  
   2.142 -fun gen_show prep_att prep_propp prep_var
   2.143 -    strict_asm before_qed after_qed fixes assumes shows int state =
   2.144 +fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state =
   2.145    let
   2.146      val testing = Unsynchronized.ref false;
   2.147      val rule = Unsynchronized.ref (NONE: thm option);
   2.148 @@ -1284,7 +1238,7 @@
   2.149        |> after_qed (result_ctxt, results);
   2.150    in
   2.151      state
   2.152 -    |> local_goal print_results prep_att prep_propp prep_var strict_asm
   2.153 +    |> local_goal print_results prep_statement prep_att strict_asm
   2.154        "show" before_qed after_qed' fixes assumes shows
   2.155      ||> int ? (fn goal_state =>
   2.156        (case test_proof (map_context (Context_Position.set_visible false) goal_state) of
   2.157 @@ -1294,10 +1248,10 @@
   2.158  
   2.159  in
   2.160  
   2.161 -val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
   2.162 -val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
   2.163 -val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
   2.164 -val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
   2.165 +val have = gen_have Proof_Context.cert_statement (K I);
   2.166 +val have_cmd = gen_have Proof_Context.read_statement Attrib.attribute_cmd;
   2.167 +val show = gen_show Proof_Context.cert_statement (K I);
   2.168 +val show_cmd = gen_show Proof_Context.read_statement Attrib.attribute_cmd;
   2.169  
   2.170  end;
   2.171  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 26 16:20:28 2016 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 26 19:37:47 2016 +0200
     3.3 @@ -166,14 +166,22 @@
     3.4    val generic_add_abbrev: string -> binding * term -> Context.generic ->
     3.5      (term * term) * Context.generic
     3.6    val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
     3.7 -  val cert_statement:
     3.8 +  val cert_stmt:
     3.9      (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
    3.10      (((binding * typ option * mixfix) * (string * term)) list * term list list *
    3.11        (indexname * term) list * (indexname * term) list) * Proof.context
    3.12 -  val read_statement:
    3.13 +  val read_stmt:
    3.14      (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
    3.15      (((binding * typ option * mixfix) * (string * term)) list * term list list *
    3.16        (indexname * term) list * (indexname * term) list) * Proof.context
    3.17 +  val cert_statement: (binding * typ option * mixfix) list ->
    3.18 +    (term * term list) list list -> (term * term list) list list -> Proof.context ->
    3.19 +    ((string * term) list * term list list * term list list * (indexname * term option) list) *
    3.20 +      Proof.context
    3.21 +  val read_statement: (binding * string option * mixfix) list ->
    3.22 +    (string * string list) list list -> (string * string list) list list -> Proof.context ->
    3.23 +    ((string * term) list * term list list * term list list * (indexname * term option) list) *
    3.24 +      Proof.context
    3.25    val print_syntax: Proof.context -> unit
    3.26    val print_abbrevs: bool -> Proof.context -> unit
    3.27    val pretty_term_bindings: Proof.context -> Pretty.T list
    3.28 @@ -1328,11 +1336,19 @@
    3.29  end;
    3.30  
    3.31  
    3.32 -(* structured statement *)
    3.33 +(* structured statements *)
    3.34  
    3.35  local
    3.36  
    3.37 -fun prep_statement prep_var prep_propp raw_vars raw_propps ctxt =
    3.38 +fun export_binds ctxt' ctxt params binds =
    3.39 +  let
    3.40 +    val rhss =
    3.41 +      map (the_list o Option.map (Logic.close_term params) o snd) binds
    3.42 +      |> burrow (Variable.export_terms ctxt' ctxt)
    3.43 +      |> map (try the_single);
    3.44 +  in map fst binds ~~ rhss end;
    3.45 +
    3.46 +fun prep_stmt prep_var prep_propp raw_vars raw_propps ctxt =
    3.47    let
    3.48      val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
    3.49      val xs = map (Variable.check_name o #1) vars;
    3.50 @@ -1345,13 +1361,33 @@
    3.51      val params = xs ~~ map Free ps;
    3.52  
    3.53      val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
    3.54 -    val binds' = (map o apsnd) (Logic.close_term params) binds;
    3.55 +    val binds' = binds
    3.56 +      |> map (apsnd SOME)
    3.57 +      |> export_binds params_ctxt ctxt params
    3.58 +      |> map (apsnd the);
    3.59  
    3.60      val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
    3.61    in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
    3.62  
    3.63 +fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
    3.64 +  let
    3.65 +    val ((fixes, (assumes, shows), binds), ctxt') = ctxt
    3.66 +      |> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
    3.67 +      |-> (fn (vars, propss, binds, _) =>
    3.68 +        fold Variable.bind_term binds #>
    3.69 +        pair (map #2 vars, chop (length raw_assumes) propss, binds));
    3.70 +    val binds' =
    3.71 +      (Auto_Bind.facts ctxt' (flat shows) @
    3.72 +        (case try List.last (flat shows) of
    3.73 +          NONE => []
    3.74 +        | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
    3.75 +      |> export_binds ctxt' ctxt fixes;
    3.76 +  in ((fixes, assumes, shows, binds'), ctxt') end;
    3.77 +
    3.78  in
    3.79  
    3.80 +val cert_stmt = prep_stmt cert_var cert_propp;
    3.81 +val read_stmt = prep_stmt read_var read_propp;
    3.82  val cert_statement = prep_statement cert_var cert_propp;
    3.83  val read_statement = prep_statement read_var read_propp;
    3.84