paulson@3120: (* Title: HOL/Induct/Com paulson@3120: ID: $Id$ 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@13075: theory Com = Main: paulson@3120: paulson@13075: typedecl loc paulson@13075: paulson@13075: types state = "loc => nat" paulson@13075: n2n2n = "nat => nat => nat" paulson@3120: wenzelm@12338: arities loc :: type paulson@3120: paulson@3120: datatype paulson@3120: exp = N nat paulson@3120: | X loc paulson@3120: | Op n2n2n exp exp nipkow@10759: | valOf com exp ("VALOF _ RESULTIS _" 60) nipkow@10759: and nipkow@10759: com = SKIP paulson@3120: | ":=" loc exp (infixl 60) nipkow@10759: | Semi com com ("_;;_" [60, 60] 60) nipkow@10759: | Cond exp com com ("IF _ THEN _ ELSE _" 60) nipkow@10759: | While exp com ("WHILE _ DO _" 60) paulson@3120: paulson@13075: text{* Execution of commands *} nipkow@10759: consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" paulson@3120: "@exec" :: "((exp*state) * (nat*state)) set => nipkow@10759: [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50) paulson@3120: paulson@13075: translations "csig -[eval]-> s" == "(csig,s) \ exec eval" paulson@3120: oheimb@4264: syntax eval' :: "[exp*state,nat*state] => oheimb@4264: ((exp*state) * (nat*state)) set => bool" paulson@13075: ("_/ -|[_]-> _" [50,0,50] 50) oheimb@4264: paulson@13075: translations paulson@13075: "esig -|[eval]-> ns" => "(esig,ns) \ eval" paulson@3120: paulson@13075: text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*} paulson@13075: inductive "exec eval" paulson@13075: intros paulson@13075: Skip: "(SKIP,s) -[eval]-> s" paulson@3120: paulson@13075: Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)" paulson@3120: paulson@13075: Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] paulson@13075: ==> (c0 ;; c1, s) -[eval]-> s1" paulson@13075: paulson@13075: IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] paulson@3120: ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" paulson@3120: paulson@13075: IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] paulson@13075: ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" paulson@13075: paulson@13075: WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) paulson@13075: ==> (WHILE e DO c, s) -[eval]-> s1" paulson@13075: paulson@13075: WhileTrue: "[| (e,s) -|[eval]-> (0,s1); paulson@13075: (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 paulson@13075: [elim!]: "(SKIP,s) -[eval]-> t" paulson@13075: and [elim!]: "(x:=a,s) -[eval]-> t" paulson@13075: and [elim!]: "(c1;;c2, s) -[eval]-> t" paulson@13075: and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t" paulson@13075: 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)" paulson@13075: apply (unfold exec.defs ) paulson@13075: apply (rule lfp_mono) paulson@13075: apply (assumption | rule basic_monos)+ paulson@13075: done paulson@13075: paulson@13075: ML {* paulson@13075: Unify.trace_bound := 30; paulson@13075: Unify.search_bound := 60; paulson@13075: *} paulson@13075: 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) paulson@13075: 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@13075: section {* Expressions *} paulson@13075: paulson@13075: text{* Evaluation of arithmetic expressions *} paulson@13075: consts eval :: "((exp*state) * (nat*state)) set" paulson@13075: "-|->" :: "[exp*state,nat*state] => bool" (infixl 50) paulson@13075: paulson@13075: translations paulson@13075: "esig -|-> (n,s)" <= "(esig,n,s) \ eval" paulson@13075: "esig -|-> ns" == "(esig,ns ) \ eval" paulson@13075: paulson@13075: inductive eval paulson@13075: intros paulson@13075: N [intro!]: "(N(n),s) -|-> (n,s)" paulson@13075: paulson@13075: X [intro!]: "(X(x),s) -|-> (s(x),s)" paulson@13075: paulson@13075: Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] paulson@13075: ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)" paulson@13075: paulson@13075: 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 paulson@13075: [elim!]: "(N(n),sigma) -|-> (n',s')" paulson@13075: and [elim!]: "(X(x),sigma) -|-> (n,s')" paulson@13075: and [elim!]: "(Op f a1 a2,sigma) -|-> (n,s')" paulson@13075: 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))" paulson@13075: by (rule fun_upd_same [THEN subst], fast) paulson@13075: paulson@13075: paulson@13075: text{* Make the induction rule look nicer -- though eta_contract makes the new paulson@13075: version look worse than it is...*} paulson@13075: paulson@13075: lemma split_lemma: paulson@13075: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))" paulson@13075: by auto paulson@13075: paulson@13075: text{*New induction rule. Note the form of the VALOF induction hypothesis*} paulson@13075: lemma eval_induct: paulson@13075: "[| (e,s) -|-> (n,s'); paulson@13075: !!n s. P (N n) s n s; paulson@13075: !!s x. P (X x) s (s x) s; paulson@13075: !!e0 e1 f n0 n1 s s0 s1. paulson@13075: [| (e0,s) -|-> (n0,s0); P e0 s n0 s0; paulson@13075: (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1 paulson@13075: |] ==> P (Op f e0 e1) s (f n0 n1) s1; paulson@13075: !!c e n s s0 s1. paulson@13075: [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; paulson@13075: (c,s) -[eval]-> s0; paulson@13075: (e,s0) -|-> (n,s1); P e s0 n s1 |] paulson@13075: ==> P (VALOF c RESULTIS e) s n s1 paulson@13075: |] ==> P e s n s'" paulson@13075: apply (erule eval.induct, blast) paulson@13075: apply blast paulson@13075: 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: paulson@13075: text{*Lemma for Function_eval. The major premise is that (c,s) executes to s1 paulson@13075: using eval restricted to its functional part. Note that the execution paulson@13075: (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that paulson@13075: the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is paulson@13075: functional on the argument (c,s). paulson@13075: *} paulson@13075: lemma com_Unique: paulson@13075: "(c,s) -[eval Int {((e,s),(n,t)). \nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 paulson@13075: ==> \s2. (c,s) -[eval]-> s2 --> s2=s1" paulson@13075: apply (erule exec.induct, 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 paulson@13075: 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) paulson@13075: 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: paulson@13075: paulson@13075: lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)" paulson@13075: by (erule eval_induct, simp_all) paulson@13075: paulson@13075: lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl] paulson@13075: paulson@13075: paulson@13075: text{*This theorem says that "WHILE TRUE DO c" cannot terminate*} paulson@13075: lemma while_true_E [rule_format]: paulson@13075: "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False" paulson@13075: by (erule exec.induct, auto) paulson@13075: paulson@13075: paulson@13075: subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and paulson@13075: WHILE e DO c *} paulson@13075: paulson@13075: lemma while_if1 [rule_format]: paulson@13075: "(c',s) -[eval]-> t paulson@13075: ==> (c' = WHILE e DO c) --> paulson@13075: (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t" paulson@13075: by (erule exec.induct, auto) paulson@13075: paulson@13075: lemma while_if2 [rule_format]: paulson@13075: "(c',s) -[eval]-> t paulson@13075: ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> paulson@13075: (WHILE e DO c, s) -[eval]-> t" paulson@13075: by (erule exec.induct, auto) paulson@13075: paulson@13075: paulson@13075: theorem while_if: paulson@13075: "((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: paulson@13075: lemma if_semi1 [rule_format]: paulson@13075: "(c',s) -[eval]-> t paulson@13075: ==> (c' = (IF e THEN c1 ELSE c2);;c) --> paulson@13075: (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t" paulson@13075: by (erule exec.induct, auto) paulson@13075: paulson@13075: lemma if_semi2 [rule_format]: paulson@13075: "(c',s) -[eval]-> t paulson@13075: ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> paulson@13075: ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t" paulson@13075: by (erule exec.induct, auto) paulson@13075: paulson@13075: 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)" paulson@13075: 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: paulson@13075: lemma valof_valof1 [rule_format]: paulson@13075: "(e',s) -|-> (v,s') paulson@13075: ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> paulson@13075: (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')" paulson@13075: by (erule eval_induct, auto) paulson@13075: paulson@13075: paulson@13075: lemma valof_valof2 [rule_format]: paulson@13075: "(e',s) -|-> (v,s') paulson@13075: ==> (e' = VALOF c1;;c2 RESULTIS e) --> paulson@13075: (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')" paulson@13075: by (erule eval_induct, auto) paulson@13075: paulson@13075: theorem valof_valof: paulson@13075: "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = paulson@13075: ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))" paulson@13075: by (blast intro: valof_valof1 valof_valof2) paulson@13075: paulson@13075: paulson@13075: subsection{* Equivalence of VALOF SKIP RESULTIS e and e *} paulson@13075: paulson@13075: lemma valof_skip1 [rule_format]: paulson@13075: "(e',s) -|-> (v,s') paulson@13075: ==> (e' = VALOF SKIP RESULTIS e) --> paulson@13075: (e, s) -|-> (v,s')" paulson@13075: by (erule eval_induct, auto) paulson@13075: paulson@13075: lemma valof_skip2: paulson@13075: "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')" paulson@13075: by blast paulson@13075: paulson@13075: theorem valof_skip: paulson@13075: "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))" paulson@13075: 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: paulson@13075: lemma valof_assign1 [rule_format]: paulson@13075: "(e',s) -|-> (v,s'') paulson@13075: ==> (e' = VALOF x:=e RESULTIS X x) --> paulson@13075: (\s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))" paulson@13075: apply (erule eval_induct) paulson@13075: apply (simp_all del: fun_upd_apply, clarify, auto) paulson@13075: done paulson@13075: paulson@13075: lemma valof_assign2: paulson@13075: "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))" paulson@13075: by blast paulson@13075: paulson@13075: paulson@3120: end