src/HOL/Isar_examples/MultisetOrder.thy
changeset 10256 320a4084dfac
parent 10255 bb66874b4750
child 10257 21055ac27708
     1.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Wed Oct 18 23:33:04 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,148 +0,0 @@
     1.4 -(*  Title:      HOL/Isar_examples/MultisetOrder.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Markus Wenzel
     1.7 -
     1.8 -Wellfoundedness proof for the multiset order.
     1.9 -*)
    1.10 -
    1.11 -header {* Wellfoundedness of multiset ordering *}
    1.12 -
    1.13 -theory MultisetOrder = Multiset:
    1.14 -
    1.15 -text_raw {*
    1.16 - \footnote{Original tactic script by Tobias Nipkow (see
    1.17 - \url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
    1.18 - based on a pen-and-paper proof due to Wilfried Buchholz.}\isanewline
    1.19 -*}
    1.20 -(*<*)(* FIXME move? *)
    1.21 -declare multiset_induct [induct type: multiset]
    1.22 -declare wf_induct [induct set: wf]
    1.23 -declare acc_induct [induct set: acc](*>*)
    1.24 -
    1.25 -subsection {* A technical lemma *}
    1.26 -
    1.27 -lemma less_add: "(N, M0 + {#a#}) : mult1 r ==>
    1.28 -    (EX M. (M, M0) : mult1 r & N = M + {#a#}) |
    1.29 -    (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K)"
    1.30 -  (concl is "?case1 (mult1 r) | ?case2")
    1.31 -proof (unfold mult1_def)
    1.32 -  let ?r = "\<lambda>K a. ALL b. b :# K --> (b, a) : r"
    1.33 -  let ?R = "\<lambda>N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a"
    1.34 -  let ?case1 = "?case1 {(N, M). ?R N M}"
    1.35 -
    1.36 -  assume "(N, M0 + {#a#}) : {(N, M). ?R N M}"
    1.37 -  hence "EX a' M0' K.
    1.38 -      M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'" by simp
    1.39 -  thus "?case1 | ?case2"
    1.40 -  proof (elim exE conjE)
    1.41 -    fix a' M0' K
    1.42 -    assume N: "N = M0' + K" and r: "?r K a'"
    1.43 -    assume "M0 + {#a#} = M0' + {#a'#}"
    1.44 -    hence "M0 = M0' & a = a' |
    1.45 -        (EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})"
    1.46 -      by (simp only: add_eq_conv_ex)
    1.47 -    thus ?thesis
    1.48 -    proof (elim disjE conjE exE)
    1.49 -      assume "M0 = M0'" "a = a'"
    1.50 -      with N r have "?r K a & N = M0 + K" by simp
    1.51 -      hence ?case2 .. thus ?thesis ..
    1.52 -    next
    1.53 -      fix K'
    1.54 -      assume "M0' = K' + {#a#}"
    1.55 -      with N have n: "N = K' + K + {#a#}" by (simp add: union_ac)
    1.56 -
    1.57 -      assume "M0 = K' + {#a'#}"
    1.58 -      with r have "?R (K' + K) M0" by blast
    1.59 -      with n have ?case1 by simp thus ?thesis ..
    1.60 -    qed
    1.61 -  qed
    1.62 -qed
    1.63 -
    1.64 -
    1.65 -subsection {* The key property *}
    1.66 -
    1.67 -lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"
    1.68 -proof
    1.69 -  let ?R = "mult1 r"
    1.70 -  let ?W = "acc ?R"
    1.71 -  {
    1.72 -    fix M M0 a
    1.73 -    assume M0: "M0 : ?W"
    1.74 -      and wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
    1.75 -      and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W"
    1.76 -    have "M0 + {#a#} : ?W"
    1.77 -    proof (rule accI [of "M0 + {#a#}"])
    1.78 -      fix N
    1.79 -      assume "(N, M0 + {#a#}) : ?R"
    1.80 -      hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
    1.81 -          (EX K. (ALL b. b :# K --> (b, a) : r) & N = M0 + K))"
    1.82 -	by (rule less_add)
    1.83 -      thus "N : ?W"
    1.84 -      proof (elim exE disjE conjE)
    1.85 -	fix M assume "(M, M0) : ?R" and N: "N = M + {#a#}"
    1.86 -	from acc_hyp have "(M, M0) : ?R --> M + {#a#} : ?W" ..
    1.87 -	hence "M + {#a#} : ?W" ..
    1.88 -	thus "N : ?W" by (simp only: N)
    1.89 -      next
    1.90 -	fix K
    1.91 -	assume N: "N = M0 + K"
    1.92 -	assume "ALL b. b :# K --> (b, a) : r"
    1.93 -	have "?this --> M0 + K : ?W" (is "?P K")
    1.94 -	proof (induct K)
    1.95 -	  from M0 have "M0 + {#} : ?W" by simp
    1.96 -	  thus "?P {#}" ..
    1.97 -
    1.98 -	  fix K x assume hyp: "?P K"
    1.99 -	  show "?P (K + {#x#})"
   1.100 -	  proof
   1.101 -	    assume a: "ALL b. b :# (K + {#x#}) --> (b, a) : r"
   1.102 -	    hence "(x, a) : r" by simp
   1.103 -	    with wf_hyp have b: "ALL M:?W. M + {#x#} : ?W" by blast
   1.104 -
   1.105 -	    from a hyp have "M0 + K : ?W" by simp
   1.106 -	    with b have "(M0 + K) + {#x#} : ?W" ..
   1.107 -	    thus "M0 + (K + {#x#}) : ?W" by (simp only: union_assoc)
   1.108 -	  qed
   1.109 -	qed
   1.110 -	hence "M0 + K : ?W" ..
   1.111 -	thus "N : ?W" by (simp only: N)
   1.112 -      qed
   1.113 -    qed
   1.114 -  } note tedious_reasoning = this
   1.115 -
   1.116 -  assume wf: "wf r"
   1.117 -  fix M
   1.118 -  show "M : ?W"
   1.119 -  proof (induct M)
   1.120 -    show "{#} : ?W"
   1.121 -    proof (rule accI)
   1.122 -      fix b assume "(b, {#}) : ?R"
   1.123 -      with not_less_empty show "b : ?W" by contradiction
   1.124 -    qed
   1.125 -
   1.126 -    fix M a assume "M : ?W"
   1.127 -    from wf have "ALL M:?W. M + {#a#} : ?W"
   1.128 -    proof induct
   1.129 -      fix a
   1.130 -      assume "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)"
   1.131 -      show "ALL M:?W. M + {#a#} : ?W"
   1.132 -      proof
   1.133 -	fix M assume "M : ?W"
   1.134 -	thus "M + {#a#} : ?W"
   1.135 -          by (rule acc_induct) (rule tedious_reasoning)
   1.136 -      qed
   1.137 -    qed
   1.138 -    thus "M + {#a#} : ?W" ..
   1.139 -  qed
   1.140 -qed
   1.141 -
   1.142 -
   1.143 -subsection {* Main result *}
   1.144 -
   1.145 -theorem wf_mult1: "wf r ==> wf (mult1 r)"
   1.146 -  by (rule acc_wfI, rule all_accessible)
   1.147 -
   1.148 -theorem wf_mult: "wf r ==> wf (mult r)"
   1.149 -  by (unfold mult_def, rule wf_trancl, rule wf_mult1)
   1.150 -
   1.151 -end