--- 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) \<in> 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) \<in> 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) \<in> eval"
"esig -|-> ns" == "(esig,ns ) \<in> 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)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
+ "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
==> \<forall>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 ==>
(\<exists>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
--- 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 \<in> tt)"
+ "tt[[#v]] = (v \<in> 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 ==> \<forall>t. hyps p t - hyps p t0 |- p"
+ "{} |= p ==> \<forall>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 ==> \<forall>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
-