src/HOL/Library/While_Combinator_Example.thy
author wenzelm
Fri, 03 Nov 2000 21:35:59 +0100
changeset 10390 1d54567bed24
parent 10251 5cc44cae9590
child 10392 f27afee8475d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10251
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     1
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     2
header {* \title{} *}
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     3
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     4
theory While_Combinator_Example = While_Combinator:
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     5
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     6
text {*
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     7
 An example of using the @{term while} combinator.
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     8
*}
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
     9
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    10
lemma aux: "{f n| n. A n \<or> B n} = {f n| n. A n} \<union> {f n| n. B n}"
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    11
  apply blast
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    12
  done
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    13
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    14
theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6| n. n \<in> N})) =
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    15
    P {#0, #4, #2}"
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    16
  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    17
     apply (rule monoI)
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    18
    apply blast
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    19
   apply simp
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    20
  apply (simp add: aux set_eq_subset)
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    21
  txt {* The fixpoint computation is performed purely by rewriting: *}
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    22
  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    23
  done
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    24
5cc44cae9590 A general ``while'' combinator (from main HOL);
wenzelm
parents:
diff changeset
    25
end