isabelle: src/HOL/Induct/Com.thy@c3658c18b7bc

     1 (*  Title:      HOL/Induct/Com.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1997  University of Cambridge

     5 Example of Mutual Induction via Iteratived Inductive Definitions: Commands

     6 *)

     8 section\<open>Mutual Induction via Iteratived Inductive Definitions\<close>

    10 theory Com imports Main begin

    12 typedecl loc

    13 type_synonym state = "loc => nat"

    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)

    28 subsection \<open>Commands\<close>

    30 text\<open>Execution of commands\<close>

    32 abbreviation (input)

    33   generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)  where

    34   "esig -|[eval]-> ns == (esig,ns) \<in> eval"

    36 text\<open>Command execution.  Natural numbers represent Booleans: 0=True, 1=False\<close>

    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"

    46   | Skip:    "(SKIP,s) -[eval]-> s"

    48   | Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"

    50   | Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]

    51              ==> (c0 ;; c1, s) -[eval]-> s1"

    53   | IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]

    54              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"

    56   | IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]

    57               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"

    59   | WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)

    60                  ==> (WHILE e DO c, s) -[eval]-> s1"

    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"

    66 declare exec.intros [intro]

    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"

    77 text\<open>Justifies using "exec" in the inductive definition of "eval"\<close>

    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

    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)

    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)

    95 text\<open>Command execution is functional (deterministic) provided evaluation is\<close>

    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

   105 subsection \<open>Expressions\<close>

   107 text\<open>Evaluation of arithmetic expressions\<close>

   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"

   115   | N [intro!]: "(N(n),s) -|-> (n,s)"

   117   | X [intro!]: "(X(x),s) -|-> (s(x),s)"

   119   | Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]

   120                  ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"

   122   | valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]

   123                     ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"

   125   monos exec_mono

   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)"

   135 lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"

   136   by (rule fun_upd_same [THEN subst]) fast

   139 text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new

   140     version look worse than it is...\<close>

   142 lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (case_prod (%v. case_prod (case_prod P v)))"

   143   by auto

   145 text\<open>New induction rule.  Note the form of the VALOF induction hypothesis\<close>

   146 lemma eval_induct

   147   [case_names N X Op valOf, consumes 1, induct set: eval]:

   148   "[| (e,s) -|-> (n,s');

   149       !!n s. P (N n) s n s;

   150       !!s x. P (X x) s (s x) s;

   151       !!e0 e1 f n0 n1 s s0 s1.

   152          [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;

   153             (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1

   154          |] ==> P (Op f e0 e1) s (f n0 n1) s1;

   155       !!c e n s s0 s1.

   156          [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;

   157             (c,s) -[eval]-> s0;

   158             (e,s0) -|-> (n,s1); P e s0 n s1 |]

   159          ==> P (VALOF c RESULTIS e) s n s1

   160    |] ==> P e s n s'"

   161 apply (induct set: eval)

   162 apply blast

   163 apply blast

   164 apply blast

   165 apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])

   166 apply (auto simp add: split_lemma)

   167 done

   170 text\<open>Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}

   171   using eval restricted to its functional part.  Note that the execution

   172   @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}!  The reason is that

   173   the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is

   174   functional on the argument @{text "(c,s)"}.

   175 \<close>

   176 lemma com_Unique:

   177  "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1

   178   ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"

   179 apply (induct set: exec)

   180       apply simp_all

   181       apply blast

   182      apply force

   183     apply blast

   184    apply blast

   185   apply blast

   186  apply (blast elim: exec_WHILE_case)

   187 apply (erule_tac V = "(c,s2) -[ev]-> s3" for c ev in thin_rl)

   188 apply clarify

   189 apply (erule exec_WHILE_case, blast+)

   190 done

   193 text\<open>Expression evaluation is functional, or deterministic\<close>

   194 theorem single_valued_eval: "single_valued eval"

   195 apply (unfold single_valued_def)

   196 apply (intro allI, rule impI)

   197 apply (simp (no_asm_simp) only: split_tupled_all)

   198 apply (erule eval_induct)

   199 apply (drule_tac [4] com_Unique)

   200 apply (simp_all (no_asm_use))

   201 apply blast+

   202 done

   204 lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"

   205   by (induct e == "N n" s v s' set: eval) simp_all

   207 text\<open>This theorem says that "WHILE TRUE DO c" cannot terminate\<close>

   208 lemma while_true_E:

   209     "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"

   210   by (induct set: exec) auto

   213 subsection\<open>Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and

   214        WHILE e DO c\<close>

   216 lemma while_if1:

   217      "(c',s) -[eval]-> t

   218       ==> c' = WHILE e DO c ==>

   219           (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"

   220   by (induct set: exec) auto

   222 lemma while_if2:

   223      "(c',s) -[eval]-> t

   224       ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==>

   225           (WHILE e DO c, s) -[eval]-> t"

   226   by (induct set: exec) auto

   229 theorem while_if:

   230      "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =

   231       ((WHILE e DO c, s) -[eval]-> t)"

   232 by (blast intro: while_if1 while_if2)

   236 subsection\<open>Equivalence of  (IF e THEN c1 ELSE c2);;c

   237                          and  IF e THEN (c1;;c) ELSE (c2;;c)\<close>

   239 lemma if_semi1:

   240      "(c',s) -[eval]-> t

   241       ==> c' = (IF e THEN c1 ELSE c2);;c ==>

   242           (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"

   243   by (induct set: exec) auto

   245 lemma if_semi2:

   246      "(c',s) -[eval]-> t

   247       ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==>

   248           ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"

   249   by (induct set: exec) auto

   251 theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =

   252                   ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"

   253   by (blast intro: if_semi1 if_semi2)

   257 subsection\<open>Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)

   258                   and  VALOF c1;;c2 RESULTIS e

   259 \<close>

   261 lemma valof_valof1:

   262      "(e',s) -|-> (v,s')

   263       ==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==>

   264           (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"

   265   by (induct set: eval) auto

   267 lemma valof_valof2:

   268      "(e',s) -|-> (v,s')

   269       ==> e' = VALOF c1;;c2 RESULTIS e ==>

   270           (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"

   271   by (induct set: eval) auto

   273 theorem valof_valof:

   274      "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =

   275       ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"

   276   by (blast intro: valof_valof1 valof_valof2)

   279 subsection\<open>Equivalence of  VALOF SKIP RESULTIS e  and  e\<close>

   281 lemma valof_skip1:

   282      "(e',s) -|-> (v,s')

   283       ==> e' = VALOF SKIP RESULTIS e ==>

   284           (e, s) -|-> (v,s')"

   285   by (induct set: eval) auto

   287 lemma valof_skip2:

   288     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"

   289   by blast

   291 theorem valof_skip:

   292     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"

   293   by (blast intro: valof_skip1 valof_skip2)

   296 subsection\<open>Equivalence of  VALOF x:=e RESULTIS x  and  e\<close>

   298 lemma valof_assign1:

   299      "(e',s) -|-> (v,s'')

   300       ==> e' = VALOF x:=e RESULTIS X x ==>

   301           (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"

   302   by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto)

   304 lemma valof_assign2:

   305     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"

   306   by blast

   308 end

author	haftmann
	Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424	c3658c18b7bc
parent 60530	44f9873d6f6f
child 63167	0909deb8059b
permissions	-rw-r--r--