# HG changeset patch # User wenzelm # Date 1132949674 -3600 # Node ID 5597cfcecd49dbd6ecc96e6269e3012404d76b62 # Parent 7b14579c58f290a2abf5b4f4333a91c2bec479ec tuned induct proofs; diff -r 7b14579c58f2 -r 5597cfcecd49 src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Fri Nov 25 20:57:51 2005 +0100 +++ b/src/HOL/Induct/Com.thy Fri Nov 25 21:14:34 2005 +0100 @@ -34,14 +34,14 @@ text{* Execution of commands *} consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" - "@exec" :: "((exp*state) * (nat*state)) set => +syntax "@exec" :: "((exp*state) * (nat*state)) set => [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50) translations "csig -[eval]-> s" == "(csig,s) \ exec eval" -syntax eval' :: "[exp*state,nat*state] => - ((exp*state) * (nat*state)) set => bool" - ("_/ -|[_]-> _" [50,0,50] 50) +syntax eval' :: "[exp*state,nat*state] => + ((exp*state) * (nat*state)) set => bool" + ("_/ -|[_]-> _" [50,0,50] 50) translations "esig -|[eval]-> ns" => "(esig,ns) \ eval" @@ -53,31 +53,31 @@ Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)" - Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] + Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] ==> (c0 ;; c1, s) -[eval]-> s1" - IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] + IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |] ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" - IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] + IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |] ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1" - WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) + WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1" WhileTrue: "[| (e,s) -|[eval]-> (0,s1); - (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] + (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |] ==> (WHILE e DO c, s) -[eval]-> s3" declare exec.intros [intro] inductive_cases - [elim!]: "(SKIP,s) -[eval]-> t" + [elim!]: "(SKIP,s) -[eval]-> t" and [elim!]: "(x:=a,s) -[eval]-> t" - and [elim!]: "(c1;;c2, s) -[eval]-> t" - and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t" - and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t" + and [elim!]: "(c1;;c2, s) -[eval]-> t" + and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t" + and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t" text{*Justifies using "exec" in the inductive definition of "eval"*} @@ -95,7 +95,7 @@ text{*Command execution is functional (deterministic) provided evaluation is*} theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)" apply (simp add: single_valued_def) -apply (intro allI) +apply (intro allI) apply (rule impI) apply (erule exec.induct) apply (blast elim: exec_WHILE_case)+ @@ -111,27 +111,27 @@ translations "esig -|-> (n,s)" <= "(esig,n,s) \ eval" "esig -|-> ns" == "(esig,ns ) \ eval" - + inductive eval - intros + intros N [intro!]: "(N(n),s) -|-> (n,s)" X [intro!]: "(X(x),s) -|-> (s(x),s)" - Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] + Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |] ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)" - valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |] + valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |] ==> (VALOF c RESULTIS e, s) -|-> (n, s1)" monos exec_mono inductive_cases - [elim!]: "(N(n),sigma) -|-> (n',s')" + [elim!]: "(N(n),sigma) -|-> (n',s')" and [elim!]: "(X(x),sigma) -|-> (n,s')" - and [elim!]: "(Op f a1 a2,sigma) -|-> (n,s')" - and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)" + and [elim!]: "(Op f a1 a2,sigma) -|-> (n,s')" + and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)" lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))" @@ -146,23 +146,25 @@ by auto text{*New induction rule. Note the form of the VALOF induction hypothesis*} -lemma eval_induct: - "[| (e,s) -|-> (n,s'); - !!n s. P (N n) s n s; - !!s x. P (X x) s (s x) s; - !!e0 e1 f n0 n1 s s0 s1. - [| (e0,s) -|-> (n0,s0); P e0 s n0 s0; - (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1 - |] ==> P (Op f e0 e1) s (f n0 n1) s1; - !!c e n s s0 s1. - [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; - (c,s) -[eval]-> s0; - (e,s0) -|-> (n,s1); P e s0 n s1 |] - ==> P (VALOF c RESULTIS e) s n s1 +lemma eval_induct + [case_names N X Op valOf, consumes 1, induct set: eval]: + "[| (e,s) -|-> (n,s'); + !!n s. P (N n) s n s; + !!s x. P (X x) s (s x) s; + !!e0 e1 f n0 n1 s s0 s1. + [| (e0,s) -|-> (n0,s0); P e0 s n0 s0; + (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1 + |] ==> P (Op f e0 e1) s (f n0 n1) s1; + !!c e n s s0 s1. + [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; + (c,s) -[eval]-> s0; + (e,s0) -|-> (n,s1); P e s0 n s1 |] + ==> P (VALOF c RESULTIS e) s n s1 |] ==> P e s n s'" -apply (erule eval.induct, blast) -apply blast -apply blast +apply (induct set: eval) +apply blast +apply blast +apply blast apply (frule Int_lower1 [THEN exec_mono, THEN subsetD]) apply (auto simp add: split_lemma) done @@ -170,14 +172,15 @@ text{*Lemma for Function_eval. The major premise is that (c,s) executes to s1 using eval restricted to its functional part. Note that the execution - (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that + (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is functional on the argument (c,s). *} lemma com_Unique: - "(c,s) -[eval Int {((e,s),(n,t)). \nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 + "(c,s) -[eval Int {((e,s),(n,t)). \nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 ==> \s2. (c,s) -[eval]-> s2 --> s2=s1" -apply (erule exec.induct, simp_all) +apply (induct set: exec) + apply simp_all apply blast apply force apply blast @@ -186,14 +189,14 @@ apply (blast elim: exec_WHILE_case) apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl) apply clarify -apply (erule exec_WHILE_case, blast+) +apply (erule exec_WHILE_case, blast+) done text{*Expression evaluation is functional, or deterministic*} theorem single_valued_eval: "single_valued eval" apply (unfold single_valued_def) -apply (intro allI, rule impI) +apply (intro allI, rule impI) apply (simp (no_asm_simp) only: split_tupled_all) apply (erule eval_induct) apply (drule_tac [4] com_Unique) @@ -201,37 +204,33 @@ apply blast+ done - -lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)" -by (erule eval_induct, simp_all) - -lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl] - +lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)" + by (induct e == "N n" s v s' set: eval) simp_all text{*This theorem says that "WHILE TRUE DO c" cannot terminate*} -lemma while_true_E [rule_format]: - "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False" -by (erule exec.induct, auto) +lemma while_true_E: + "(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False" + by (induct set: exec) auto -subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and +subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and WHILE e DO c *} -lemma while_if1 [rule_format]: - "(c',s) -[eval]-> t - ==> (c' = WHILE e DO c) --> +lemma while_if1: + "(c',s) -[eval]-> t + ==> c' = WHILE e DO c ==> (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t" -by (erule exec.induct, auto) + by (induct set: exec) auto -lemma while_if2 [rule_format]: +lemma while_if2: "(c',s) -[eval]-> t - ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> + ==> c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP ==> (WHILE e DO c, s) -[eval]-> t" -by (erule exec.induct, auto) + by (induct set: exec) auto theorem while_if: - "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) = + "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) = ((WHILE e DO c, s) -[eval]-> t)" by (blast intro: while_if1 while_if2) @@ -240,21 +239,21 @@ subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c and IF e THEN (c1;;c) ELSE (c2;;c) *} -lemma if_semi1 [rule_format]: +lemma if_semi1: "(c',s) -[eval]-> t - ==> (c' = (IF e THEN c1 ELSE c2);;c) --> + ==> c' = (IF e THEN c1 ELSE c2);;c ==> (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t" -by (erule exec.induct, auto) + by (induct set: exec) auto -lemma if_semi2 [rule_format]: +lemma if_semi2: "(c',s) -[eval]-> t - ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> + ==> c' = IF e THEN (c1;;c) ELSE (c2;;c) ==> ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t" -by (erule exec.induct, auto) + by (induct set: exec) auto -theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) = +theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) = ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)" -by (blast intro: if_semi1 if_semi2) + by (blast intro: if_semi1 if_semi2) @@ -262,55 +261,51 @@ and VALOF c1;;c2 RESULTIS e *} -lemma valof_valof1 [rule_format]: - "(e',s) -|-> (v,s') - ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> +lemma valof_valof1: + "(e',s) -|-> (v,s') + ==> e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e) ==> (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')" -by (erule eval_induct, auto) + by (induct set: eval) auto - -lemma valof_valof2 [rule_format]: +lemma valof_valof2: "(e',s) -|-> (v,s') - ==> (e' = VALOF c1;;c2 RESULTIS e) --> + ==> e' = VALOF c1;;c2 RESULTIS e ==> (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')" -by (erule eval_induct, auto) + by (induct set: eval) auto theorem valof_valof: - "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = + "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))" -by (blast intro: valof_valof1 valof_valof2) + by (blast intro: valof_valof1 valof_valof2) subsection{* Equivalence of VALOF SKIP RESULTIS e and e *} -lemma valof_skip1 [rule_format]: +lemma valof_skip1: "(e',s) -|-> (v,s') - ==> (e' = VALOF SKIP RESULTIS e) --> + ==> e' = VALOF SKIP RESULTIS e ==> (e, s) -|-> (v,s')" -by (erule eval_induct, auto) + by (induct set: eval) auto lemma valof_skip2: - "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')" -by blast + "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')" + by blast theorem valof_skip: - "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))" -by (blast intro: valof_skip1 valof_skip2) + "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))" + by (blast intro: valof_skip1 valof_skip2) subsection{* Equivalence of VALOF x:=e RESULTIS x and e *} -lemma valof_assign1 [rule_format]: +lemma valof_assign1: "(e',s) -|-> (v,s'') - ==> (e' = VALOF x:=e RESULTIS X x) --> + ==> e' = VALOF x:=e RESULTIS X x ==> (\s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))" -apply (erule eval_induct) -apply (simp_all del: fun_upd_apply, clarify, auto) -done + by (induct set: eval) (simp_all del: fun_upd_apply, clarify, auto) lemma valof_assign2: - "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))" -by blast - + "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))" + by blast end diff -r 7b14579c58f2 -r 5597cfcecd49 src/HOL/Induct/PropLog.thy --- a/src/HOL/Induct/PropLog.thy Fri Nov 25 20:57:51 2005 +0100 +++ b/src/HOL/Induct/PropLog.thy Fri Nov 25 21:14:34 2005 +0100 @@ -49,7 +49,7 @@ eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100) primrec "tt[[false]] = False" - "tt[[#v]] = (v \ tt)" + "tt[[#v]] = (v \ tt)" eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])" text {* @@ -108,8 +108,8 @@ subsubsection {* The deduction theorem *} theorem deduction: "insert p H |- q ==> H |- p->q" -apply (erule thms.induct) -apply (fast intro: thms_I thms.H thms.K thms.S thms.DN +apply (induct set: thms) +apply (fast intro: thms_I thms.H thms.K thms.S thms.DN thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+ done @@ -127,7 +127,8 @@ theorem soundness: "H |- p ==> H |= p" apply (unfold sat_def) -apply (erule thms.induct, auto) +apply (induct set: thms) +apply auto done subsection {* Completeness *} @@ -143,23 +144,23 @@ lemma imp_false: "[| H |- p; H |- q->false |] ==> H |- (p->q)->false" apply (rule deduction) -apply (blast intro: weaken_left_insert thms.MP thms.H) +apply (blast intro: weaken_left_insert thms.MP thms.H) done lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)" -- {* Typical example of strengthening the induction statement. *} -apply simp -apply (induct_tac "p") +apply simp +apply (induct p) apply (simp_all add: thms_I thms.H) apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right imp_false false_imp) done lemma sat_thms_p: "{} |= p ==> hyps p tt |- p" - -- {* Key lemma for completeness; yields a set of assumptions + -- {* Key lemma for completeness; yields a set of assumptions satisfying @{text p} *} -apply (unfold sat_def) -apply (drule spec, erule mp [THEN if_P, THEN subst], +apply (unfold sat_def) +apply (drule spec, erule mp [THEN if_P, THEN subst], rule_tac [2] hyps_thms_if, simp) done @@ -176,13 +177,13 @@ lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q" apply (rule deduction [THEN deduction]) -apply (rule thms.DN [THEN thms.MP], best) +apply (rule thms.DN [THEN thms.MP], best) done lemma thms_excluded_middle_rule: "[| insert p H |- q; insert (p->false) H |- q |] ==> H |- q" -- {* Hard to prove directly because it requires cuts *} -by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) +by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) subsection{* Completeness -- lemmas for reducing the set of assumptions*} @@ -193,7 +194,7 @@ *} lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})" -by (induct_tac "p", auto) +by (induct p) auto text {* For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have @@ -201,7 +202,7 @@ *} lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})" -by (induct_tac "p", auto) +by (induct p) auto text {* Two lemmas for use with @{text weaken_left} *} @@ -217,10 +218,10 @@ *} lemma hyps_finite: "finite(hyps p t)" -by (induct_tac "p", auto) +by (induct p) auto lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})" -by (induct_tac "p", auto) +by (induct p) auto lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left] @@ -232,18 +233,18 @@ *} lemma completeness_0_lemma: - "{} |= p ==> \t. hyps p t - hyps p t0 |- p" + "{} |= p ==> \t. hyps p t - hyps p t0 |- p" apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]]) apply (simp add: sat_thms_p, safe) txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *} - apply (iprover intro: thms_excluded_middle_rule - insert_Diff_same [THEN weaken_left] - insert_Diff_subset2 [THEN weaken_left] + apply (iprover intro: thms_excluded_middle_rule + insert_Diff_same [THEN weaken_left] + insert_Diff_subset2 [THEN weaken_left] hyps_Diff [THEN Diff_weaken_left]) txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *} - apply (iprover intro: thms_excluded_middle_rule - insert_Diff_same [THEN weaken_left] - insert_Diff_subset2 [THEN weaken_left] + apply (iprover intro: thms_excluded_middle_rule + insert_Diff_same [THEN weaken_left] + insert_Diff_subset2 [THEN weaken_left] hyps_insert [THEN Diff_weaken_left]) done @@ -257,8 +258,8 @@ lemma sat_imp: "insert p H |= q ==> H |= p->q" by (unfold sat_def, auto) -theorem completeness [rule_format]: "finite H ==> \p. H |= p --> H |- p" -apply (erule finite_induct) +theorem completeness: "finite H ==> H |= p ==> H |- p" +apply (induct fixing: p rule: finite_induct) apply (blast intro: completeness_0) apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP]) done @@ -267,4 +268,3 @@ by (blast intro: soundness completeness) end -