Isabelle Task 4 complete

This commit is contained in:
Aadi Desai 2022-12-15 18:17:18 +00:00
parent a59839d924
commit a926e4e941
No known key found for this signature in database
GPG key ID: CFFFE425830EF4D9

View file

@ -141,9 +141,6 @@ next
qed(simp+) qed(simp+)
section "Task 4: More logic optimisation" section "Task 4: More logic optimisation"
(* Note: - opt_redundancy is shown to be valid (opt_redundancy_is_sound)
- opt_redundancy never increases area is incomplete (opt_redundancy_never_inc_area)
*)
(* An optimisation that exploits the following Boolean identities: (* An optimisation that exploits the following Boolean identities:
`a | (a & b) = a` `a | (a & b) = a`
@ -157,30 +154,26 @@ fun opt_redundancy :: "circuit \<Rightarrow> circuit" where
let c1' = opt_redundancy c1 in let c1' = opt_redundancy c1 in
let c2' = opt_redundancy c2 in let c2' = opt_redundancy c2 in
let c3' = opt_redundancy c3 in let c3' = opt_redundancy c3 in
if (c1' = c2') | (c1' = c3') then c1' if c1' = c2' | c1' = c3' then c1'
else if c2' = c3' then OR c1' c2' else OR c1' (AND c2' c3'))"
else OR c1' (opt_redundancy (AND c2 c3)))"
| "opt_redundancy (OR (AND c1 c2) c3) = ( | "opt_redundancy (OR (AND c1 c2) c3) = (
let c1' = opt_redundancy c1 in let c1' = opt_redundancy c1 in
let c2' = opt_redundancy c2 in let c2' = opt_redundancy c2 in
let c3' = opt_redundancy c3 in let c3' = opt_redundancy c3 in
if (c1' = c3') | (c2' = c3') then c3' if c1' = c3' | c2' = c3' then c3'
else if c1' = c2' then OR c1' c3' else (OR (AND c1' c2') c3'))"
else OR (opt_redundancy (AND c1 c2)) c3')"
| "opt_redundancy (AND c1 (OR c2 c3)) = ( | "opt_redundancy (AND c1 (OR c2 c3)) = (
let c1' = opt_redundancy c1 in let c1' = opt_redundancy c1 in
let c2' = opt_redundancy c2 in let c2' = opt_redundancy c2 in
let c3' = opt_redundancy c3 in let c3' = opt_redundancy c3 in
if (c1' = c2') | (c1' = c3') then c1' if c1' = c2' | c1' = c3' then c1'
else if c2' = c3' then AND c1' c2' else AND c1' (OR c2' c3'))"
else AND c1' (opt_redundancy (OR c2 c3)))"
| "opt_redundancy (AND (OR c1 c2) c3) = ( | "opt_redundancy (AND (OR c1 c2) c3) = (
let c1' = opt_redundancy c1 in let c1' = opt_redundancy c1 in
let c2' = opt_redundancy c2 in let c2' = opt_redundancy c2 in
let c3' = opt_redundancy c3 in let c3' = opt_redundancy c3 in
if (c1' = c3') | (c2' = c3') then c3' if c1' = c3' | c2' = c3' then c3'
else if c1' = c2' then AND c1' c3' else (AND (OR c1' c2') c3'))"
else AND (opt_redundancy (OR c1 c2)) c3')"
| "opt_redundancy (AND c1 c2) = ( | "opt_redundancy (AND c1 c2) = (
let c1' = opt_redundancy c1 in let c1' = opt_redundancy c1 in
let c2' = opt_redundancy c2 in let c2' = opt_redundancy c2 in
@ -329,120 +322,79 @@ next
qed(simp+) qed(simp+)
theorem opt_redundancy_never_inc_area: "area (opt_redundancy c) \<le> area c" theorem opt_redundancy_never_inc_area: "area (opt_redundancy c) \<le> area c"
proof (induct rule:opt_redundancy.induct) proof (induct rule:opt_redundancy.induct) case (2 c1 c2 c3)
case (2 c1 c2 c3) thus ?case by (smt (verit, ccfv_threshold) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) circuit.inject(3) not_less_eq_eq opt_redundancy.simps(2) plus_1_eq_Suc)
(* area (opt_redundancy (OR c1 (AND c2 c3))) \<le> area (OR c1 (AND c2 c3)) *) next case ("3_1" c1 c2 c3)
thus ?case by (smt (verit, del_insts) add_leE add_mono_thms_linordered_semiring(1) area.simps(3) area.simps(2) nle_le opt_redundancy.simps(3))
next case ("3_2" c1 c2 c3 c4)
thus ?case by (smt (verit, ccfv_threshold) Suc_leI add_mono_thms_linordered_semiring(1) area.simps(3) area.simps(2) less_Suc_eq_le opt_redundancy.simps(4) plus_1_eq_Suc trans_le_add2)
next case ("3_3" c1 c2)
thus ?case by (smt (verit) add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) area.simps(4) dual_order.eq_iff less_Suc_eq_0_disj less_Suc_eq_le opt_redundancy.simps(5))
next case ("3_4" c1 c2)
thus ?case by (smt (verit) add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) area.simps(5) dual_order.eq_iff less_Suc_eq_0_disj less_Suc_eq_le opt_redundancy.simps(6))
next case ("3_5" c1 c2 c3)
let ?c1' = "opt_redundancy c1" let ?c1' = "opt_redundancy c1"
let ?c2' = "opt_redundancy c2" let ?c2' = "opt_redundancy c2"
let ?c3' = "opt_redundancy c3" from "3_5" have IH:"area (OR (AND ?c1' ?c2') (INPUT c3)) \<le> area (OR (AND c1 c2) (INPUT c3))" by auto
from 2 have IH:"area (OR ?c1' (AND ?c2' ?c3')) \<le> area (OR c1 (AND c2 c3))" by fastforce hence "area (opt_redundancy (OR (AND c1 c2) (INPUT c3))) \<le> area (OR (AND ?c1' ?c2') (INPUT c3))"
have a:"(area (opt_redundancy (OR c1 (AND c2 c3))) = area ?c1') by (smt area.simps(6) bot_nat_0.extremum_unique nat_le_linear opt_redundancy.simps(66) opt_redundancy.simps(7))
\<or> (area (opt_redundancy (OR c1 (AND c2 c3))) = area (OR ?c1' ?c2')) thus ?case using IH by linarith
\<or> (area (opt_redundancy (OR c1 (AND c2 c3))) = area (OR ?c1' (opt_redundancy (AND c2 c3))))" next case (4 c1 c2 c3)
by (smt opt_redundancy.simps(2)) thus ?case by (smt (verit, ccfv_threshold) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) not_less_eq_eq opt_redundancy.simps(8) plus_1_eq_Suc)
have b:"area ?c1' \<le> area (OR c1 (AND c2 c3))" using IH by simp next case ("5_1" c1 c2 c3)
have c:"area (OR ?c1' ?c2') \<le> area (OR c1 (AND c2 c3))" using IH by simp thus ?case by (smt (verit, del_insts) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) nle_le opt_redundancy.simps(9))
have d:"area (OR ?c1' (opt_redundancy (AND c2 c3))) \<le> area (OR c1 (AND c2 c3))" using IH sorry next case ("5_2" c1 c2 c3 c4)
thus ?case using a b c d by metis thus ?case by (smt (verit, del_insts) Suc_leI add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) less_Suc_eq_le opt_redundancy.simps(10) plus_1_eq_Suc trans_le_add2)
next next case ("5_3" c1 c2)
case ("3_1" c1 c2 v) thus ?case by (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) area.simps(4) bot_nat_0.extremum_unique nat_le_linear opt_redundancy.simps(11))
thus ?case sorry next case ("5_4" c1 c2)
next thus ?case by (smt (verit, ccfv_threshold) add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) area.simps(5) bot_nat_0.extremum_unique nat_le_linear opt_redundancy.simps(12))
case ("3_2" c1 c2 v va) next case ("5_5" c1 c2 c3)
thus ?case sorry thus ?case by (smt (verit, del_insts) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(3) not_less_eq_eq opt_redundancy.simps(13) plus_1_eq_Suc)
next next case ("6_1" c1 c2)
case ("3_3" c1 c2) thus ?case by (smt (verit) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) not_less_eq_eq opt_redundancy.simps(14) plus_1_eq_Suc)
thus ?case sorry next case ("6_2" c1 c2 c3)
next thus ?case by (smt (verit) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) nat_le_linear opt_redundancy.simps(15))
case ("3_4" c1 c2) next case ("6_6" c1 c2 c3)
thus ?case sorry thus ?case by (smt (verit) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) not_less_eq_eq opt_redundancy.simps(19) plus_1_eq_Suc)
next next case ("6_7" c1 c2 c3 c4)
case ("3_5" c1 c2 v) thus ?case by (smt add_leD1 add_le_mono area.simps(2) le_cases3 not_less_eq_eq opt_redundancy.simps(20) plus_1_eq_Suc)
thus ?case sorry next case ("6_8" c1 c2)
next thus ?case by (smt One_nat_def area.simps(2) area.simps(4) nat_le_linear not_less_eq_eq opt_redundancy.simps(21) opt_redundancy.simps(64) plus_1_eq_Suc)
case (4 c1 c2 c3) next case ("6_9" c1 c2)
thus ?case sorry thus ?case by (smt One_nat_def area.simps(2) area.simps(5) nat_le_linear not_less_eq_eq opt_redundancy.simps(22) opt_redundancy.simps(65) plus_1_eq_Suc)
next next case ("6_10" c1 c2 c3)
case ("5_1" c1 c2 v) thus ?case by (smt One_nat_def area.simps(2) area.simps(6) nat_le_linear not_less_eq_eq opt_redundancy.simps(23) opt_redundancy.simps(66) plus_1_eq_Suc)
thus ?case sorry next case ("6_12" c1 c2)
next thus ?case by (smt add_cancel_right_right area.simps(2) area.simps(4) linorder_linear not_less_eq_eq opt_redundancy.simps(25) opt_redundancy.simps(64) plus_1_eq_Suc)
case ("5_2" c1 c2 v va) next case ("6_17" c1 c2)
thus ?case sorry thus ?case by (smt (verit) add_leE add_mono_thms_linordered_semiring(1) area.simps(2) not_less_eq_eq opt_redundancy.simps(30) plus_1_eq_Suc)
next next case ("6_22" c1 c2 c3)
case ("5_3" c1 c2) thus ?case by (smt add_cancel_right_right add_mono_thms_linordered_semiring(1) area.simps(2) area.simps(6) nat_le_linear not_less_eq_eq opt_redundancy.simps(35) plus_1_eq_Suc)
thus ?case sorry next case ("6_25" c1 c2)
next thus ?case by (metis (full_types) area.simps(6) bot_nat_0.extremum opt_redundancy.simps(38) opt_redundancy.simps(66) verit_comp_simplify1(2))
case ("5_4" c1 c2) next case ("7_1" c1 c2)
thus ?case sorry thus ?case by (smt (verit) Suc_leI add_mono_thms_linordered_semiring(1) area.simps(3) le_imp_less_Suc opt_redundancy.simps(39) plus_1_eq_Suc trans_le_add2)
next next case ("7_2" c1 c2 c3)
case ("5_5" c1 c2 v) thus ?case by (smt (verit) add_leD1 add_mono_thms_linordered_semiring(1) area.simps(3) nat_le_linear not_less_eq_eq opt_redundancy.simps(40) plus_1_eq_Suc)
thus ?case sorry next case ("7_6" c1 c2 c3)
next thus ?case by (smt (verit) add_leE add_mono_thms_linordered_semiring(1) area.simps(3) nat_le_linear opt_redundancy.simps(44))
case ("6_1" va v) next case ("7_7" c1 c2 c3 c4)
thus ?case sorry thus ?case by (smt (verit) add_leD1 add_le_mono area.simps(3) le_cases3 not_less_eq_eq opt_redundancy.simps(45) plus_1_eq_Suc)
next next case ("7_8" c1 c2)
case ("6_2" va vb v) thus ?case by (smt One_nat_def Suc_le_mono area.simps(3) area.simps(4) le_SucI opt_redundancy.simps(46) opt_redundancy.simps(64) plus_1_eq_Suc)
thus ?case sorry next case ("7_9" c1 c2)
next thus ?case by (smt One_nat_def Suc_le_mono area.simps(3) area.simps(5) le_Suc_eq opt_redundancy.simps(47) opt_redundancy.simps(65) plus_1_eq_Suc)
case ("6_6" vb v va) next case ("7_10" c1 c2 c3)
thus ?case sorry thus ?case by (smt add.right_neutral area.simps(3) area.simps(6) nat_le_linear not_less_eq_eq opt_redundancy.simps(48) opt_redundancy.simps(66) plus_1_eq_Suc)
next next case ("7_12" c1 c2)
case ("6_7" vb vc v va) thus ?case by (smt add_leE add_mono_thms_linordered_semiring(1) area.simps(3) not_less_eq_eq opt_redundancy.simps(50) plus_1_eq_Suc)
thus ?case sorry next case ("7_17" c1 c2)
next thus ?case by (smt (verit) add_leE add_mono_thms_linordered_semiring(1) area.simps(3) not_less_eq_eq opt_redundancy.simps(55) plus_1_eq_Suc)
case ("6_8" v va) next case ("7_22" c1 c2 c3)
thus ?case sorry thus ?case by (smt add.right_neutral area.simps(3) area.simps(6) bot_nat_0.extremum_unique nle_le not_less_eq_eq opt_redundancy.simps(60) plus_1_eq_Suc)
next next case ("7_25" c1 c2)
case ("6_9" v va) thus ?case by (metis (full_types) area.simps(6) opt_redundancy.simps(63) opt_redundancy.simps(66) order_refl zero_le)
thus ?case sorry
next
case ("6_10" vb v va)
thus ?case sorry
next
case ("6_12" v va)
thus ?case sorry
next
case ("6_17" v va)
thus ?case sorry
next
case ("6_22" va vb v)
thus ?case sorry
next
case ("6_25" va v)
thus ?case sorry
next
case ("7_1" va v)
thus ?case sorry
next
case ("7_2" va vb v)
thus ?case sorry
next
case ("7_6" vb v va)
thus ?case sorry
next
case ("7_7" vb vc v va)
thus ?case sorry
next
case ("7_8" v va)
thus ?case sorry
next
case ("7_9" v va)
thus ?case sorry
next
case ("7_10" vb v va)
thus ?case sorry
next
case ("7_12" v va)
thus ?case sorry
next
case ("7_17" v va)
thus ?case sorry
next
case ("7_22" va vb v)
thus ?case sorry
next
case ("7_25" va v)
thus ?case sorry
qed(simp+) qed(simp+)
end end