9 |
9 |
10 ML {* |
10 ML {* |
11 fun pretty_terms ctxt trms = |
11 fun pretty_terms ctxt trms = |
12 Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms)) |
12 Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms)) |
13 *} |
13 *} |
14 |
|
15 lemma int_add_C :"x + (y::int) = y + x" |
|
16 by simp |
|
17 |
|
18 lemma int_add_A : "(x + y) + z = x + (y + (z::int))" |
|
19 by simp |
|
20 |
|
21 lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)" |
|
22 by simp |
|
23 |
|
24 lemmas int_add_ac = int_add_A int_add_C int_add_LC |
|
25 |
|
26 method_setup prune = |
|
27 {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} |
|
28 "pruning parameters" |
|
29 |
14 |
30 ML {* |
15 ML {* |
31 structure StepRules = Named_Thms |
16 structure StepRules = Named_Thms |
32 (val name = @{binding "step"} |
17 (val name = @{binding "step"} |
33 val description = "Theorems for hoare rules for every step") |
18 val description = "Theorems for hoare rules for every step") |
41 |
26 |
42 setup {* StepRules.setup *} |
27 setup {* StepRules.setup *} |
43 |
28 |
44 setup {* FwdRules.setup *} |
29 setup {* FwdRules.setup *} |
45 |
30 |
|
31 method_setup prune = |
|
32 {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} |
|
33 "pruning parameters" |
|
34 |
|
35 lemma int_add_C :"x + (y::int) = y + x" |
|
36 by simp |
|
37 |
|
38 lemma int_add_A : "(x + y) + z = x + (y + (z::int))" |
|
39 by simp |
|
40 |
|
41 lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)" |
|
42 by simp |
|
43 |
|
44 lemmas int_add_ac = int_add_A int_add_C int_add_LC |
|
45 |
|
46 |
46 section {* Operational Semantics of TM *} |
47 section {* Operational Semantics of TM *} |
47 |
48 |
48 datatype taction = W0 | W1 | L | R |
49 datatype taction = W0 | W1 | L | R |
49 |
50 |
50 type_synonym tstate = nat |
51 type_synonym tstate = nat |
53 |
54 |
54 datatype Block = Oc | Bk |
55 datatype Block = Oc | Bk |
55 |
56 |
56 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
57 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
57 |
58 |
58 fun next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
59 fun |
59 where "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" | |
60 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
60 "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" | |
61 where |
61 "next_tape L (pos, m) = (pos - 1, m)" | |
62 "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" | |
62 "next_tape R (pos, m) = (pos + 1, m)" |
63 "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" | |
|
64 "next_tape L (pos, m) = (pos - 1, m)" | |
|
65 "next_tape R (pos, m) = (pos + 1, m)" |
63 |
66 |
64 fun tstep :: "tconf \<Rightarrow> tconf" |
67 fun tstep :: "tconf \<Rightarrow> tconf" |
65 where "tstep (faults, prog, pc, pos, m) = |
68 where "tstep (faults, prog, pc, pos, m) = |
66 (case (prog pc) of |
69 (case (prog pc) of |
67 Some ((action0, pc0), (action1, pc1)) \<Rightarrow> |
70 Some ((action0, pc0), (action1, pc1)) \<Rightarrow> |
86 m pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and> |
89 m pos = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) \<and> |
87 (\<forall> faults prog pc pos m . |
90 (\<forall> faults prog pc pos m . |
88 s = (faults, prog, pc, pos, m) \<longrightarrow> |
91 s = (faults, prog, pc, pos, m) \<longrightarrow> |
89 prog pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) |
92 prog pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m)) |
90 )" |
93 )" |
91 by (case_tac s, auto split:option.splits Block.splits) |
94 by (cases s) (auto split: option.splits Block.splits) |
92 |
95 |
93 datatype tresource = |
96 datatype tresource = |
94 TM int Block |
97 TM int Block |
95 | TC nat tm_inst |
98 | TC nat tm_inst |
96 | TAt nat |
99 | TAt nat |
108 fun trset_of :: "tconf \<Rightarrow> tresource set" |
111 fun trset_of :: "tconf \<Rightarrow> tresource set" |
109 where "trset_of (faults, prog, pc, pos, m) = |
112 where "trset_of (faults, prog, pc, pos, m) = |
110 tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults" |
113 tprog_set prog \<union> tpc_set pc \<union> tpos_set pos \<union> tmem_set m \<union> tfaults_set faults" |
111 |
114 |
112 interpretation tm: sep_exec tstep trset_of . |
115 interpretation tm: sep_exec tstep trset_of . |
|
116 |
|
117 |
113 |
118 |
114 section {* Assembly language for TMs and its program logic *} |
119 section {* Assembly language for TMs and its program logic *} |
115 |
120 |
116 subsection {* The assembly language *} |
121 subsection {* The assembly language *} |
117 |
122 |
518 by simp |
523 by simp |
519 from t_hoare_label_last_pre[OF this[unfolded h1]] h2 |
524 from t_hoare_label_last_pre[OF this[unfolded h1]] h2 |
520 show ?thesis by auto |
525 show ?thesis by auto |
521 qed |
526 qed |
522 |
527 |
|
528 |
523 subsection {* Basic assertions for TM *} |
529 subsection {* Basic assertions for TM *} |
524 |
530 |
|
531 (* ones between tape position i and j *) |
525 function ones :: "int \<Rightarrow> int \<Rightarrow> tassert" where |
532 function ones :: "int \<Rightarrow> int \<Rightarrow> tassert" where |
526 "ones i j = (if j < i then <(i = j + 1)> else |
533 "ones i j = (if j < i then <(i = j + 1)> |
527 (one i) ** ones (i + 1) j)" |
534 else (one i) \<and>* ones (i + 1) j)" |
528 by auto |
535 by auto |
529 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto |
536 |
530 |
537 termination |
531 lemma ones_base_simp: "j < i \<Longrightarrow> ones i j = <(i = j + 1)>" |
538 by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto |
|
539 |
|
540 lemma ones_base_simp: |
|
541 "j < i \<Longrightarrow> ones i j = <(i = j + 1)>" |
532 by simp |
542 by simp |
533 |
543 |
534 lemma ones_step_simp: "\<not> j < i \<Longrightarrow> ones i j = ((one i) ** ones (i + 1) j)" |
544 lemma ones_step_simp: |
|
545 "\<not> j < i \<Longrightarrow> ones i j = ((one i) \<and>* ones (i + 1) j)" |
535 by simp |
546 by simp |
536 |
547 |
537 lemmas ones_simps = ones_base_simp ones_step_simp |
548 lemmas ones_simps = ones_base_simp ones_step_simp |
538 |
549 |
539 declare ones.simps [simp del] ones_simps [simp] |
550 declare ones.simps [simp del] ones_simps [simp] |
540 |
551 |
541 lemma ones_induct [case_names Base Step]: |
552 lemma ones_induct [case_names Base Step]: |
542 fixes P i j |
|
543 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
553 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
544 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) ** ones (i + 1) j)" |
554 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) \<and>* ones (i + 1) j)" |
545 shows "P i j (ones i j)" |
555 shows "P i j (ones i j)" |
546 proof(induct i j rule:ones.induct) |
556 proof(induct i j rule:ones.induct) |
547 fix i j |
557 fix i j |
548 assume ih: "(\<not> j < i \<Longrightarrow> P (i + 1) j (ones (i + 1) j))" |
558 assume ih: "(\<not> j < i \<Longrightarrow> P (i + 1) j (ones (i + 1) j))" |
549 show "P i j (ones i j)" |
559 show "P i j (ones i j)" |
558 with False show ?thesis by auto |
568 with False show ?thesis by auto |
559 qed |
569 qed |
560 qed |
570 qed |
561 |
571 |
562 function ones' :: "int \<Rightarrow> int \<Rightarrow> tassert" where |
572 function ones' :: "int \<Rightarrow> int \<Rightarrow> tassert" where |
563 "ones' i j = (if j < i then <(i = j + 1)> else |
573 "ones' i j = (if j < i then <(i = j + 1)> |
564 ones' i (j - 1) ** one j)" |
574 else ones' i (j - 1) \<and>* one j)" |
565 by auto |
575 by auto |
566 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto |
576 termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto |
567 |
577 |
568 lemma ones_rev: "\<not> j < i \<Longrightarrow> (ones i j) = ((ones i (j - 1)) ** one j)" |
578 lemma ones_rev: "\<not> j < i \<Longrightarrow> (ones i j) = ((ones i (j - 1)) ** one j)" |
569 proof(induct i j rule:ones_induct) |
579 proof(induct i j rule:ones_induct) |
582 by (auto simp:sep_conj_ac) |
592 by (auto simp:sep_conj_ac) |
583 qed |
593 qed |
584 qed |
594 qed |
585 |
595 |
586 lemma ones_rev_induct [case_names Base Step]: |
596 lemma ones_rev_induct [case_names Base Step]: |
587 fixes P i j |
|
588 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
597 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
589 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (ones i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((ones i (j - 1)) ** one j)" |
598 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (ones i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((ones i (j - 1)) ** one j)" |
590 shows "P i j (ones i j)" |
599 shows "P i j (ones i j)" |
591 proof(induct i j rule:ones'.induct) |
600 proof(induct i j rule:ones'.induct) |
592 fix i j |
601 fix i j |
620 |
629 |
621 declare zeros.simps [simp del] |
630 declare zeros.simps [simp del] |
622 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp |
631 lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp |
623 |
632 |
624 lemma zeros_induct [case_names Base Step]: |
633 lemma zeros_induct [case_names Base Step]: |
625 fixes P i j |
|
626 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
634 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
627 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (zeros (i + 1) j)\<rbrakk> \<Longrightarrow> |
635 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (zeros (i + 1) j)\<rbrakk> \<Longrightarrow> |
628 P i j ((zero i) ** zeros (i + 1) j)" |
636 P i j ((zero i) ** zeros (i + 1) j)" |
629 shows "P i j (zeros i j)" |
637 shows "P i j (zeros i j)" |
630 proof(induct i j rule:zeros.induct) |
638 proof(induct i j rule:zeros.induct) |
658 with Step show ?thesis by (auto simp:sep_conj_ac) |
666 with Step show ?thesis by (auto simp:sep_conj_ac) |
659 qed |
667 qed |
660 qed |
668 qed |
661 |
669 |
662 lemma zeros_rev_induct [case_names Base Step]: |
670 lemma zeros_rev_induct [case_names Base Step]: |
663 fixes P i j |
|
664 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
671 assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)" |
665 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (zeros i (j - 1))\<rbrakk> \<Longrightarrow> |
672 and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (zeros i (j - 1))\<rbrakk> \<Longrightarrow> |
666 P i j ((zeros i (j - 1)) ** zero j)" |
673 P i j ((zeros i (j - 1)) ** zero j)" |
667 shows "P i j (zeros i j)" |
674 shows "P i j (zeros i j)" |
668 proof(induct i j rule:ones'.induct) |
675 proof(induct i j rule:ones'.induct) |
680 with zeros_rev and False |
687 with zeros_rev and False |
681 show ?thesis by simp |
688 show ?thesis by simp |
682 qed |
689 qed |
683 qed |
690 qed |
684 |
691 |
685 definition "rep i j k = ((ones i (i + (int k))) ** <(j = i + int k)>)" |
692 definition "rep i j k = ((ones i (i + (int k))) \<and>* <(j = i + int k)>)" |
686 |
693 |
687 fun reps :: "int \<Rightarrow> int \<Rightarrow> nat list\<Rightarrow> tassert" |
694 fun reps :: "int \<Rightarrow> int \<Rightarrow> nat list\<Rightarrow> tassert" |
688 where |
695 where |
689 "reps i j [] = <(i = j + 1)>" | |
696 "reps i j [] = <(i = j + 1)>" | |
690 "reps i j [k] = (ones i (i + int k) ** <(j = i + int k)>)" | |
697 "reps i j [k] = (ones i (i + int k) ** <(j = i + int k)>)" | |
890 reps_len_cons[OF h(1)] |
897 reps_len_cons[OF h(1)] |
891 sep_conj_ac, subst ss, simp) |
898 sep_conj_ac, subst ss, simp) |
892 qed |
899 qed |
893 qed |
900 qed |
894 |
901 |
|
902 |
895 subsection {* A theory of list extension *} |
903 subsection {* A theory of list extension *} |
896 |
904 |
897 definition "list_ext n xs = xs @ replicate ((Suc n) - length xs) 0" |
905 definition "list_ext n xs = xs @ replicate ((Suc n) - length xs) 0" |
898 |
906 |
899 lemma list_ext_len_eq: "length (list_ext a xs) = length xs + (Suc a - length xs)" |
907 lemma list_ext_len_eq: "length (list_ext a xs) = length xs + (Suc a - length xs)" |
923 by (metis list_ext_len nth_list_update_eq) |
931 by (metis list_ext_len nth_list_update_eq) |
924 |
932 |
925 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)" |
933 lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)" |
926 by (metis not_less nth_append) |
934 by (metis not_less nth_append) |
927 |
935 |
|
936 (* FIXME in Hoare_gen? *) |
928 lemma pred_exI: |
937 lemma pred_exI: |
929 assumes "(P(x) \<and>* r) s" |
938 assumes "(P(x) \<and>* r) s" |
930 shows "((EXS x. P(x)) \<and>* r) s" |
939 shows "((EXS x. P(x)) \<and>* r) s" |
931 by (metis assms pred_ex_def sep_globalise) |
940 by (metis assms pred_ex_def sep_globalise) |
932 |
941 |