uniform handling of fixes;
authorwenzelm
Fri Jan 13 01:13:11 2006 +0100 (2006-01-13)
changeset 18670c3f445b92aff
parent 18669 cd6d6baf0411
child 18671 621efeed255b
uniform handling of fixes;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/specification.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jan 13 01:13:08 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 13 01:13:11 2006 +0100
     1.3 @@ -177,15 +177,13 @@
     1.4  
     1.5  (* constant definitions *)
     1.6  
     1.7 -val vars = P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ));
     1.8 -
     1.9  val structs =
    1.10 -  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (vars --| P.$$$ ")")) [];
    1.11 +  Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
    1.12  
    1.13  val constdecl =
    1.14 -  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, Syntax.NoSyn)) ||
    1.15 +  (P.name --| P.$$$ "where") >> (fn x => (x, NONE, NoSyn)) ||
    1.16      P.name -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix' >> P.triple1 ||
    1.17 -    P.name -- (P.mixfix' >> pair NONE) >> P.triple2;
    1.18 +    P.name -- (P.mixfix >> pair NONE) >> P.triple2;
    1.19  val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
    1.20  
    1.21  val constdefsP =
    1.22 @@ -197,7 +195,7 @@
    1.23  
    1.24  val axiomatizationP =
    1.25    OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
    1.26 -    (P.and_list1 P.param -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
    1.27 +    (P.fixes -- Scan.optional (P.$$$ "where" |-- P.!!! (P.and_list1 P.named_spec)) []
    1.28      >> (Toplevel.theory o (#2 oo Specification.axiomatize)));
    1.29  
    1.30  
    1.31 @@ -254,7 +252,7 @@
    1.32  
    1.33  val setupP =
    1.34    OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
    1.35 -    (P.text >> (Toplevel.theory o PureThy.generic_setup));
    1.36 +    (Scan.option P.text >> (Toplevel.theory o PureThy.generic_setup));
    1.37  
    1.38  val method_setupP =
    1.39    OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
    1.40 @@ -316,7 +314,8 @@
    1.41    OuterSyntax.command "locale" "define named proof context" K.thy_decl
    1.42      ((P.opt_keyword "open" >> not) -- P.name
    1.43          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    1.44 -      >> (Toplevel.theory_context o (fn ((x, y), (z, w)) => Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
    1.45 +      >> (Toplevel.theory_context o (fn ((x, y), (z, w)) =>
    1.46 +          Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
    1.47  
    1.48  val opt_inst =
    1.49    Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
    1.50 @@ -418,7 +417,7 @@
    1.51  val fixP =
    1.52    OuterSyntax.command "fix" "fix local variables (Skolem constants)"
    1.53      (K.tag_proof K.prf_asm)
    1.54 -    (vars >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
    1.55 +    (P.simple_fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix)));
    1.56  
    1.57  val assumeP =
    1.58    OuterSyntax.command "assume" "assume propositions"
    1.59 @@ -440,16 +439,13 @@
    1.60  val obtainP =
    1.61    OuterSyntax.command "obtain" "generalized existence"
    1.62      (K.tag_proof K.prf_asm_goal)
    1.63 -    (Scan.optional
    1.64 -      (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
    1.65 -        --| P.$$$ "where") [] -- statement
    1.66 +    (Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- statement
    1.67        >> (Toplevel.print oo (Toplevel.proof' o uncurry Obtain.obtain)));
    1.68  
    1.69  val guessP =
    1.70    OuterSyntax.command "guess" "wild guessing (unstructured)"
    1.71      (K.tag_proof K.prf_asm_goal)
    1.72 -    (P.and_list (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
    1.73 -      >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
    1.74 +    (Scan.optional P.simple_fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess)));
    1.75  
    1.76  val letP =
    1.77    OuterSyntax.command "let" "bind text variables"
    1.78 @@ -651,13 +647,14 @@
    1.79  
    1.80  val print_localeP =
    1.81    OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
    1.82 -    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
    1.83 +    (Scan.optional (P.$$$ "!" >> K true) false -- locale_val
    1.84 +      >> (Toplevel.no_timing oo IsarCmd.print_locale));
    1.85  
    1.86  val print_registrationsP =
    1.87    OuterSyntax.improper_command "print_interps"
    1.88      "print interpretations of named locale" K.diag
    1.89 -    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname >>
    1.90 -      (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
    1.91 +    (Scan.optional (P.$$$ "!" >> K true) false -- P.xname
    1.92 +      >> (Toplevel.no_timing oo uncurry IsarCmd.print_registrations));
    1.93  
    1.94  val print_attributesP =
    1.95    OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
     2.1 --- a/src/Pure/Isar/obtain.ML	Fri Jan 13 01:13:08 2006 +0100
     2.2 +++ b/src/Pure/Isar/obtain.ML	Fri Jan 13 01:13:11 2006 +0100
     2.3 @@ -36,22 +36,23 @@
     2.4  
     2.5  signature OBTAIN =
     2.6  sig
     2.7 -  val obtain: (string list * string option) list ->
     2.8 +  val obtain: (string * string option) list ->
     2.9      ((string * Attrib.src list) * (string * (string list * string list)) list) list
    2.10      -> bool -> Proof.state -> Proof.state
    2.11 -  val obtain_i: (string list * typ option) list ->
    2.12 +  val obtain_i: (string * typ option) list ->
    2.13      ((string * Proof.context attribute list) * (term * (term list * term list)) list) list
    2.14      -> bool -> Proof.state -> Proof.state
    2.15 -  val guess: (string list * string option) list -> bool -> Proof.state -> Proof.state
    2.16 -  val guess_i: (string list * typ option) list -> bool -> Proof.state -> Proof.state
    2.17 +  val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
    2.18 +  val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
    2.19  end;
    2.20  
    2.21  structure Obtain: OBTAIN =
    2.22  struct
    2.23  
    2.24 -(** export_obtained **)
    2.25  
    2.26 -fun export_obtained state parms rule cprops thm =
    2.27 +(** obtain_export **)
    2.28 +
    2.29 +fun obtain_export state parms rule cprops thm =
    2.30    let
    2.31      val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
    2.32      val cparms = map (Thm.cterm_of thy) parms;
    2.33 @@ -78,9 +79,9 @@
    2.34  (** obtain **)
    2.35  
    2.36  fun bind_judgment ctxt name =
    2.37 -  let val (t as _ $ Free v) =
    2.38 -    ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name
    2.39 -    |> ProofContext.bind_skolem ctxt [name]
    2.40 +  let
    2.41 +    val (bind, _) = ProofContext.bind_fixes [name] ctxt;
    2.42 +    val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
    2.43    in (v, t) end;
    2.44  
    2.45  local
    2.46 @@ -94,9 +95,10 @@
    2.47      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    2.48  
    2.49      (*obtain vars*)
    2.50 -    val (vars, vars_ctxt) = fold_map prep_vars raw_vars ctxt;
    2.51 -    val fix_ctxt = vars_ctxt |> ProofContext.fix_i vars;
    2.52 -    val xs = List.concat (map fst vars);
    2.53 +    val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
    2.54 +    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    2.55 +    val xs = map #1 vars;
    2.56 +    val Ts = map #2 vars;
    2.57  
    2.58      (*obtain asms*)
    2.59      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    2.60 @@ -126,14 +128,14 @@
    2.61      fun after_qed _ =
    2.62        Proof.local_qed (NONE, false)
    2.63        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    2.64 -        Proof.fix_i vars
    2.65 -        #> Proof.assm_i (K (export_obtained state parms rule)) asms));
    2.66 +        Proof.fix_i (xs ~~ Ts)
    2.67 +        #> Proof.assm_i (K (obtain_export state parms rule)) asms));
    2.68    in
    2.69      state
    2.70      |> Proof.enter_forward
    2.71      |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
    2.72      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
    2.73 -    |> Proof.fix_i [([thesisN], NONE)]
    2.74 +    |> Proof.fix_i [(thesisN, NONE)]
    2.75      |> Proof.assume_i
    2.76        [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])]
    2.77      |> `Proof.the_facts
    2.78 @@ -205,8 +207,7 @@
    2.79      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    2.80  
    2.81      val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
    2.82 -    val varss = #1 (fold_map prep_vars raw_vars ctxt);
    2.83 -    val vars = List.concat (map (fn (xs, T) => map (rpair T) xs) varss);
    2.84 +    val (vars, _) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
    2.85  
    2.86      fun check_result th =
    2.87        (case Thm.prems_of th of
    2.88 @@ -221,8 +222,9 @@
    2.89  
    2.90      fun guess_context raw_rule =
    2.91        let
    2.92 -        val (parms, rule) = match_params state vars raw_rule;
    2.93 -        val ts = map (ProofContext.bind_skolem ctxt (map #1 parms) o Free) parms;
    2.94 +        val (parms, rule) = match_params state (map (fn (x, T, _) => (x, T)) vars) raw_rule;
    2.95 +        val (bind, _) = ProofContext.bind_fixes (map #1 parms) ctxt;
    2.96 +        val ts = map (bind o Free) parms;
    2.97          val ps = map dest_Free ts;
    2.98          val asms =
    2.99            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   2.100 @@ -230,8 +232,8 @@
   2.101          val _ = conditional (null asms) (fn () =>
   2.102            raise Proof.STATE ("Trivial result -- nothing guessed", state));
   2.103        in
   2.104 -        Proof.fix_i (map (fn (x, T) => ([x], SOME T)) parms)
   2.105 -        #> Proof.assm_i (K (export_obtained state ts rule)) [(("", []), asms)]
   2.106 +        Proof.fix_i (map (apsnd SOME) parms)
   2.107 +        #> Proof.assm_i (K (obtain_export state ts rule)) [(("", []), asms)]
   2.108          #> Proof.add_binds_i AutoBind.no_facts
   2.109        end;
   2.110  
   2.111 @@ -242,7 +244,7 @@
   2.112      state
   2.113      |> Proof.enter_forward
   2.114      |> Proof.begin_block
   2.115 -    |> Proof.fix_i [([AutoBind.thesisN], NONE)]
   2.116 +    |> Proof.fix_i [(AutoBind.thesisN, NONE)]
   2.117      |> Proof.chain_facts chain_facts
   2.118      |> Proof.local_goal (ProofDisplay.print_results int) (K I) (apsnd (rpair I))
   2.119        "guess" before_qed after_qed [(("", []), [Var (("guess", 0), propT)])]
     3.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 13 01:13:08 2006 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Fri Jan 13 01:13:11 2006 +0100
     3.3 @@ -42,12 +42,12 @@
     3.4    val match_bind_i: (term list * term) list -> state -> state
     3.5    val let_bind: (string list * string) list -> state -> state
     3.6    val let_bind_i: (term list * term) list -> state -> state
     3.7 -  val fix: (string list * string option) list -> state -> state
     3.8 -  val fix_i: (string list * typ option) list -> state -> state
     3.9 -  val assm: ProofContext.exporter ->
    3.10 +  val fix: (string * string option) list -> state -> state
    3.11 +  val fix_i: (string * typ option) list -> state -> state
    3.12 +  val assm: ProofContext.export ->
    3.13      ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    3.14      state -> state
    3.15 -  val assm_i: ProofContext.exporter ->
    3.16 +  val assm_i: ProofContext.export ->
    3.17      ((string * context attribute list) * (term * (term list * term list)) list) list
    3.18      -> state -> state
    3.19    val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    3.20 @@ -359,7 +359,7 @@
    3.21  
    3.22      val prt_ctxt =
    3.23        if ! verbose orelse mode = Forward then ProofContext.pretty_context context
    3.24 -      else if mode = Backward then ProofContext.pretty_asms context
    3.25 +      else if mode = Backward then ProofContext.pretty_ctxt context
    3.26        else [];
    3.27    in
    3.28      [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
    3.29 @@ -515,15 +515,15 @@
    3.30  
    3.31  local
    3.32  
    3.33 -fun gen_fix fix_ctxt args =
    3.34 +fun gen_fix add_fixes args =
    3.35    assert_forward
    3.36 -  #> map_context (fix_ctxt args)
    3.37 +  #> map_context (snd o add_fixes (map Syntax.no_syn args))
    3.38    #> put_facts NONE;
    3.39  
    3.40  in
    3.41  
    3.42 -val fix = gen_fix ProofContext.fix;
    3.43 -val fix_i = gen_fix ProofContext.fix_i;
    3.44 +val fix = gen_fix ProofContext.add_fixes;
    3.45 +val fix_i = gen_fix ProofContext.add_fixes_i;
    3.46  
    3.47  end;
    3.48  
    3.49 @@ -540,12 +540,12 @@
    3.50  
    3.51  in
    3.52  
    3.53 -val assm      = gen_assume ProofContext.assume Attrib.local_attribute;
    3.54 -val assm_i    = gen_assume ProofContext.assume_i (K I);
    3.55 -val assume    = assm ProofContext.export_assume;
    3.56 -val assume_i  = assm_i ProofContext.export_assume;
    3.57 -val presume   = assm ProofContext.export_presume;
    3.58 -val presume_i = assm_i ProofContext.export_presume;
    3.59 +val assm      = gen_assume ProofContext.add_assms Attrib.local_attribute;
    3.60 +val assm_i    = gen_assume ProofContext.add_assms_i (K I);
    3.61 +val assume    = assm ProofContext.assume_export;
    3.62 +val assume_i  = assm_i ProofContext.assume_export;
    3.63 +val presume   = assm ProofContext.presume_export;
    3.64 +val presume_i = assm_i ProofContext.presume_export;
    3.65  
    3.66  end;
    3.67  
    3.68 @@ -566,8 +566,8 @@
    3.69      val eqs = ProofContext.mk_def (context_of state') (xs ~~ rhss);
    3.70    in
    3.71      state'
    3.72 -    |> fix [(xs, NONE)]
    3.73 -    |> assm_i ProofContext.export_def ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
    3.74 +    |> fix (map (rpair NONE) xs)
    3.75 +    |> assm_i ProofContext.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
    3.76    end;
    3.77  
    3.78  in
    3.79 @@ -787,6 +787,7 @@
    3.80      goal_state
    3.81      |> tap (check_tvars props)
    3.82      |> tap (check_vars props)
    3.83 +    |> map_context (ProofContext.set_body true)
    3.84      |> put_goal (SOME (make_goal ((kind, propss), [], goal, before_qed, after_qed')))
    3.85      |> map_context (ProofContext.add_cases false (AutoBind.cases thy props))
    3.86      |> map_context (ProofContext.auto_bind_goal props)
    3.87 @@ -868,7 +869,7 @@
    3.88        #> after_qed results;
    3.89    in
    3.90      init ctxt
    3.91 -    |> generic_goal (prepp #> ProofContext.auto_fix) (kind ^ goal_names target name names)
    3.92 +    |> generic_goal (prepp #> ProofContext.auto_fixes) (kind ^ goal_names target name names)
    3.93        before_qed (K Seq.single, after_qed') propp
    3.94    end;
    3.95  
     4.1 --- a/src/Pure/Isar/specification.ML	Fri Jan 13 01:13:08 2006 +0100
     4.2 +++ b/src/Pure/Isar/specification.ML	Fri Jan 13 01:13:11 2006 +0100
     4.3 @@ -43,31 +43,27 @@
     4.4  
     4.5  (* prepare specification *)
     4.6  
     4.7 -fun prep_specification prep_typ prep_propp prep_att
     4.8 -    (raw_params, raw_specs) context =
     4.9 +fun prep_specification prep_vars prep_propp prep_att
    4.10 +    (raw_vars, raw_specs) ctxt =
    4.11    let
    4.12 -    fun prep_param (x, raw_T, mx) ctxt =
    4.13 -      let
    4.14 -        val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx;
    4.15 -        val T = Option.map (prep_typ ctxt) raw_T;
    4.16 -      in ((x', mx'), ProofContext.add_fixes [(x', T, SOME mx')] ctxt) end;
    4.17 +    val thy = ProofContext.theory_of ctxt;
    4.18  
    4.19 -    val ((xs, mxs), params_ctxt) =
    4.20 -      context |> fold_map prep_param raw_params |>> split_list;
    4.21 -    val ((specs, vars), specs_ctxt) =
    4.22 +    val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
    4.23 +    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    4.24 +    val ((specs, vs), specs_ctxt) =
    4.25        prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
    4.26        |> swap |>> map (map fst)
    4.27 -      ||>> fold_map ProofContext.declared_type xs;
    4.28 +      ||>> fold_map ProofContext.inferred_type xs;
    4.29  
    4.30 -    val params = map2 (fn (x, T) => fn mx => (x, T, mx)) vars mxs;
    4.31 +    val params = map2 (fn (x, T) => fn (_, _, mx) => (x, T, mx)) vs vars;
    4.32      val names = map (fst o fst) raw_specs;
    4.33 -    val atts = map (map (prep_att (ProofContext.theory_of context)) o snd o fst) raw_specs;
    4.34 +    val atts = map (map (prep_att thy) o snd o fst) raw_specs;
    4.35    in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
    4.36  
    4.37  fun read_specification x =
    4.38 -  prep_specification ProofContext.read_typ ProofContext.read_propp Attrib.generic_attribute x;
    4.39 +  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.generic_attribute x;
    4.40  fun cert_specification x =
    4.41 -  prep_specification ProofContext.cert_typ ProofContext.cert_propp (K I) x;
    4.42 +  prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
    4.43  
    4.44  
    4.45  (* axiomatize *)
     5.1 --- a/src/Pure/Tools/class_package.ML	Fri Jan 13 01:13:08 2006 +0100
     5.2 +++ b/src/Pure/Tools/class_package.ML	Fri Jan 13 01:13:11 2006 +0100
     5.3 @@ -173,7 +173,7 @@
     5.4               | _ => NONE)
     5.5        |> Library.flat
     5.6        |> map (fn (c, ty, syn) =>
     5.7 -           ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c o the) syn))
     5.8 +           ((c, the ty), (Syntax.unlocalize_mixfix o Syntax.fix_mixfix c) syn))
     5.9        |> `(fn consts => extract_tyvar_name thy (map (snd o fst) consts))
    5.10        |-> (fn v => map ((apfst o apsnd) (subst_clsvar v (TFree (v, []))))
    5.11           #> pair v);