src/Pure/goal.ML
 author wenzelm Thu Dec 22 00:29:18 2005 +0100 (2005-12-22) changeset 18484 5dd6f2f5704f parent 18252 9e2c15ae0e86 child 18497 7569674d7bb1 permissions -rw-r--r--
conclude/SELECT: Thm.bicompose_no_flatten avoids unsolicited modification of result;
```     1 (*  Title:      Pure/goal.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Makarius and Lawrence C Paulson
```
```     4
```
```     5 Goals in tactical theorem proving.
```
```     6 *)
```
```     7
```
```     8 signature BASIC_GOAL =
```
```     9 sig
```
```    10   val SELECT_GOAL: tactic -> int -> tactic
```
```    11 end;
```
```    12
```
```    13 signature GOAL =
```
```    14 sig
```
```    15   include BASIC_GOAL
```
```    16   val init: cterm -> thm
```
```    17   val protect: thm -> thm
```
```    18   val conclude: thm -> thm
```
```    19   val finish: thm -> thm
```
```    20   val norm_hhf: thm -> thm
```
```    21   val norm_hhf_protect: thm -> thm
```
```    22   val compose_hhf: thm -> int -> thm -> thm Seq.seq
```
```    23   val compose_hhf_tac: thm -> int -> tactic
```
```    24   val comp_hhf: thm -> thm -> thm
```
```    25   val prove_multi: theory -> string list -> term list -> term list ->
```
```    26     (thm list -> tactic) -> thm list
```
```    27   val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
```
```    28   val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
```
```    29 end;
```
```    30
```
```    31 structure Goal: GOAL =
```
```    32 struct
```
```    33
```
```    34 (** goals **)
```
```    35
```
```    36 (*
```
```    37   -------- (init)
```
```    38   C ==> #C
```
```    39 *)
```
```    40 fun init ct = Drule.instantiate' [] [SOME ct] Drule.protectI;
```
```    41
```
```    42 (*
```
```    43    C
```
```    44   --- (protect)
```
```    45   #C
```
```    46 *)
```
```    47 fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
```
```    48
```
```    49 (*
```
```    50   A ==> ... ==> #C
```
```    51   ---------------- (conclude)
```
```    52   A ==> ... ==> C
```
```    53 *)
```
```    54 fun conclude th =
```
```    55   (case SINGLE (Thm.bicompose_no_flatten false (false, th, Thm.nprems_of th) 1)
```
```    56       (Drule.incr_indexes th Drule.protectD) of
```
```    57     SOME th' => th'
```
```    58   | NONE => raise THM ("Failed to conclude goal", 0, [th]));
```
```    59
```
```    60 (*
```
```    61   #C
```
```    62   --- (finish)
```
```    63    C
```
```    64 *)
```
```    65 fun finish th =
```
```    66   (case Thm.nprems_of th of
```
```    67     0 => conclude th
```
```    68   | n => raise THM ("Proof failed.\n" ^
```
```    69       Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
```
```    70       ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
```
```    71
```
```    72
```
```    73
```
```    74 (** results **)
```
```    75
```
```    76 (* HHF normal form: !! before ==>, outermost !! generalized *)
```
```    77
```
```    78 local
```
```    79
```
```    80 fun gen_norm_hhf ss =
```
```    81   (not o Drule.is_norm_hhf o Thm.prop_of) ?
```
```    82     Drule.fconv_rule (MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) ss)
```
```    83   #> Thm.adjust_maxidx_thm
```
```    84   #> Drule.gen_all;
```
```    85
```
```    86 val ss =
```
```    87   MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
```
```    88     addsimps [Drule.norm_hhf_eq];
```
```    89
```
```    90 in
```
```    91
```
```    92 val norm_hhf = gen_norm_hhf ss;
```
```    93 val norm_hhf_protect = gen_norm_hhf (ss addeqcongs [Drule.protect_cong]);
```
```    94
```
```    95 end;
```
```    96
```
```    97
```
```    98 (* composition of normal results *)
```
```    99
```
```   100 fun compose_hhf tha i thb =
```
```   101   Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
```
```   102
```
```   103 fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
```
```   104
```
```   105 fun comp_hhf tha thb =
```
```   106   (case Seq.chop (2, compose_hhf tha 1 thb) of
```
```   107     ([th], _) => th
```
```   108   | ([], _) => raise THM ("comp_hhf: no unifiers", 1, [tha, thb])
```
```   109   | _  => raise THM ("comp_hhf: multiple unifiers", 1, [tha, thb]));
```
```   110
```
```   111
```
```   112
```
```   113 (** tactical theorem proving **)
```
```   114
```
```   115 (* prove_multi *)
```
```   116
```
```   117 fun prove_multi thy xs asms props tac =
```
```   118   let
```
```   119     val prop = Logic.mk_conjunction_list props;
```
```   120     val statement = Logic.list_implies (asms, prop);
```
```   121     val frees = Term.add_frees statement [];
```
```   122     val fixed_frees = filter_out (member (op =) xs o #1) frees;
```
```   123     val fixed_tfrees = fold (Term.add_tfreesT o #2) fixed_frees [];
```
```   124     val params = List.mapPartial (fn x => Option.map (pair x) (AList.lookup (op =) frees x)) xs;
```
```   125
```
```   126     fun err msg = raise ERROR_MESSAGE
```
```   127       (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
```
```   128         Sign.string_of_term thy (Term.list_all_free (params, statement)));
```
```   129
```
```   130     fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
```
```   131       handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
```
```   132
```
```   133     val _ = cert_safe statement;
```
```   134     val _ = Term.no_dummy_patterns statement handle TERM (msg, _) => err msg;
```
```   135
```
```   136     val cparams = map (cert_safe o Free) params;
```
```   137     val casms = map cert_safe asms;
```
```   138     val prems = map (norm_hhf o Thm.assume) casms;
```
```   139
```
```   140     val goal = init (cert_safe prop);
```
```   141     val goal' = case SINGLE (tac prems) goal of SOME goal' => goal' | _ => err "Tactic failed.";
```
```   142     val raw_result = finish goal' handle THM (msg, _, _) => err msg;
```
```   143
```
```   144     val prop' = Thm.prop_of raw_result;
```
```   145     val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
```
```   146       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
```
```   147   in
```
```   148     Drule.conj_elim_precise (length props) raw_result
```
```   149     |> map
```
```   150       (Drule.implies_intr_list casms
```
```   151         #> Drule.forall_intr_list cparams
```
```   152         #> norm_hhf
```
```   153         #> Thm.varifyT' fixed_tfrees
```
```   154         #-> K Drule.zero_var_indexes)
```
```   155   end;
```
```   156
```
```   157
```
```   158 (* prove *)
```
```   159
```
```   160 fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
```
```   161
```
```   162
```
```   163 (* prove_raw -- no checks, no normalization of result! *)
```
```   164
```
```   165 fun prove_raw casms cprop tac =
```
```   166   (case SINGLE (tac (map (norm_hhf o Thm.assume) casms)) (init cprop) of
```
```   167     SOME th => Drule.implies_intr_list casms (finish th)
```
```   168   | NONE => raise ERROR_MESSAGE "Tactic failed.");
```
```   169
```
```   170
```
```   171 (* SELECT_GOAL *)
```
```   172
```
```   173 (*Tactical for restricting the effect of a tactic to subgoal i.  Works
```
```   174   by making a new state from subgoal i, applying tac to it, and
```
```   175   composing the resulting thm with the original state.*)
```
```   176
```
```   177 local
```
```   178
```
```   179 fun SELECT tac i st =
```
```   180   init (Thm.adjust_maxidx (Thm.cprem_of st i))
```
```   181   |> tac
```
```   182   |> Seq.maps (fn st' =>
```
```   183     Thm.bicompose_no_flatten false (false, conclude st', Thm.nprems_of st') i st);
```
```   184
```
```   185 in
```
```   186
```
```   187 fun SELECT_GOAL tac i st =
```
```   188   let val n = Thm.nprems_of st in
```
```   189     if 1 <= i andalso i <= n then
```
```   190       if n = 1 then tac st else SELECT tac i st
```
```   191     else Seq.empty
```
```   192   end;
```
```   193
```
```   194 end;
```
```   195
```
```   196 end;
```
```   197
```
```   198 structure BasicGoal: BASIC_GOAL = Goal;
```
```   199 open BasicGoal;
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.55620915,"math_prob":0.9819391,"size":4770,"snap":"2019-43-2019-47","text_gpt3_token_len":1449,"char_repetition_ratio":0.12001678,"word_repetition_ratio":0.03422053,"special_character_ratio":0.3595388,"punctuation_ratio":0.17845118,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.98438805,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-11-12T06:23:53Z\",\"WARC-Record-ID\":\"<urn:uuid:c02d7315-232b-4e1f-9c7a-c2553739ef4a>\",\"Content-Length\":\"33024\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:92609f06-b7e2-4c61-b551-7cd056c94aaa>\",\"WARC-Concurrent-To\":\"<urn:uuid:3dd18206-415b-4da4-bf35-fa06948ae4a2>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"http://isabelle.in.tum.de/repos/isabelle/file/5dd6f2f5704f/src/Pure/goal.ML\",\"WARC-Payload-Digest\":\"sha1:GSRZDL2OJOU6XO6XTQK5A2MKKH6TAT4C\",\"WARC-Block-Digest\":\"sha1:LO7B7M5B5OV2YD72R47QDMUZQDOBQSR7\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-47/CC-MAIN-2019-47_segments_1573496664752.70_warc_CC-MAIN-20191112051214-20191112075214-00436.warc.gz\"}"}