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