Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
117 commits
Select commit Hold shift + click to select a range
bbd618c
Merge pull request #1 from wimmers/master
BilelGho Nov 30, 2020
7f2d262
Merge branch 'wimmers:master' into master
BilelGho Jul 8, 2021
b155017
old ROOTS
BilelGho Jul 8, 2021
6f7f868
Merge branch 'master' of github.com:BilelGho/poly-reductions
BilelGho Jul 8, 2021
bd0e75a
non-harmful changes to ease the refinement to HOL-nat
BilelGho Aug 13, 2021
b6a414e
refinement of the reduction to HOL_nat
BilelGho Aug 13, 2021
285336a
refinement of the reduction to HOL_nat
BilelGho Aug 13, 2021
64ad165
refinement of the reduction to HOL_nat
BilelGho Aug 13, 2021
464c70e
Merge branch 'wimmers:master' into master
BilelGho Aug 13, 2021
4145b68
Merge pull request #2 from wimmers/cook-levin-hol-statement
BilelGho Aug 14, 2021
7055c43
slightly cleaned up proofs
notiho Aug 17, 2021
365d121
push everything to work on remote
BilelGho Aug 17, 2021
5a844e0
ROOT file
BilelGho Aug 17, 2021
3f31fc8
forgot to add file
BilelGho Aug 18, 2021
fe19cd2
reduction no longer existentially quantified + refined called functio…
Aug 18, 2021
b4c26f5
forgot to add file
Aug 18, 2021
9391b76
Merge branch 'master' of github.com:BilelGho/poly-reductions
Aug 18, 2021
297eef8
implemented and verified multiplication in IMP-
notiho Aug 19, 2021
48b1bdc
refinement to HOL_nat + main_lemma_hol_nat
Aug 19, 2021
bcc6668
fixed ;)
Aug 19, 2021
b88fd58
Merge branch 'wimmers-master'
Aug 19, 2021
68133e2
transformed higher order functions into independent instances
Aug 19, 2021
4492441
started refinment to HOL-tail
Aug 22, 2021
93e3b5e
refinement to tail-rec, started general pattern for IMP- to IMP--
Aug 28, 2021
4219a29
IMP- to IMP-- tail recursive
BilelGho Aug 28, 2021
7981690
prove correctness for nat, imp- to imp--, first try
Aug 28, 2021
a54496d
IMP- to IMP -- refined to tail recursive
Aug 29, 2021
a492fb7
all the functions that need a general pattern for tail recursion
BilelGho Aug 31, 2021
1f86712
more refinement to tail-rec , max constant remaining
Aug 31, 2021
c840922
max constant refined to tail-rec
BilelGho Aug 31, 2021
f1f97ec
finished refinement to tail-rec
Aug 31, 2021
de1edea
updated multiplication
notiho Sep 1, 2021
ea36ca3
Merge branch 'wimmers:master' into multiplication
notiho Sep 1, 2021
97391b1
Merge pull request #1 from BilelGho/master
notiho Sep 1, 2021
6d76b4e
verified implementation of encoding and decoding pairs in IMP-
notiho Sep 2, 2021
0f147ab
implemented and verified a few functions from IMP- Max Constant
notiho Sep 2, 2021
8d52aa3
termination proof: trying with size function
Sep 3, 2021
0ce1728
temrination order for max_constant, and all_variables (stack versions…
BilelGho Sep 3, 2021
e6a9206
temrination order for stack simulation implementations on HOL level, …
BilelGho Sep 4, 2021
a8cd411
implemented and verified add_res
notiho Sep 6, 2021
84fc9c2
show termination for nat, only for valid input and replace correctnes…
BilelGho Sep 7, 2021
1cd1de1
rewrite prod_encode, fst_nat , snd_nat in polynomial time code (whil…
BilelGho Sep 7, 2021
7df8676
started implementing max_constant
notiho Sep 9, 2021
0d7a9e5
Merge pull request #2 from BilelGho/master
notiho Sep 13, 2021
07c5b9f
finished implementing and verifiying max_constant
notiho Sep 14, 2021
83291d3
implemented another function
notiho Sep 17, 2021
61ea718
Created empty theory IMP_Minus_Common_Funs_Nat
Sep 20, 2021
a00f8e7
imported IMP_Minus_Nat_Bijection
Sep 22, 2021
b742b35
stopped working on append
Sep 22, 2021
bdccbd5
defined elemof_IMP_Minus_iteration
Sep 22, 2021
0520d6e
defined elemof_IMP_Minus_iteration_time
Sep 22, 2021
524f539
stated and gave very messy proof to elemof_IMP_Minus_iteration_correct
Sep 22, 2021
b18f52f
Defined elemof_IMP_Minus_loop
Sep 25, 2021
6145c7a
Defined elemof_IMP_Minus_loop_time
Sep 25, 2021
396c387
Stated and gave horrible proof to elemof_IMP_Minus_loop_correct
Sep 25, 2021
15e33dc
removed unnecessary simp add
lakiryt Sep 26, 2021
d31e19f
defined elemof_IMP_Minus
lakiryt Sep 26, 2021
793c26c
defined elemof_IMP_Minus_time
lakiryt Sep 26, 2021
dc87925
Stated and gave awfully verbose proof elemof_IMP_Minus_correct
lakiryt Sep 26, 2021
3c096e6
marginally shortened elemof_IMP_Minus_correct proof
lakiryt Sep 26, 2021
52a92fd
marginally shortened elemof_IMP_Minus_loop_correct
lakiryt Sep 26, 2021
5df081e
shortened True-case in elemof_IMP_Minus_iteration_correct
lakiryt Sep 26, 2021
d5204ab
shortened proof for elemof_IMP_Minus_iteration_correct
lakiryt Sep 29, 2021
fe02275
simplified time definition
lakiryt Sep 29, 2021
b57e4cb
shortened elemof_IMP_Minus_correct proof
lakiryt Oct 1, 2021
ec48586
removed lemmata from elemof_IMP_Minus_loop_correct
lakiryt Oct 1, 2021
bcbfcd7
stylistics
lakiryt Oct 1, 2021
882b0d8
Defined append_tail_IMP_Minus
lakiryt Oct 1, 2021
4e09851
defined append_tail_IMP_Minus_time
lakiryt Oct 1, 2021
f292a06
named revapp lemma
lakiryt Oct 1, 2021
16fd265
stated and (verbosely) proved append_tail_IMP_Minus_correct
lakiryt Oct 1, 2021
6032f98
shortened proof of append_tail_IMP_Minus_correct
lakiryt Oct 2, 2021
5e6aeb3
removed unused lemma
lakiryt Oct 2, 2021
875027c
simplified append_tail_IMP_Minus_time
lakiryt Oct 2, 2021
973bad9
stopped working on remdups_tail due to run out of registers
lakiryt Oct 5, 2021
2588bad
defined list_from_acc_IMP_Minus_iteration
lakiryt Oct 5, 2021
aee45ae
defined list_from_acc_IMP_Minus_iteration_time
lakiryt Oct 5, 2021
7abe883
stated and proved list_from_acc_IMP_Minus_iteration_correct
lakiryt Oct 5, 2021
0c8a812
defined list_from_acc_IMP_Minus_loop_time
lakiryt Oct 5, 2021
d901930
stated and proved list_from_acc_loop_correct
lakiryt Oct 5, 2021
91bcd31
shortened proof for list_from_acc_correct
lakiryt Oct 5, 2021
9de7f54
defined concat_acc_IMP_Minus_iteration with additional registers
lakiryt Oct 8, 2021
69d3b78
defined concat_acc_IMP_Minus_iteration_time
lakiryt Oct 8, 2021
fbd2a2d
stated and proved concat_acc_IMP_Minus_iteration_correct
lakiryt Oct 8, 2021
0703c84
defined concat_acc_IMP_Minus_loop_time
lakiryt Oct 8, 2021
bfa2c4d
stated and proved concat_acc_IMP_Minus_correct
lakiryt Oct 8, 2021
9a3eef6
added canonical state transformers
notiho Oct 8, 2021
7f68029
Merge remote-tracking branch 'upstream/multiplication' into utilfun
lakiryt Oct 9, 2021
bb18dff
started changing IMP- implementations to state_transformer
notiho Oct 11, 2021
aa7dd65
Merge remote-tracking branch 'upstream/multiplication' into utilfun
lakiryt Oct 12, 2021
bf620ed
left proof with "sorry"s
lakiryt Oct 19, 2021
3d1f66a
removed unnecessary parts
lakiryt Oct 19, 2021
93f57b8
proved c1
lakiryt Oct 24, 2021
70912f1
proved c2
lakiryt Oct 24, 2021
779a5a7
marginally shortened c2 proof
lakiryt Oct 29, 2021
e416062
corrected overridden local variable name and corresponding proof steps
lakiryt Oct 29, 2021
1744648
re-added formerly working proof before sorry
lakiryt Oct 29, 2021
2833d47
factored out duplicate auxiliary proof
lakiryt Oct 29, 2021
a45cd88
improved readability of the cons_list_IMP_Minus_state_transformer and…
lakiryt Oct 29, 2021
5a92494
further shortened proof, gave meaningful name to aux->cons_list_state…
lakiryt Oct 29, 2021
660fdf8
corrected bracketing, reviving Nil-case proof (+marginally shortened)
lakiryt Oct 29, 2021
5d33bdb
removed commented out old/experimental state_transformers for cons_list
lakiryt Oct 29, 2021
53955ba
Merge pull request #4 from lakiryt/utilfun
BilelGho Nov 26, 2021
e741b37
working on first function in binary arithmetic theory
BilelGho Dec 8, 2021
dab1770
fixing state transformers
BilelGho Dec 9, 2021
9afe3a4
test
BilelGho Dec 9, 2021
6e55461
Added experimental proofs to deal with IH, if and while
mabdula Dec 15, 2021
5c8654c
New approach instaed of state transformers
mabdula Dec 21, 2021
ef54812
Finished prod_encode
mabdula Dec 22, 2021
5a4e162
Mul is standard now
mabdula Dec 22, 2021
36e4aca
prod decode
mabdula Dec 23, 2021
8b97418
hd and tl
mabdula Dec 23, 2021
fbd00b3
IMP- primitives in a new file
mabdula Dec 24, 2021
59dc8a3
Call by prefixes in IMP-
mabdula Dec 24, 2021
1490a3a
Moved IMP- primitives to new file; Refined some more primitives; New …
mabdula Dec 24, 2021
1485c7b
Added some comment
mabdula Dec 24, 2021
3a7e65b
N-th bit + slightly better infrastructure
mabdula Dec 26, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions #Untitled-2#
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
xckdxcddsc*s
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
!a;4288;4288
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@

section \<open>IMP-- Subprograms\<close>

theory IMP_Minus_Minus_Subprograms imports "../IMP_Minus_Minus_Small_StepT"
theory IMP_Minus_Minus_Subprograms
imports IMP_Minus_Minus_Small_StepT
begin

text \<open>We give functions that enumerate all subprograms of an IMP-- program, that is, all
Expand Down

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
section "IMP-- to SAS++ Correctness"

theory IMP_Minus_Minus_To_SAS_Plus_Plus_Correctness
imports IMP_Minus_Minus_To_SAS_Plus_Plus_Reduction "../SAS_Plus_Plus"
imports IMP_Minus_Minus_To_SAS_Plus_Plus_Reduction SAS_Plus_Plus
begin

text \<open> We show correctness for the IMP-- to SAS++ reduction. \<close>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,11 @@ type_synonym operator = "(variable, domain_element) sas_plus_operator"
type_synonym problem = "(variable, domain_element) sas_plus_problem"

definition pc_to_com :: "(variable \<times> domain_element) list \<Rightarrow> com" where
"pc_to_com l = (case l ! 0 of (_, PCV x) \<Rightarrow> x)"
"pc_to_com l = (if l = [] then SKIP else (case l ! 0 of (_, PCV x) \<Rightarrow> x | t \<Rightarrow> SKIP))"

lemma pc_to_com_def2 :"l \<noteq> [] \<Longrightarrow> pc_to_com l = (case l ! 0 of (_, PCV x) \<Rightarrow> x | t \<Rightarrow> SKIP)"
apply (auto simp add: pc_to_com_def)
done

fun com_to_operators :: "com \<Rightarrow> operator list" where
"com_to_operators (SKIP) = []" |
Expand Down Expand Up @@ -144,16 +148,18 @@ lemma map_of_precondition_of_op_PC[simp]: "op \<in> set (com_to_operators c)

lemma pc_to_com_precondition_of_op_PC [simp]: "op \<in> set (com_to_operators c)
\<Longrightarrow> pc_to_com (precondition_of op) = c"
using PC_of_precondition
by (metis PC_in_effect_precondition domain_element.simps nth_mem old.prod.case pc_to_com_def
precondition_nonempty)
using PC_of_precondition pc_to_com_def2
by (metis PC_in_effect_precondition domain_element.simps(6)
length_greater_0_conv nth_mem old.prod.case precondition_nonempty)


lemma pc_to_com_effect[simp]: "op \<in> set (com_to_operators c)
\<Longrightarrow> (PC, y) \<in> set (effect_of op) \<longleftrightarrow> y = PCV (pc_to_com (effect_of op))"
using com_to_operators_variables_distinct PC_in_effect_precondition
by (auto simp: pc_to_com_def)
(metis domain_element.simps effect_nonempty eq_key_imp_eq_value nth_mem old.prod.case)+

pc_to_com_def2
by (metis domain_element.simps(6) effect_nonempty eq_key_imp_eq_value length_greater_0_conv
nth_mem old.prod.case)

lemma PC_of_effect[simp]: "op \<in> set (com_to_operators c)
\<Longrightarrow> map_of (effect_of op) PC = Some (PCV (pc_to_com (effect_of op)))"
using com_to_operators_variables_distinct PC_in_effect_precondition
Expand Down
Loading