more examples;
authorwenzelm
Sat Jun 13 13:18:37 2015 +0200 (2015-06-13)
changeset 60450b54b913dfa6a
parent 60449 229bad93377e
child 60451 1f2b29f78439
more examples;
src/HOL/Isar_Examples/Structured_Statements.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Sat Jun 13 13:18:37 2015 +0200
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  Title:      HOL/Isar_Examples/Structured_Statements.thy
     1.5 +    Author:     Makarius
     1.6 +*)
     1.7 +
     1.8 +section \<open>Structured statements within Isar proofs\<close>
     1.9 +
    1.10 +theory Structured_Statements
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +notepad
    1.15 +begin
    1.16 +
    1.17 +  fix A B :: bool
    1.18 +
    1.19 +  have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
    1.20 +  proof
    1.21 +    show "B \<and> A" if "A \<and> B"
    1.22 +    proof
    1.23 +      show B using that ..
    1.24 +      show A using that ..
    1.25 +    qed
    1.26 +    show "A \<and> B" if "B \<and> A"
    1.27 +    proof
    1.28 +      show A using that ..
    1.29 +      show B using that ..
    1.30 +    qed
    1.31 +  qed
    1.32 +
    1.33 +  text \<open>Alternative proof, avoiding redundant copy of symmetric argument.\<close>
    1.34 +  have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
    1.35 +  proof
    1.36 +    show "B \<and> A" if "A \<and> B" for A B
    1.37 +    proof
    1.38 +      show B using that ..
    1.39 +      show A using that ..
    1.40 +    qed
    1.41 +    then show "A \<and> B" if "B \<and> A"
    1.42 +      by this (rule that)
    1.43 +  qed
    1.44 +
    1.45 +end
    1.46 +
    1.47 +end
    1.48 \ No newline at end of file
     2.1 --- a/src/HOL/ROOT	Sat Jun 13 13:09:05 2015 +0200
     2.2 +++ b/src/HOL/ROOT	Sat Jun 13 13:18:37 2015 +0200
     2.3 @@ -623,6 +623,7 @@
     2.4      Peirce
     2.5      Puzzle
     2.6      Summation
     2.7 +    Structured_Statements
     2.8    document_files
     2.9      "root.bib"
    2.10      "root.tex"