'same' method, 'immediate' proof;
authorwenzelm
Tue Jan 12 17:19:53 1999 +0100 (1999-01-12)
changeset 61082c9ed58c30ba
parent 6107 1418bc571f23
child 6109 82b50115564c
'same' method, 'immediate' proof;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jan 12 17:19:13 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jan 12 17:19:53 1999 +0100
     1.3 @@ -353,9 +353,9 @@
     1.4  val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;
     1.5  val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
     1.6  
     1.7 -val trivial_proofP =
     1.8 -  OuterSyntax.parser false "." "trivial proof"
     1.9 -    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.trivial_proof));
    1.10 +val immediate_proofP =
    1.11 +  OuterSyntax.parser false "." "immediate proof"
    1.12 +    (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
    1.13  
    1.14  val default_proofP =
    1.15    OuterSyntax.parser false ".." "default proof"
    1.16 @@ -524,7 +524,7 @@
    1.17    (*proof commands*)
    1.18    theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
    1.19    factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,
    1.20 -  then_refineP, proofP, terminal_proofP, trivial_proofP,
    1.21 +  then_refineP, proofP, terminal_proofP, immediate_proofP,
    1.22    default_proofP, clear_undoP, undoP, redoP, undosP, redosP, backP,
    1.23    prevP, upP, topP,
    1.24    (*diagnostic commands*)
     2.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Jan 12 17:19:13 1999 +0100
     2.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Jan 12 17:19:53 1999 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4    val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
     2.5    val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
     2.6    val terminal_proof: Method.text -> ProofHistory.T -> ProofHistory.T
     2.7 -  val trivial_proof: ProofHistory.T -> ProofHistory.T
     2.8 +  val immediate_proof: ProofHistory.T -> ProofHistory.T
     2.9    val default_proof: ProofHistory.T -> ProofHistory.T
    2.10    val use_mltext: string -> theory option -> theory option
    2.11    val use_mltext_theory: string -> theory -> theory
    2.12 @@ -167,7 +167,7 @@
    2.13  val proof = ProofHistory.applys o Method.proof;
    2.14  val end_block = ProofHistory.applys_close Method.end_block;
    2.15  val terminal_proof = ProofHistory.applys_close o Method.terminal_proof;
    2.16 -val trivial_proof = ProofHistory.applys_close Method.trivial_proof;
    2.17 +val immediate_proof = ProofHistory.applys_close Method.immediate_proof;
    2.18  val default_proof = ProofHistory.applys_close Method.default_proof;
    2.19  
    2.20  
     3.1 --- a/src/Pure/Isar/method.ML	Tue Jan 12 17:19:13 1999 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Tue Jan 12 17:19:53 1999 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4    val METHOD0: tactic -> Proof.method
     3.5    val fail: Proof.method
     3.6    val succeed: Proof.method
     3.7 -  val trivial: Proof.method
     3.8 +  val same: Proof.method
     3.9    val assumption: Proof.method
    3.10    val forward_chain: thm list -> thm list -> thm Seq.seq
    3.11    val rule_tac: thm list -> thm list -> int -> tactic
    3.12 @@ -56,7 +56,7 @@
    3.13    val proof: text option -> Proof.state -> Proof.state Seq.seq
    3.14    val end_block: Proof.state -> Proof.state Seq.seq
    3.15    val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    3.16 -  val trivial_proof: Proof.state -> Proof.state Seq.seq
    3.17 +  val immediate_proof: Proof.state -> Proof.state Seq.seq
    3.18    val default_proof: Proof.state -> Proof.state Seq.seq
    3.19    val qed: bstring option -> theory attribute list option -> Proof.state
    3.20      -> theory * (string * string * thm)
    3.21 @@ -82,15 +82,15 @@
    3.22  val succeed = METHOD (K all_tac);
    3.23  
    3.24  
    3.25 -(* trivial, assumption *)
    3.26 +(* same, assumption *)
    3.27  
    3.28 -fun trivial_tac [] = K all_tac
    3.29 -  | trivial_tac facts =
    3.30 +fun same_tac [] = K all_tac
    3.31 +  | same_tac facts =
    3.32        let val r = ~ (length facts);
    3.33        in metacuts_tac facts THEN' rotate_tac r end;
    3.34  
    3.35 -val trivial = METHOD (ALLGOALS o trivial_tac);
    3.36 -val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
    3.37 +val same = METHOD (ALLGOALS o same_tac);
    3.38 +val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac));
    3.39  
    3.40  val asm_finish = METHOD (K (FILTER (equal 0 o Thm.nprems_of) (ALLGOALS assume_tac)));
    3.41  
    3.42 @@ -293,7 +293,7 @@
    3.43  val end_block = Proof.end_block (dynamic_method finishN);
    3.44  
    3.45  fun terminal_proof text = Seq.THEN (proof (Some text), end_block);
    3.46 -val trivial_proof = terminal_proof (Basic (K trivial));
    3.47 +val immediate_proof = terminal_proof (Basic (K same));
    3.48  val default_proof = terminal_proof default_txt;
    3.49  
    3.50  val qed = Proof.qed (dynamic_method finishN);
    3.51 @@ -307,7 +307,7 @@
    3.52  val pure_methods =
    3.53   [("fail", no_args fail, "force failure"),
    3.54    ("succeed", no_args succeed, "succeed"),
    3.55 -  ("trivial", no_args trivial, "proof all goals trivially"),
    3.56 +  ("same", no_args same, "insert facts, nothing else"),
    3.57    ("assumption", no_args assumption, "proof by assumption"),
    3.58    ("finish", no_args asm_finish, "finish proof by assumption"),
    3.59    ("rule", thms_args rule, "apply primitive rule")];