doc-src/TutorialI/Overview/FP1.thy
 author nipkow Fri, 30 Mar 2001 18:18:22 +0200 changeset 11237 0ef5ecc1fd4d parent 11236 17403c5a9eb1 child 11292 d838df879585 permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 11235 860c65c7388a *** empty log message *** nipkow parents: diff changeset  1 theory FP1 = Main:  860c65c7388a *** empty log message *** nipkow parents: diff changeset  2 860c65c7388a *** empty log message *** nipkow parents: diff changeset  3 subsection{*More Constructs*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  4 860c65c7388a *** empty log message *** nipkow parents: diff changeset  5 lemma "if xs = ys  860c65c7388a *** empty log message *** nipkow parents: diff changeset  6  then rev xs = rev ys  860c65c7388a *** empty log message *** nipkow parents: diff changeset  7  else rev xs \ rev ys"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  8 by auto  860c65c7388a *** empty log message *** nipkow parents: diff changeset  9 860c65c7388a *** empty log message *** nipkow parents: diff changeset  10 lemma "case xs of  860c65c7388a *** empty log message *** nipkow parents: diff changeset  11  [] \ tl xs = xs  860c65c7388a *** empty log message *** nipkow parents: diff changeset  12  | y#ys \ tl xs \ xs"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  13 apply(case_tac xs)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  14 by auto  860c65c7388a *** empty log message *** nipkow parents: diff changeset  15 860c65c7388a *** empty log message *** nipkow parents: diff changeset  16 860c65c7388a *** empty log message *** nipkow parents: diff changeset  17 subsection{*More Types*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  18 860c65c7388a *** empty log message *** nipkow parents: diff changeset  19 860c65c7388a *** empty log message *** nipkow parents: diff changeset  20 subsubsection{*Natural Numbers*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  21 860c65c7388a *** empty log message *** nipkow parents: diff changeset  22 consts sum :: "nat \ nat"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  23 primrec "sum 0 = 0"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  24  "sum (Suc n) = Suc n + sum n"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  25 860c65c7388a *** empty log message *** nipkow parents: diff changeset  26 lemma "sum n + sum n = n*(Suc n)";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  27 apply(induct_tac n);  860c65c7388a *** empty log message *** nipkow parents: diff changeset  28 apply(auto);  860c65c7388a *** empty log message *** nipkow parents: diff changeset  29 done  860c65c7388a *** empty log message *** nipkow parents: diff changeset  30 860c65c7388a *** empty log message *** nipkow parents: diff changeset  31 lemma "\ \ m < n; m < n+1 \ \ m = n"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  32 by(auto)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  33 860c65c7388a *** empty log message *** nipkow parents: diff changeset  34 lemma "min i (max j k) = max (min k i) (min i (j::nat))";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  35 by(arith)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  36 860c65c7388a *** empty log message *** nipkow parents: diff changeset  37 lemma "n*n = n \ n=0 \ n=1"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  38 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  39 860c65c7388a *** empty log message *** nipkow parents: diff changeset  40 860c65c7388a *** empty log message *** nipkow parents: diff changeset  41 subsubsection{*Pairs*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  42 860c65c7388a *** empty log message *** nipkow parents: diff changeset  43 lemma "fst(x,y) = snd(z,x)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  44 by auto  860c65c7388a *** empty log message *** nipkow parents: diff changeset  45 860c65c7388a *** empty log message *** nipkow parents: diff changeset  46 860c65c7388a *** empty log message *** nipkow parents: diff changeset  47 860c65c7388a *** empty log message *** nipkow parents: diff changeset  48 subsection{*Definitions*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  49 860c65c7388a *** empty log message *** nipkow parents: diff changeset  50 consts xor :: "bool \ bool \ bool"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  51 defs xor_def: "xor x y \ x \ \y \ \x \ y"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  52 860c65c7388a *** empty log message *** nipkow parents: diff changeset  53 constdefs nand :: "bool \ bool \ bool"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  54  "nand x y \ \(x \ y)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  55 860c65c7388a *** empty log message *** nipkow parents: diff changeset  56 lemma "\ xor x x"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  57 apply(unfold xor_def)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  58 by auto  860c65c7388a *** empty log message *** nipkow parents: diff changeset  59 860c65c7388a *** empty log message *** nipkow parents: diff changeset  60 860c65c7388a *** empty log message *** nipkow parents: diff changeset  61 860c65c7388a *** empty log message *** nipkow parents: diff changeset  62 subsection{*Simplification*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  63 860c65c7388a *** empty log message *** nipkow parents: diff changeset  64 860c65c7388a *** empty log message *** nipkow parents: diff changeset  65 subsubsection{*Simplification Rules*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  66 860c65c7388a *** empty log message *** nipkow parents: diff changeset  67 lemma fst_conv[simp]: "fst(x,y) = x"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  68 by auto  860c65c7388a *** empty log message *** nipkow parents: diff changeset  69 860c65c7388a *** empty log message *** nipkow parents: diff changeset  70 declare fst_conv[simp]  860c65c7388a *** empty log message *** nipkow parents: diff changeset  71 declare fst_conv[simp del]  860c65c7388a *** empty log message *** nipkow parents: diff changeset  72 860c65c7388a *** empty log message *** nipkow parents: diff changeset  73 860c65c7388a *** empty log message *** nipkow parents: diff changeset  74 subsubsection{*The Simplification Method*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  75 860c65c7388a *** empty log message *** nipkow parents: diff changeset  76 lemma "x*(y+1) = y*(x+1)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  77 apply simp  860c65c7388a *** empty log message *** nipkow parents: diff changeset  78 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  79 860c65c7388a *** empty log message *** nipkow parents: diff changeset  80 860c65c7388a *** empty log message *** nipkow parents: diff changeset  81 subsubsection{*Adding and Deleting Simplification Rules*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  82 860c65c7388a *** empty log message *** nipkow parents: diff changeset  83 lemma "\x::nat. x*(y+z) = r"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  84 apply (simp add: add_mult_distrib2)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  85 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  86 860c65c7388a *** empty log message *** nipkow parents: diff changeset  87 lemma "rev(rev(xs @ [])) = xs"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  88 apply (simp del: rev_rev_ident)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  89 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  90 860c65c7388a *** empty log message *** nipkow parents: diff changeset  91 860c65c7388a *** empty log message *** nipkow parents: diff changeset  92 subsubsection{*Assumptions*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  93 860c65c7388a *** empty log message *** nipkow parents: diff changeset  94 lemma "\ xs @ zs = ys @ xs; [] @ xs = [] @ [] \ \ ys = zs";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  95 apply simp;  860c65c7388a *** empty log message *** nipkow parents: diff changeset  96 done  860c65c7388a *** empty log message *** nipkow parents: diff changeset  97 860c65c7388a *** empty log message *** nipkow parents: diff changeset  98 lemma "\x. f x = g (f (g x)) \ f [] = f [] @ []";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  99 apply(simp (no_asm));  860c65c7388a *** empty log message *** nipkow parents: diff changeset  100 done  860c65c7388a *** empty log message *** nipkow parents: diff changeset  101 860c65c7388a *** empty log message *** nipkow parents: diff changeset  102 860c65c7388a *** empty log message *** nipkow parents: diff changeset  103 subsubsection{*Rewriting with Definitions*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  104 860c65c7388a *** empty log message *** nipkow parents: diff changeset  105 lemma "xor A (\A)";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  106 apply(simp only:xor_def);  860c65c7388a *** empty log message *** nipkow parents: diff changeset  107 by simp  860c65c7388a *** empty log message *** nipkow parents: diff changeset  108 860c65c7388a *** empty log message *** nipkow parents: diff changeset  109 860c65c7388a *** empty log message *** nipkow parents: diff changeset  110 subsubsection{*Conditional Equations*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  111 860c65c7388a *** empty log message *** nipkow parents: diff changeset  112 lemma hd_Cons_tl[simp]: "xs \ [] \ hd xs # tl xs = xs"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  113 apply(case_tac xs, simp, simp)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  114 done  860c65c7388a *** empty log message *** nipkow parents: diff changeset  115 860c65c7388a *** empty log message *** nipkow parents: diff changeset  116 lemma "xs \ [] \ hd(rev xs) # tl(rev xs) = rev xs"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  117 by(simp)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  118 860c65c7388a *** empty log message *** nipkow parents: diff changeset  119 860c65c7388a *** empty log message *** nipkow parents: diff changeset  120 subsubsection{*Automatic Case Splits*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  121 860c65c7388a *** empty log message *** nipkow parents: diff changeset  122 lemma "\xs. if xs = [] then A else B";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  123 apply simp  860c65c7388a *** empty log message *** nipkow parents: diff changeset  124 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  125 860c65c7388a *** empty log message *** nipkow parents: diff changeset  126 lemma "case xs @ [] of [] \ A | y#ys \ B";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  127 apply simp  860c65c7388a *** empty log message *** nipkow parents: diff changeset  128 apply(simp split: list.split)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  129 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  130 860c65c7388a *** empty log message *** nipkow parents: diff changeset  131 860c65c7388a *** empty log message *** nipkow parents: diff changeset  132 subsubsection{*Arithmetic*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  133 860c65c7388a *** empty log message *** nipkow parents: diff changeset  134 lemma "\ \ m < n; m < n+1 \ \ m = n"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  135 by simp  860c65c7388a *** empty log message *** nipkow parents: diff changeset  136 860c65c7388a *** empty log message *** nipkow parents: diff changeset  137 lemma "\ m < n \ m < n+1 \ m = n";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  138 apply simp  860c65c7388a *** empty log message *** nipkow parents: diff changeset  139 by(arith)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  140 860c65c7388a *** empty log message *** nipkow parents: diff changeset  141 860c65c7388a *** empty log message *** nipkow parents: diff changeset  142 subsubsection{*Tracing*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  143 860c65c7388a *** empty log message *** nipkow parents: diff changeset  144 lemma "rev [a] = []"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  145 apply(simp)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  146 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  147 860c65c7388a *** empty log message *** nipkow parents: diff changeset  148 860c65c7388a *** empty log message *** nipkow parents: diff changeset  149 860c65c7388a *** empty log message *** nipkow parents: diff changeset  150 subsection{*Case Study: Compiling Expressions*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  151 860c65c7388a *** empty log message *** nipkow parents: diff changeset  152 860c65c7388a *** empty log message *** nipkow parents: diff changeset  153 subsubsection{*Expressions*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  154 860c65c7388a *** empty log message *** nipkow parents: diff changeset  155 types 'v binop = "'v \ 'v \ 'v";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  156 860c65c7388a *** empty log message *** nipkow parents: diff changeset  157 datatype ('a,'v)expr = Cex 'v  860c65c7388a *** empty log message *** nipkow parents: diff changeset  158  | Vex 'a  860c65c7388a *** empty log message *** nipkow parents: diff changeset  159  | Bex "'v binop" "('a,'v)expr" "('a,'v)expr";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  160 860c65c7388a *** empty log message *** nipkow parents: diff changeset  161 consts value :: "('a,'v)expr \ ('a \ 'v) \ 'v";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  162 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  163 "value (Cex v) env = v"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  164 "value (Vex a) env = env a"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  165 "value (Bex f e1 e2) env = f (value e1 env) (value e2 env)";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  166 860c65c7388a *** empty log message *** nipkow parents: diff changeset  167 860c65c7388a *** empty log message *** nipkow parents: diff changeset  168 subsubsection{*The Stack Machine*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  169 860c65c7388a *** empty log message *** nipkow parents: diff changeset  170 datatype ('a,'v) instr = Const 'v  860c65c7388a *** empty log message *** nipkow parents: diff changeset  171  | Load 'a  860c65c7388a *** empty log message *** nipkow parents: diff changeset  172  | Apply "'v binop";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  173 860c65c7388a *** empty log message *** nipkow parents: diff changeset  174 consts exec :: "('a,'v)instr list \ ('a\'v) \ 'v list \ 'v list";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  175 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  176 "exec [] s vs = vs"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  177 "exec (i#is) s vs = (case i of  860c65c7388a *** empty log message *** nipkow parents: diff changeset  178  Const v \ exec is s (v#vs)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  179  | Load a \ exec is s ((s a)#vs)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  180  | Apply f \ exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  181 860c65c7388a *** empty log message *** nipkow parents: diff changeset  182 860c65c7388a *** empty log message *** nipkow parents: diff changeset  183 subsubsection{*The Compiler*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  184 860c65c7388a *** empty log message *** nipkow parents: diff changeset  185 consts comp :: "('a,'v)expr \ ('a,'v)instr list";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  186 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  187 "comp (Cex v) = [Const v]"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  188 "comp (Vex a) = [Load a]"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  189 "comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  190 860c65c7388a *** empty log message *** nipkow parents: diff changeset  191 theorem "exec (comp e) s [] = [value e s]";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  192 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  193 860c65c7388a *** empty log message *** nipkow parents: diff changeset  194 860c65c7388a *** empty log message *** nipkow parents: diff changeset  195 11236 17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  196 subsection{*Advanced Datatypes*}  11235 860c65c7388a *** empty log message *** nipkow parents: diff changeset  197 860c65c7388a *** empty log message *** nipkow parents: diff changeset  198 860c65c7388a *** empty log message *** nipkow parents: diff changeset  199 subsubsection{*Mutual Recursion*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  200 860c65c7388a *** empty log message *** nipkow parents: diff changeset  201 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  202  | Sum "'a aexp" "'a aexp"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  203  | Var 'a  860c65c7388a *** empty log message *** nipkow parents: diff changeset  204  | Num nat  860c65c7388a *** empty log message *** nipkow parents: diff changeset  205 and 'a bexp = Less "'a aexp" "'a aexp"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  206  | And "'a bexp" "'a bexp"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  207  | Neg "'a bexp";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  208 860c65c7388a *** empty log message *** nipkow parents: diff changeset  209 860c65c7388a *** empty log message *** nipkow parents: diff changeset  210 consts evala :: "'a aexp \ ('a \ nat) \ nat"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  211  evalb :: "'a bexp \ ('a \ nat) \ bool";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  212 860c65c7388a *** empty log message *** nipkow parents: diff changeset  213 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  214  "evala (IF b a1 a2) env =  860c65c7388a *** empty log message *** nipkow parents: diff changeset  215  (if evalb b env then evala a1 env else evala a2 env)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  216  "evala (Sum a1 a2) env = evala a1 env + evala a2 env"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  217  "evala (Var v) env = env v"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  218  "evala (Num n) env = n"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  219 860c65c7388a *** empty log message *** nipkow parents: diff changeset  220  "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  221  "evalb (And b1 b2) env = (evalb b1 env \ evalb b2 env)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  222  "evalb (Neg b) env = (\ evalb b env)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  223 860c65c7388a *** empty log message *** nipkow parents: diff changeset  224 consts substa :: "('a \ 'b aexp) \ 'a aexp \ 'b aexp"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  225  substb :: "('a \ 'b aexp) \ 'a bexp \ 'b bexp"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  226 860c65c7388a *** empty log message *** nipkow parents: diff changeset  227 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  228  "substa s (IF b a1 a2) =  860c65c7388a *** empty log message *** nipkow parents: diff changeset  229  IF (substb s b) (substa s a1) (substa s a2)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  230  "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  231  "substa s (Var v) = s v"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  232  "substa s (Num n) = Num n"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  233 860c65c7388a *** empty log message *** nipkow parents: diff changeset  234  "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  235  "substb s (And b1 b2) = And (substb s b1) (substb s b2)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  236  "substb s (Neg b) = Neg (substb s b)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  237 860c65c7388a *** empty log message *** nipkow parents: diff changeset  238 lemma substitution_lemma:  860c65c7388a *** empty log message *** nipkow parents: diff changeset  239  "evala (substa s a) env = evala a (\x. evala (s x) env) \  860c65c7388a *** empty log message *** nipkow parents: diff changeset  240  evalb (substb s b) env = evalb b (\x. evala (s x) env)";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  241 apply(induct_tac a and b);  860c65c7388a *** empty log message *** nipkow parents: diff changeset  242 by simp_all  860c65c7388a *** empty log message *** nipkow parents: diff changeset  243 860c65c7388a *** empty log message *** nipkow parents: diff changeset  244 860c65c7388a *** empty log message *** nipkow parents: diff changeset  245 subsubsection{*Nested Recursion*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  246 860c65c7388a *** empty log message *** nipkow parents: diff changeset  247 datatype tree = C "tree list"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  248 860c65c7388a *** empty log message *** nipkow parents: diff changeset  249 term "C[]"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  250 term "C[C[C[]],C[]]"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  251 860c65c7388a *** empty log message *** nipkow parents: diff changeset  252 consts  860c65c7388a *** empty log message *** nipkow parents: diff changeset  253 mirror :: "tree \ tree"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  254 mirrors:: "tree list \ tree list";  860c65c7388a *** empty log message *** nipkow parents: diff changeset  255 860c65c7388a *** empty log message *** nipkow parents: diff changeset  256 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  257  "mirror(C ts) = C(mirrors ts)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  258 860c65c7388a *** empty log message *** nipkow parents: diff changeset  259  "mirrors [] = []"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  260  "mirrors (t # ts) = mirrors ts @ [mirror t]"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  261 860c65c7388a *** empty log message *** nipkow parents: diff changeset  262 lemma "mirror(mirror t) = t \ mirrors(mirrors ts) = ts"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  263 apply(induct_tac t and ts)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  264 apply simp_all  860c65c7388a *** empty log message *** nipkow parents: diff changeset  265 oops  860c65c7388a *** empty log message *** nipkow parents: diff changeset  266 11236 17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  267 text{*  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  268 \begin{exercise}  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  269 Complete the above proof.  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  270 \end{exercise}  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  271 *}  11235 860c65c7388a *** empty log message *** nipkow parents: diff changeset  272 860c65c7388a *** empty log message *** nipkow parents: diff changeset  273 860c65c7388a *** empty log message *** nipkow parents: diff changeset  274 subsubsection{*Datatypes Involving Functions*}  860c65c7388a *** empty log message *** nipkow parents: diff changeset  275 860c65c7388a *** empty log message *** nipkow parents: diff changeset  276 datatype ('a,'i)bigtree = Tip | Br 'a "'i \ ('a,'i)bigtree"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  277 860c65c7388a *** empty log message *** nipkow parents: diff changeset  278 term "Br 0 (\i. Br i (\n. Tip))"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  279 860c65c7388a *** empty log message *** nipkow parents: diff changeset  280 consts map_bt :: "('a \ 'b) \ ('a,'i)bigtree \ ('b,'i)bigtree"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  281 primrec  860c65c7388a *** empty log message *** nipkow parents: diff changeset  282 "map_bt f Tip = Tip"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  283 "map_bt f (Br a F) = Br (f a) (\i. map_bt f (F i))"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  284 860c65c7388a *** empty log message *** nipkow parents: diff changeset  285 lemma "map_bt (g o f) T = map_bt g (map_bt f T)"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  286 apply(induct_tac T, rename_tac[2] F)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  287 apply simp_all  860c65c7388a *** empty log message *** nipkow parents: diff changeset  288 done  860c65c7388a *** empty log message *** nipkow parents: diff changeset  289 860c65c7388a *** empty log message *** nipkow parents: diff changeset  290 (* This is NOT allowed:  860c65c7388a *** empty log message *** nipkow parents: diff changeset  291 datatype lambda = C "lambda \ lambda"  860c65c7388a *** empty log message *** nipkow parents: diff changeset  292 *)  860c65c7388a *** empty log message *** nipkow parents: diff changeset  293 11236 17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  294 text{*  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  295 \begin{exercise}  11237 0ef5ecc1fd4d *** empty log message *** nipkow parents: 11236 diff changeset  296 Define a datatype of ordinals and the ordinal $\Gamma_0$.  11236 17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  297 \end{exercise}  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  298 *}  17403c5a9eb1 *** empty log message *** nipkow parents: 11235 diff changeset  299 11235 860c65c7388a *** empty log message *** nipkow parents: diff changeset  300 end