wenzelm@36862: (*  Title:      HOL/Induct/Com.thy
paulson@3120:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120:     Copyright   1997  University of Cambridge
paulson@3120: 
paulson@3120: Example of Mutual Induction via Iteratived Inductive Definitions: Commands
paulson@3120: *)
paulson@3120: 
paulson@14527: header{*Mutual Induction via Iteratived Inductive Definitions*}
paulson@14527: 
haftmann@16417: theory Com imports Main begin
paulson@3120: 
paulson@13075: typedecl loc
wenzelm@41818: type_synonym state = "loc => nat"
paulson@3120: 
blanchet@58305: datatype_new
paulson@3120:   exp = N nat
paulson@3120:       | X loc
wenzelm@24824:       | Op "nat => nat => nat" exp exp
nipkow@10759:       | valOf com exp          ("VALOF _ RESULTIS _"  60)
nipkow@10759: and
nipkow@10759:   com = SKIP
wenzelm@24824:       | Assign loc exp         (infixl ":=" 60)
wenzelm@24824:       | Semi com com           ("_;;_"  [60, 60] 60)
wenzelm@24824:       | Cond exp com com       ("IF _ THEN _ ELSE _"  60)
nipkow@10759:       | While exp com          ("WHILE _ DO _"  60)
paulson@3120: 
paulson@14527: 
paulson@14527: subsection {* Commands *}
paulson@14527: 
paulson@13075: text{* Execution of commands *}
oheimb@4264: 
wenzelm@19736: abbreviation (input)
berghofe@23746:   generic_rel  ("_/ -|[_]-> _" [50,0,50] 50)  where
wenzelm@19736:   "esig -|[eval]-> ns == (esig,ns) \<in> eval"
paulson@3120: 
paulson@13075: text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
paulson@3120: 
berghofe@23746: inductive_set
berghofe@23746:   exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
berghofe@23746:   and exec_rel :: "com * state => ((exp*state) * (nat*state)) set => state => bool"
berghofe@23746:     ("_/ -[_]-> _" [50,0,50] 50)
berghofe@23746:   for eval :: "((exp*state) * (nat*state)) set"
berghofe@23746:   where
berghofe@23746:     "csig -[eval]-> s == (csig,s) \<in> exec eval"
paulson@3120: 
berghofe@23746:   | Skip:    "(SKIP,s) -[eval]-> s"
berghofe@23746: 
berghofe@23746:   | Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
berghofe@23746: 
berghofe@23746:   | Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
paulson@13075:              ==> (c0 ;; c1, s) -[eval]-> s1"
paulson@13075: 
berghofe@23746:   | IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |]
paulson@3120:              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
paulson@3120: 
berghofe@23746:   | IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |]
paulson@13075:               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
paulson@13075: 
berghofe@23746:   | WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
paulson@13075:                  ==> (WHILE e DO c, s) -[eval]-> s1"
paulson@13075: 
berghofe@23746:   | WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
wenzelm@18260:                     (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |]
paulson@13075:                  ==> (WHILE e DO c, s) -[eval]-> s3"
paulson@13075: 
paulson@13075: declare exec.intros [intro]
paulson@13075: 
paulson@13075: 
paulson@13075: inductive_cases
wenzelm@18260:         [elim!]: "(SKIP,s) -[eval]-> t"
paulson@13075:     and [elim!]: "(x:=a,s) -[eval]-> t"
wenzelm@18260:     and [elim!]: "(c1;;c2, s) -[eval]-> t"
wenzelm@18260:     and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
wenzelm@18260:     and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
paulson@13075: 
paulson@13075: 
paulson@13075: text{*Justifies using "exec" in the inductive definition of "eval"*}
paulson@13075: lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
berghofe@23746: apply (rule subsetI)
berghofe@23746: apply (simp add: split_paired_all)
berghofe@23746: apply (erule exec.induct)
berghofe@23746: apply blast+
paulson@13075: done
paulson@13075: 
berghofe@23746: lemma [pred_set_conv]:
berghofe@23746:   "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
huffman@44174:   unfolding subset_eq
wenzelm@44965:   by (auto simp add: le_fun_def)
berghofe@23746: 
berghofe@23746: lemma [pred_set_conv]:
berghofe@23746:   "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
huffman@44174:   unfolding subset_eq
wenzelm@44965:   by (auto simp add: le_fun_def)
berghofe@23746: 
paulson@13075: text{*Command execution is functional (deterministic) provided evaluation is*}
paulson@13075: theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
paulson@13075: apply (simp add: single_valued_def)
wenzelm@18260: apply (intro allI)
paulson@13075: apply (rule impI)
paulson@13075: apply (erule exec.induct)
paulson@13075: apply (blast elim: exec_WHILE_case)+
paulson@13075: done
paulson@13075: 
paulson@13075: 
paulson@14527: subsection {* Expressions *}
paulson@13075: 
paulson@13075: text{* Evaluation of arithmetic expressions *}
wenzelm@18260: 
berghofe@23746: inductive_set
berghofe@23746:   eval    :: "((exp*state) * (nat*state)) set"
berghofe@23746:   and eval_rel :: "[exp*state,nat*state] => bool"  (infixl "-|->" 50)
berghofe@23746:   where
berghofe@23746:     "esig -|-> ns == (esig, ns) \<in> eval"
paulson@13075: 
berghofe@23746:   | N [intro!]: "(N(n),s) -|-> (n,s)"
paulson@13075: 
berghofe@23746:   | X [intro!]: "(X(x),s) -|-> (s(x),s)"
berghofe@23746: 
berghofe@23746:   | Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |]
paulson@13075:                  ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
paulson@13075: 
berghofe@23746:   | valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |]
paulson@13075:                     ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
paulson@13075: 
paulson@13075:   monos exec_mono
paulson@13075: 
paulson@13075: 
paulson@13075: inductive_cases
wenzelm@18260:         [elim!]: "(N(n),sigma) -|-> (n',s')"
paulson@13075:     and [elim!]: "(X(x),sigma) -|-> (n,s')"
wenzelm@18260:     and [elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
wenzelm@18260:     and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
paulson@13075: 
paulson@13075: 
paulson@13075: lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
wenzelm@44965:   by (rule fun_upd_same [THEN subst]) fast
paulson@13075: 
paulson@13075: 
berghofe@23746: text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
paulson@13075:     version look worse than it is...*}
paulson@13075: 
wenzelm@44965: lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
wenzelm@44965:   by auto
paulson@13075: 
paulson@13075: text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
wenzelm@18260: lemma eval_induct
wenzelm@18260:   [case_names N X Op valOf, consumes 1, induct set: eval]:
wenzelm@18260:   "[| (e,s) -|-> (n,s');
wenzelm@18260:       !!n s. P (N n) s n s;
wenzelm@18260:       !!s x. P (X x) s (s x) s;
wenzelm@18260:       !!e0 e1 f n0 n1 s s0 s1.
wenzelm@18260:          [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;
wenzelm@18260:             (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1
wenzelm@18260:          |] ==> P (Op f e0 e1) s (f n0 n1) s1;
wenzelm@18260:       !!c e n s s0 s1.
wenzelm@18260:          [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;
wenzelm@18260:             (c,s) -[eval]-> s0;
wenzelm@18260:             (e,s0) -|-> (n,s1); P e s0 n s1 |]
wenzelm@18260:          ==> P (VALOF c RESULTIS e) s n s1
paulson@13075:    |] ==> P e s n s'"
wenzelm@18260: apply (induct set: eval)
wenzelm@18260: apply blast
wenzelm@18260: apply blast
wenzelm@18260: apply blast
paulson@13075: apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
paulson@13075: apply (auto simp add: split_lemma)
paulson@13075: done
paulson@13075: 
paulson@3120: 
berghofe@23746: text{*Lemma for @{text Function_eval}.  The major premise is that @{text "(c,s)"} executes to @{text "s1"}
paulson@13075:   using eval restricted to its functional part.  Note that the execution
berghofe@23746:   @{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}!  The reason is that
berghofe@23746:   the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
berghofe@23746:   functional on the argument @{text "(c,s)"}.
paulson@13075: *}
paulson@13075: lemma com_Unique:
wenzelm@18260:  "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
paulson@13075:   ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
wenzelm@18260: apply (induct set: exec)
wenzelm@18260:       apply simp_all
paulson@13075:       apply blast
paulson@13075:      apply force
paulson@13075:     apply blast
paulson@13075:    apply blast
paulson@13075:   apply blast
paulson@13075:  apply (blast elim: exec_WHILE_case)
paulson@13075: apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
paulson@13075: apply clarify
wenzelm@18260: apply (erule exec_WHILE_case, blast+)
paulson@13075: done
paulson@13075: 
paulson@13075: 
paulson@13075: text{*Expression evaluation is functional, or deterministic*}
paulson@13075: theorem single_valued_eval: "single_valued eval"
paulson@13075: apply (unfold single_valued_def)
wenzelm@18260: apply (intro allI, rule impI)
paulson@13075: apply (simp (no_asm_simp) only: split_tupled_all)
paulson@13075: apply (erule eval_induct)
paulson@13075: apply (drule_tac [4] com_Unique)
paulson@13075: apply (simp_all (no_asm_use))
paulson@13075: apply blast+
paulson@13075: done
paulson@13075: 
wenzelm@18260: lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
wenzelm@18260:   by (induct e == "N n" s v s' set: eval) simp_all
paulson@13075: 
paulson@13075: text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
wenzelm@18260: lemma while_true_E:
wenzelm@18260:     "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
wenzelm@18260:   by (induct set: exec) auto
paulson@13075: 
paulson@13075: 
wenzelm@18260: subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and
paulson@13075:        WHILE e DO c *}
paulson@13075: 
wenzelm@18260: lemma while_if1:
wenzelm@18260:      "(c',s) -[eval]-> t
wenzelm@18260:       ==> c' = WHILE e DO c ==>
paulson@13075:           (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
wenzelm@18260:   by (induct set: exec) auto
paulson@13075: 
wenzelm@18260: lemma while_if2:
paulson@13075:      "(c',s) -[eval]-> t
wenzelm@18260:       ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==>
paulson@13075:           (WHILE e DO c, s) -[eval]-> t"
wenzelm@18260:   by (induct set: exec) auto
paulson@13075: 
paulson@13075: 
paulson@13075: theorem while_if:
wenzelm@18260:      "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =
paulson@13075:       ((WHILE e DO c, s) -[eval]-> t)"
paulson@13075: by (blast intro: while_if1 while_if2)
paulson@13075: 
paulson@13075: 
paulson@13075: 
paulson@13075: subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
paulson@13075:                          and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
paulson@13075: 
wenzelm@18260: lemma if_semi1:
paulson@13075:      "(c',s) -[eval]-> t
wenzelm@18260:       ==> c' = (IF e THEN c1 ELSE c2);;c ==>
paulson@13075:           (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
wenzelm@18260:   by (induct set: exec) auto
paulson@13075: 
wenzelm@18260: lemma if_semi2:
paulson@13075:      "(c',s) -[eval]-> t
wenzelm@18260:       ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==>
paulson@13075:           ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
wenzelm@18260:   by (induct set: exec) auto
paulson@13075: 
wenzelm@18260: theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =
paulson@13075:                   ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
wenzelm@18260:   by (blast intro: if_semi1 if_semi2)
paulson@13075: 
paulson@13075: 
paulson@13075: 
paulson@13075: subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
paulson@13075:                   and  VALOF c1;;c2 RESULTIS e
paulson@13075:  *}
paulson@13075: 
wenzelm@18260: lemma valof_valof1:
wenzelm@18260:      "(e',s) -|-> (v,s')
wenzelm@18260:       ==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==>
paulson@13075:           (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
wenzelm@18260:   by (induct set: eval) auto
paulson@13075: 
wenzelm@18260: lemma valof_valof2:
paulson@13075:      "(e',s) -|-> (v,s')
wenzelm@18260:       ==> e' = VALOF c1;;c2 RESULTIS e ==>
paulson@13075:           (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
wenzelm@18260:   by (induct set: eval) auto
paulson@13075: 
paulson@13075: theorem valof_valof:
wenzelm@18260:      "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =
paulson@13075:       ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
wenzelm@18260:   by (blast intro: valof_valof1 valof_valof2)
paulson@13075: 
paulson@13075: 
paulson@13075: subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
paulson@13075: 
wenzelm@18260: lemma valof_skip1:
paulson@13075:      "(e',s) -|-> (v,s')
wenzelm@18260:       ==> e' = VALOF SKIP RESULTIS e ==>
paulson@13075:           (e, s) -|-> (v,s')"
wenzelm@18260:   by (induct set: eval) auto
paulson@13075: 
paulson@13075: lemma valof_skip2:
wenzelm@18260:     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
wenzelm@18260:   by blast
paulson@13075: 
paulson@13075: theorem valof_skip:
wenzelm@18260:     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
wenzelm@18260:   by (blast intro: valof_skip1 valof_skip2)
paulson@13075: 
paulson@13075: 
paulson@13075: subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
paulson@13075: 
wenzelm@18260: lemma valof_assign1:
paulson@13075:      "(e',s) -|-> (v,s'')
wenzelm@18260:       ==> e' = VALOF x:=e RESULTIS X x ==>
paulson@13075:           (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
wenzelm@18260:   by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto)
paulson@13075: 
paulson@13075: lemma valof_assign2:
wenzelm@18260:     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
wenzelm@18260:   by blast
paulson@13075: 
paulson@3120: end