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