isabelle: src/HOL/Library/While_Combinator.thy@337c00fd385b

     1 (*  Title:      HOL/Library/While.thy

     2     ID:         $Id$

     3     Author:     Tobias Nipkow

     4     Copyright   2000 TU Muenchen

     5 *)

     7 header {*

     8  \title{A general ``while'' combinator}

     9  \author{Tobias Nipkow}

    10 *}

    12 theory While_Combinator = Main:

    14 text {*

    15  We define a while-combinator @{term while} and prove: (a) an

    16  unrestricted unfolding law (even if while diverges!)  (I got this

    17  idea from Wolfgang Goerigk), and (b) the invariant rule for reasoning

    18  about @{term while}.

    19 *}

    21 consts while_aux :: "('a => bool) \<times> ('a => 'a) \<times> 'a => 'a"

    22 recdef while_aux

    23   "same_fst (\<lambda>b. True) (\<lambda>b. same_fst (\<lambda>c. True) (\<lambda>c.

    24       {(t, s).  b s \<and> c s = t \<and>

    25         \<not> (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))}))"

    26   "while_aux (b, c, s) =

    27     (if (\<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1)))

    28       then arbitrary

    29       else if b s then while_aux (b, c, c s)

    30       else s)"

    32 constdefs

    33   while :: "('a => bool) => ('a => 'a) => 'a => 'a"

    34   "while b c s == while_aux (b, c, s)"

    36 ML_setup {*

    37   goalw_cterm [] (cterm_of (sign_of (the_context ()))

    38     (HOLogic.mk_Trueprop (hd (RecdefPackage.tcs_of (the_context ()) "while_aux"))));

    39   br wf_same_fst 1;

    40   br wf_same_fst 1;

    41   by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain]) 1);

    42   by (Blast_tac 1);

    43   qed "while_aux_tc";

    44 *} (* FIXME cannot access recdef tcs in Isar yet! *)

    46 lemma while_aux_unfold:

    47   "while_aux (b, c, s) =

    48     (if \<exists>f. f 0 = s \<and> (\<forall>i. b (f i) \<and> c (f i) = f (i + 1))

    49       then arbitrary

    50       else if b s then while_aux (b, c, c s)

    51       else s)"

    52   apply (rule while_aux_tc [THEN while_aux.simps [THEN trans]])

    53    apply (simp add: same_fst_def)

    54   apply (rule refl)

    55   done

    57 text {*

    58  The recursion equation for @{term while}: directly executable!

    59 *}

    61 theorem while_unfold:

    62     "while b c s = (if b s then while b c (c s) else s)"

    63   apply (unfold while_def)

    64   apply (rule while_aux_unfold [THEN trans])

    65   apply auto

    66   apply (subst while_aux_unfold)

    67   apply simp

    68   apply clarify

    69   apply (erule_tac x = "\<lambda>i. f (Suc i)" in allE)

    70   apply blast

    71   done

    73 text {*

    74  The proof rule for @{term while}, where @{term P} is the invariant.

    75 *}

    77 theorem while_rule_lemma[rule_format]:

    78   "(!!s. P s ==> b s ==> P (c s)) ==>

    79     (!!s. P s ==> \<not> b s ==> Q s) ==>

    80     wf {(t, s). P s \<and> b s \<and> t = c s} ==>

    81     P s --> Q (while b c s)"

    82 proof -

    83   case antecedent

    84   assume wf: "wf {(t, s). P s \<and> b s \<and> t = c s}"

    85   show ?thesis

    86     apply (induct s rule: wf [THEN wf_induct])

    87     apply simp

    88     apply clarify

    89     apply (subst while_unfold)

    90     apply (simp add: antecedent)

    91     done

    92 qed

    94 theorem while_rule:

    95   "[| P s; !!s. [| P s; b s  |] ==> P (c s);

    96     !!s. [| P s; \<not> b s  |] ==> Q s;

    97     wf r;  !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>

    98     Q (while b c s)"

    99 apply (rule while_rule_lemma)

   100 prefer 4 apply assumption

   101 apply blast

   102 apply blast

   103 apply(erule wf_subset)

   104 apply blast

   105 done

   107 hide const while_aux

   109 end

author	wenzelm
	Thu Dec 14 19:37:27 2000 +0100 (2000-12-14)
changeset 10673	337c00fd385b
parent 10653	55f33da63366
child 10774	4de3a0d3ae28
permissions	-rw-r--r--