doc-src/TutorialI/Inductive/AB.thy
author nipkow
Mon Oct 16 13:21:01 2000 +0200 (2000-10-16)
changeset 10225 b9fd52525b69
parent 10217 e61e7e1eacaf
child 10236 7626cb4e1407
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)theory AB = Main:(*>*)
     2 
     3 section{*A context free grammar*}
     4 
     5 datatype alfa = a | b;
     6 
     7 lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)";
     8 apply(case_tac x);
     9 by(auto);
    10 
    11 consts S :: "alfa list set"
    12        A :: "alfa list set"
    13        B :: "alfa list set";
    14 
    15 inductive S A B
    16 intros
    17 "[] : S"
    18 "w : A ==> b#w : S"
    19 "w : B ==> a#w : S"
    20 
    21 "w : S ==> a#w : A"
    22 "[| v:A; w:A |] ==> b#v@w : A"
    23 
    24 "w : S ==> b#w : B"
    25 "[| v:B; w:B |] ==> a#v@w : B";
    26 
    27 thm S_A_B.induct[no_vars];
    28 
    29 lemma "(w : S --> size[x:w. x=a] = size[x:w. x=b]) &
    30        (w : A --> size[x:w. x=a] = size[x:w. x=b] + 1) &
    31        (w : B --> size[x:w. x=b] = size[x:w. x=a] + 1)";
    32 apply(rule S_A_B.induct);
    33 by(auto);
    34 
    35 lemma intermed_val[rule_format(no_asm)]:
    36  "(!i<n. abs(f(i+1) - f i) <= #1) --> 
    37   f 0 <= k & k <= f n --> (? i <= n. f i = (k::int))";
    38 apply(induct n);
    39  apply(simp);
    40  apply(arith);
    41 apply(rule);
    42 apply(erule impE);
    43  apply(simp);
    44 apply(rule);
    45 apply(erule_tac x = n in allE);
    46 apply(simp);
    47 apply(case_tac "k = f(n+1)");
    48  apply(force);
    49 apply(erule impE);
    50  apply(simp add:zabs_def split:split_if_asm);
    51  apply(arith);
    52 by(blast intro:le_SucI);
    53 
    54 lemma step1: "ALL i < size w.
    55   abs((int(size[x:take (i+1) w . P x]) - int(size[x:take (i+1) w . ~P x])) -
    56       (int(size[x:take i w . P x]) - int(size[x:take i w . ~P x]))) <= #1";
    57 apply(induct w);
    58  apply(simp);
    59 apply(simp add:take_Cons split:nat.split);
    60 apply(clarsimp);
    61 apply(rule conjI);
    62  apply(clarify);
    63  apply(erule allE);
    64  apply(erule impE);
    65   apply(assumption);
    66  apply(arith);
    67 apply(clarify);
    68 apply(erule allE);
    69 apply(erule impE);
    70  apply(assumption);
    71 by(arith);
    72 
    73 
    74 lemma part1:
    75  "size[x:w. P x] = Suc(Suc(size[x:w. ~P x])) ==>
    76   EX i<=size w. size[x:take i w. P x] = size[x:take i w. ~P x]+1";
    77 apply(insert intermed_val[OF step1, of "P" "w" "#1"]);
    78 apply(simp);
    79 apply(erule exE);
    80 apply(rule_tac x=i in exI);
    81 apply(simp);
    82 apply(rule int_int_eq[THEN iffD1]);
    83 apply(simp);
    84 by(arith);
    85 
    86 lemma part2:
    87 "[| size[x:take i xs @ drop i xs. P x] = size[x:take i xs @ drop i xs. ~P x]+2;
    88     size[x:take i xs. P x] = size[x:take i xs. ~P x]+1 |]
    89  ==> size[x:drop i xs. P x] = size[x:drop i xs. ~P x]+1";
    90 by(simp del:append_take_drop_id);
    91 
    92 lemmas [simp] = S_A_B.intros;
    93 
    94 lemma "(size[x:w. x=a] = size[x:w. x=b] --> w : S) &
    95        (size[x:w. x=a] = size[x:w. x=b] + 1 --> w : A) &
    96        (size[x:w. x=b] = size[x:w. x=a] + 1 --> w : B)";
    97 apply(induct_tac w rule: length_induct);
    98 apply(case_tac "xs");
    99  apply(simp);
   100 apply(simp);
   101 apply(rule conjI);
   102  apply(clarify);
   103  apply(frule part1[of "%x. x=a", simplified]);
   104  apply(erule exE);
   105  apply(erule conjE);
   106  apply(drule part2[of "%x. x=a", simplified]);
   107   apply(assumption);
   108  apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
   109  apply(rule S_A_B.intros);
   110   apply(force simp add:min_less_iff_disj);
   111  apply(force split add: nat_diff_split);
   112 apply(clarify);
   113 apply(frule part1[of "%x. x=b", simplified]);
   114 apply(erule exE);
   115 apply(erule conjE);
   116 apply(drule part2[of "%x. x=b", simplified]);
   117  apply(assumption);
   118 apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]);
   119 apply(rule S_A_B.intros);
   120  apply(force simp add:min_less_iff_disj);
   121 by(force simp add:min_less_iff_disj split add: nat_diff_split);
   122 
   123 (*<*)end(*>*)