src/Pure/Isar/method.ML
changeset 6872 b250da153b1e
parent 6849 0b660860c0ad
child 6934 04d051190a5f
equal deleted inserted replaced
6871:01866edde713 6872:b250da153b1e
   296 (* structured proof steps *)
   296 (* structured proof steps *)
   297 
   297 
   298 val default_text = named_method "default";
   298 val default_text = named_method "default";
   299 val finish_text = named_method "finish";
   299 val finish_text = named_method "finish";
   300 
   300 
       
   301 
   301 fun proof opt_text state =
   302 fun proof opt_text state =
   302   state
   303   state
   303   |> Proof.assert_backward
   304   |> Proof.assert_backward
   304   |> refine (if_none opt_text default_text)
   305   |> refine (if_none opt_text default_text)
   305   |> Seq.map Proof.enter_forward;
   306   |> Seq.map Proof.enter_forward;
   307 fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
   308 fun local_qed opt_text = Proof.local_qed (refine (if_none opt_text finish_text));
   308 fun local_terminal_proof text pr = Seq.THEN (proof (Some text), local_qed None pr);
   309 fun local_terminal_proof text pr = Seq.THEN (proof (Some text), local_qed None pr);
   309 val local_immediate_proof = local_terminal_proof (Basic (K same));
   310 val local_immediate_proof = local_terminal_proof (Basic (K same));
   310 val local_default_proof = local_terminal_proof default_text;
   311 val local_default_proof = local_terminal_proof default_text;
   311 
   312 
   312 fun global_qed alt_name alt_atts opt_text =
   313 
       
   314 fun global_qeds alt_name alt_atts opt_text =
   313   Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
   315   Proof.global_qed (refine (if_none opt_text finish_text)) alt_name alt_atts;
   314 
   316 
   315 fun global_terminal_proof text = Seq.hd o Seq.map (global_qed None None None) o proof (Some text);
   317 fun global_qed alt_name alt_atts opt_text state =
       
   318   state
       
   319   |> global_qeds alt_name alt_atts opt_text
       
   320   |> Proof.check_result "Failed to finish proof" state
       
   321   |> Seq.hd;
       
   322 
       
   323 fun global_terminal_proof text state =
       
   324   state
       
   325   |> proof (Some text)
       
   326   |> Proof.check_result "Terminal proof method failed" state
       
   327   |> (Seq.flat o Seq.map (global_qeds None None None))
       
   328   |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
       
   329   |> Seq.hd;
       
   330 
   316 val global_immediate_proof = global_terminal_proof (Basic (K same));
   331 val global_immediate_proof = global_terminal_proof (Basic (K same));
   317 val global_default_proof = global_terminal_proof default_text;
   332 val global_default_proof = global_terminal_proof default_text;
   318 
   333 
   319 
   334 
   320 
   335