src/HOL/Induct/Com.thy
author berghofe
Wed Jul 11 11:14:51 2007 +0200 (2007-07-11)
changeset 23746 a455e69c31cc
parent 19736 d8d0f8f51d69
child 24178 4ff1dc2aa18d
permissions -rw-r--r--
Adapted to new inductive definition package.
     1 (*  Title:      HOL/Induct/Com
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     7 *)
     8 
     9 header{*Mutual Induction via Iteratived Inductive Definitions*}
    10 
    11 theory Com imports Main begin
    12 
    13 typedecl loc
    14 
    15 types  state = "loc => nat"
    16        n2n2n = "nat => nat => nat"
    17 
    18 datatype
    19   exp = N nat
    20       | X loc
    21       | Op n2n2n exp exp
    22       | valOf com exp          ("VALOF _ RESULTIS _"  60)
    23 and
    24   com = SKIP
    25       | ":="  loc exp          (infixl  60)
    26       | Semi  com com          ("_;;_"  [60, 60] 60)
    27       | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    28       | While exp com          ("WHILE _ DO _"  60)
    29 
    30 
    31 subsection {* Commands *}
    32 
    33 text{* Execution of commands *}
    34 
    35 abbreviation (input)
    36   generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)  where
    37   "esig -|[eval]-> ns == (esig,ns) \<in> eval"
    38 
    39 text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
    40 
    41 inductive_set
    42   exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    43   and exec_rel :: "com * state => ((exp*state) * (nat*state)) set => state => bool"
    44     ("_/ -[_]-> _" [50,0,50] 50)
    45   for eval :: "((exp*state) * (nat*state)) set"
    46   where
    47     "csig -[eval]-> s == (csig,s) \<in> exec eval"
    48 
    49   | Skip:    "(SKIP,s) -[eval]-> s"
    50 
    51   | Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    52 
    53   | Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
    54              ==> (c0 ;; c1, s) -[eval]-> s1"
    55 
    56   | IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
    57              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    58 
    59   | IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
    60               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    61 
    62   | WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
    63                  ==> (WHILE e DO c, s) -[eval]-> s1"
    64 
    65   | WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
    66                     (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
    67                  ==> (WHILE e DO c, s) -[eval]-> s3"
    68 
    69 declare exec.intros [intro]
    70 
    71 
    72 inductive_cases
    73         [elim!]: "(SKIP,s) -[eval]-> t"
    74     and [elim!]: "(x:=a,s) -[eval]-> t"
    75     and [elim!]: "(c1;;c2, s) -[eval]-> t"
    76     and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
    77     and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
    78 
    79 
    80 text{*Justifies using "exec" in the inductive definition of "eval"*}
    81 lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
    82 apply (rule subsetI)
    83 apply (simp add: split_paired_all)
    84 apply (erule exec.induct)
    85 apply blast+
    86 done
    87 
    88 lemma [pred_set_conv]:
    89   "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
    90   by (auto simp add: le_fun_def le_bool_def)
    91 
    92 lemma [pred_set_conv]:
    93   "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
    94   by (auto simp add: le_fun_def le_bool_def)
    95 
    96 ML {*
    97 Unify.trace_bound := 30;
    98 Unify.search_bound := 60;
    99 *}
   100 
   101 text{*Command execution is functional (deterministic) provided evaluation is*}
   102 theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
   103 apply (simp add: single_valued_def)
   104 apply (intro allI)
   105 apply (rule impI)
   106 apply (erule exec.induct)
   107 apply (blast elim: exec_WHILE_case)+
   108 done
   109 
   110 
   111 subsection {* Expressions *}
   112 
   113 text{* Evaluation of arithmetic expressions *}
   114 
   115 inductive_set
   116   eval    :: "((exp*state) * (nat*state)) set"
   117   and eval_rel :: "[exp*state,nat*state] => bool"  (infixl "-|->" 50)
   118   where
   119     "esig -|-> ns == (esig, ns) \<in> eval"
   120 
   121   | N [intro!]: "(N(n),s) -|-> (n,s)"
   122 
   123   | X [intro!]: "(X(x),s) -|-> (s(x),s)"
   124 
   125   | Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
   126                  ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
   127 
   128   | valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
   129                     ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
   130 
   131   monos exec_mono
   132 
   133 
   134 inductive_cases
   135         [elim!]: "(N(n),sigma) -|-> (n',s')"
   136     and [elim!]: "(X(x),sigma) -|-> (n,s')"
   137     and [elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
   138     and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
   139 
   140 
   141 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
   142 by (rule fun_upd_same [THEN subst], fast)
   143 
   144 
   145 text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
   146     version look worse than it is...*}
   147 
   148 lemma split_lemma:
   149      "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
   150 by auto
   151 
   152 text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
   153 lemma eval_induct
   154   [case_names N X Op valOf, consumes 1, induct set: eval]:
   155   "[| (e,s) -|-> (n,s');
   156       !!n s. P (N n) s n s;
   157       !!s x. P (X x) s (s x) s;
   158       !!e0 e1 f n0 n1 s s0 s1.
   159          [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;
   160             (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1
   161          |] ==> P (Op f e0 e1) s (f n0 n1) s1;
   162       !!c e n s s0 s1.
   163          [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;
   164             (c,s) -[eval]-> s0;
   165             (e,s0) -|-> (n,s1); P e s0 n s1 |]
   166          ==> P (VALOF c RESULTIS e) s n s1
   167    |] ==> P e s n s'"
   168 apply (induct set: eval)
   169 apply blast
   170 apply blast
   171 apply blast
   172 apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
   173 apply (auto simp add: split_lemma)
   174 done
   175 
   176 
   177 text{*Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}
   178   using eval restricted to its functional part.  Note that the execution
   179   @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}!  The reason is that
   180   the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
   181   functional on the argument @{text "(c,s)"}.
   182 *}
   183 lemma com_Unique:
   184  "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
   185   ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
   186 apply (induct set: exec)
   187       apply simp_all
   188       apply blast
   189      apply force
   190     apply blast
   191    apply blast
   192   apply blast
   193  apply (blast elim: exec_WHILE_case)
   194 apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
   195 apply clarify
   196 apply (erule exec_WHILE_case, blast+)
   197 done
   198 
   199 
   200 text{*Expression evaluation is functional, or deterministic*}
   201 theorem single_valued_eval: "single_valued eval"
   202 apply (unfold single_valued_def)
   203 apply (intro allI, rule impI)
   204 apply (simp (no_asm_simp) only: split_tupled_all)
   205 apply (erule eval_induct)
   206 apply (drule_tac [4] com_Unique)
   207 apply (simp_all (no_asm_use))
   208 apply blast+
   209 done
   210 
   211 lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
   212   by (induct e == "N n" s v s' set: eval) simp_all
   213 
   214 text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
   215 lemma while_true_E:
   216     "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
   217   by (induct set: exec) auto
   218 
   219 
   220 subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
   221        WHILE e DO c *}
   222 
   223 lemma while_if1:
   224      "(c',s) -[eval]-> t
   225       ==> c' = WHILE e DO c ==>
   226           (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
   227   by (induct set: exec) auto
   228 
   229 lemma while_if2:
   230      "(c',s) -[eval]-> t
   231       ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==>
   232           (WHILE e DO c, s) -[eval]-> t"
   233   by (induct set: exec) auto
   234 
   235 
   236 theorem while_if:
   237      "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =
   238       ((WHILE e DO c, s) -[eval]-> t)"
   239 by (blast intro: while_if1 while_if2)
   240 
   241 
   242 
   243 subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
   244                          and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
   245 
   246 lemma if_semi1:
   247      "(c',s) -[eval]-> t
   248       ==> c' = (IF e THEN c1 ELSE c2);;c ==>
   249           (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
   250   by (induct set: exec) auto
   251 
   252 lemma if_semi2:
   253      "(c',s) -[eval]-> t
   254       ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==>
   255           ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
   256   by (induct set: exec) auto
   257 
   258 theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =
   259                   ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
   260   by (blast intro: if_semi1 if_semi2)
   261 
   262 
   263 
   264 subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
   265                   and  VALOF c1;;c2 RESULTIS e
   266  *}
   267 
   268 lemma valof_valof1:
   269      "(e',s) -|-> (v,s')
   270       ==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==>
   271           (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
   272   by (induct set: eval) auto
   273 
   274 lemma valof_valof2:
   275      "(e',s) -|-> (v,s')
   276       ==> e' = VALOF c1;;c2 RESULTIS e ==>
   277           (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
   278   by (induct set: eval) auto
   279 
   280 theorem valof_valof:
   281      "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =
   282       ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
   283   by (blast intro: valof_valof1 valof_valof2)
   284 
   285 
   286 subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
   287 
   288 lemma valof_skip1:
   289      "(e',s) -|-> (v,s')
   290       ==> e' = VALOF SKIP RESULTIS e ==>
   291           (e, s) -|-> (v,s')"
   292   by (induct set: eval) auto
   293 
   294 lemma valof_skip2:
   295     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
   296   by blast
   297 
   298 theorem valof_skip:
   299     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
   300   by (blast intro: valof_skip1 valof_skip2)
   301 
   302 
   303 subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
   304 
   305 lemma valof_assign1:
   306      "(e',s) -|-> (v,s'')
   307       ==> e' = VALOF x:=e RESULTIS X x ==>
   308           (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
   309   by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto)
   310 
   311 lemma valof_assign2:
   312     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
   313   by blast
   314 
   315 end