Some theorys for isabelle, the theorem prover. They're incomplete and don't really work, because I'm not really sure what the fundamental properties for patches are. See ../RevisingPatchTheory :). In many cases the proofs aren't very good either, becuase I don't really grok Isabelle.
Patches.thy
theory Patches = List + Set + Product_Type:
record ('r, 'p) simple_patch =
repos :: "'r set"
patches :: "'p set"
apply_patch :: "'r => 'p => 'r option"
record ('r, 'p) invertible_patch = "('r, 'p) simple_patch" +
inverse :: "'p => 'p"
record ('r, 'p) commutable_patch = "('r, 'p) invertible_patch" +
commute_patch :: "'p => 'p => ('p * 'p) option"
locale simple_patch =
fixes apply_patch
assumes "True"
constdefs
can_apply :: "[('r, 'p, 'sp) simple_patch_scheme, 'r, 'p] => bool"
"can_apply SP r p == (apply_patch SP r p ~= None)"
app :: "[('r, 'p, 'sp) simple_patch_scheme, 'r, 'p] => 'r"
"app SP r p == the (apply_patch SP r p)"
consts
can_apply_n :: "[('r, 'p, 'sp) simple_patch_scheme, 'r, 'p list] => bool"
app_n :: "[('r, 'p, 'sp) simple_patch_scheme, 'r, 'p list] => 'r"
primrec
"can_apply_n SP r [] = True"
"can_apply_n SP r (p#ps) =
(can_apply SP r p & (can_apply_n SP (app SP r p) ps))"
defs
app_n_def: "app_n SP r ps == foldl (app SP) r ps"
locale invertible_patch =
fixes inverse
assumes apply_inverse:
"can_apply SP r p --> app SP (inverse p) (app SP r p) = r"
assumes inverse_inverse:
"inverse (inverse p) == p"
consts
app_add :: "int => int => int option"
invert_add :: "int => int"
defs
app_add_def: "app_add n m == Some (n + m)"
invert_add_def: "invert_add n == 0 - n"
theorem "simple_patch (| apply_patch = app_add_def |)"
proof (intro)
constdefs
can_commute :: "[('r,'p,'cp) commutable_patch_scheme, 'p, 'p] => bool"
"can_commute CP p q == (commute_patch CP p q ~= None)"
comm :: "[('r,'p,'cp) commutable_patch_scheme, 'p, 'p] => ('p * 'p)"
"comm CP p q == the (commute_patch CP p q)"
consts
commute_equiv_class :: "[('r,'p,'cp) commutable_patch_scheme] => 'p list => 'p list set"
commute_equiv_set :: "[('r,'p,'cp) commutable_patch_scheme] => 'p list => 'p => 'p list => 'p list set"
primrec
"commute_equiv_class CP [] = {[]}"
"commute_equiv_class CP (p#ps) =
UNION (commute_equiv_class CP ps) (%x. commute_equiv_set CP [] p x)"
primrec
"commute_equiv_set CP b p [] = { b@[p] }"
"commute_equiv_set CP b p (q#qs) = { b@[p]@(q#qs) } Un
(if can_commute CP p q
then split (%q' p'. commute_equiv_set CP (b@[q']) p' qs)
(comm CP p q)
else {})"
constdefs
merge_patch :: "[('r,'p,'cp) commutable_patch_scheme, 'p] => 'p => 'p * 'p"
"merge_patch SP p q == prod_fun (inverse SP) id (comm SP (inverse SP q) p)"
locale commutable_patch =
fixes commute
assumes app_comm:
"can_commute SP p q
--> can_apply_n SP r [p,q]
--> (q',p') = commute p q --> can_apply_n SP r [q',p']
& app_n SP r [p,q] = app_n SP r [q',p']"
assumes comm_comm:
"can_commute SP p q --> (p,q) = split commute (commute p q)"
assumes comm_past_inverse:
"can_commute SP p q
--> (q',p') = comm SP p q
--> (commute_patch SP p' (inverse SP q) = Some (inverse SP q',p))"
theorem (in commutable_patch) equiv_set_id: "a#x : commute_equiv_set SP [] a x"
by (induct x, simp, simp)
theorem (in commutable_patch) equiv_class_1: "ps : commute_equiv_class SP ps"
proof (induct ps)
case Nil
show ?case by simp
case (Cons h t)
let ?a = "t:commute_equiv_class SP t"
let ?b = "h#t : commute_equiv_set SP [] h t"
have a: "?a" .
have b: "?b" by (simp only: equiv_set_id)
from a and b have "?a & ?b" by simp
thus ?case by auto
qed
end
FilePatches.thy
theory FilePatches = Main + IntArith + Patches:
datatype 'a filepatch = AddFile | RmFile
| Hunk nat "'a list" "'a list"
datatype 'a file = File "'a list"
| NoFile
consts
mid :: "nat => nat => 'a list => 'a list * 'a list * 'a list"
append3 :: "'a list * 'a list * 'a list => 'a list"
replacemid :: "'a => 'a * 'a * 'a => 'a * 'a * 'a"
defs
mid_def [simp] :
"mid s e l == ((take s l), (take e (drop s l)), (drop e (drop s l)))"
append3_def [simp] :
"append3 x == (fst x)@(fst (snd x))@(snd (snd x))"
replacemid_def [simp] : "replacemid y2 xyz == (fst xyz, y2, snd (snd xyz))"
lemma app3mid [simp]: "append3 (mid s e l) = l"
by (simp only: mid_def, simp only: append3_def, simp only: snd_conv,
simp only: fst_conv, simp only: append_take_drop_id)
lemma midapp3 [simp]: "(length (fst x) = s & length (fst (snd x)) = m) --> mid s m (append3 x) = x"
by (simp)
consts applypatch :: "'a filepatch => 'a file => ('a file) option"
primrec
"applypatch p NoFile =
(case p of AddFile => Some(File([]))
| RmFile => None
| Hunk n r a => None)"
"applypatch p (File f) =
(case p of AddFile => None
| RmFile => (if f = [] then Some(NoFile) else None)
| Hunk n r a =>
if (length f) < n + (length r) then None
else
(%m.
if (fst (snd m)) = r then Some(File( append3(replacemid a m) ))
else None
) (mid n (length r) f)
)"
constdefs
my_app_filepatch :: "'a file => 'a filepatch => 'a file option"
"my_app_filepatch f p == applypatch p f"
lemma "simple_patch A --> simple_patch A & True"
by (simp)
consts
applies :: "'a filepatch => 'a file => bool"
app :: "'a filepatch => 'a file => 'a file"
defs
applies_def [simp] : "applies p f == (applypatch p f) ~= None"
app_def [simp] : "app p f == the (applypatch p f)"
lemma hlhunk:
"applies (Hunk n r a) (File fl) -->
(fst (snd (mid n (length r) fl))) = r"
proof (simp only: applies_def, simp only: applypatch.simps, simp)
qed
lemma apphunkwhen: "take (length r) (drop n fl) = r --> n + (length r) <= length fl --> applies (Hunk n r a) (File fl)"
by (simp)
lemma apphunksizeprop: "applies (Hunk n r a) (File fl) --> n + (length r) <= length fl"
by simp
lemma apphunksubprop: "applies (Hunk n r a) (File fl) --> take (length r) (drop n fl) = r"
by simp
consts hunked_file :: "nat => 'a list => 'a list => 'a list => 'a list"
defs hunked_file_def [simp] : "hunked_file n r a fl == append3 (replacemid a (mid n (length r) fl))"
lemma apphunk: "applies (Hunk n r a) (File fl) --> app (Hunk n r a) (File fl) = (File (hunked_file n r a fl))"
by (simp)
consts invert :: "'a filepatch => 'a filepatch"
primrec
"invert AddFile = RmFile"
"invert RmFile = AddFile"
"invert (Hunk n r a) = Hunk n a r"
theorem "invert (invert p) = p"
by (induct p, auto)
lemma shorthunkedfile: "length f <= n --> hunked_file n x y f = f@y"
by (simp only: hunked_file_def, simp only: mid_def, simp only: append3_def,
simp only: replacemid_def, simp only: snd_conv, simp only: fst_conv, simp)
lemma longtake: "n <= length f --> take n (take n f @ x) = take n f"
by simp
lemma hunkedfilesimp [simp]: "n <= length f --> hunked_file n y z (hunked_file n x y f) = hunked_file n x z f"
by (simp only: hunked_file_def, simp only: mid_def, simp only: append3_def, simp only: replacemid_def, simp only: snd_conv, simp only: fst_conv, simp add: min_def)
theorem "applies p f --> app (invert p) (app p f) = f"
proof (induct p)
case RmFile
show ?case by (induct f, auto)
case AddFile
show ?case by (induct f, auto)
case (Hunk n r a)
show ?case
proof (induct f)
case NoFile show ?case by simp
case (File fl)show ?case
proof (rule impI)
let ?fl' = "hunked_file n r a fl"
let ?fl'' = "hunked_file n a r ?fl'"
let ?lhsi = "app (Hunk n r a) (File fl)"
let ?lhs = "app (invert (Hunk n r a)) (?lhsi)"
assume "applies (Hunk n r a) (File fl)"
with apphunksizeprop have "n + length r <= length fl" ..
then have "n <= length fl" by simp
with hunkedfilesimp have "?fl'' = hunked_file n r r fl" ..
then have FL: "?fl'' = fl"
proof -
assume "?fl'' = hunked_file n r r fl"
have FACT: "?fl'' = hunked_file n r r fl" .
from apphunksubprop have "take (length r) (drop n fl) = r" ..
then have "hunked_file n r r fl = fl"
proof (simp only: hunked_file_def, simp only: mid_def,
simp only: replacemid_def, simp only: append3_def,
simp only: snd_conv, simp only: fst_conv)
let ?rhs = "take n fl @ drop n fl"
let ?dnfl = "take (length r) (drop n fl) @ drop (length r) (drop n fl)"
let ?lhs = "take n fl @ r @ drop (length r) (drop n fl)"
assume "take (length r) (drop n fl) = r"
then have LHS: "?lhs = take n fl @ (?dnfl)" by simp
have RHS: "take n fl @ ?dnfl = fl" by (simp only: append_take_drop_id)
with LHS show "?lhs = fl" by simp
qed
with FACT show "?fl'' = fl" by simp
qed
from apphunk have LHSI: "?lhsi = File ?fl'" ..
have "applies (Hunk n r a) (File fl) --> n <= length fl" by (simp)
then have "n <= length fl" ..
then have "applies (invert (Hunk n r a)) (File ?fl')"
by (simp add: min_def)
then have "app (invert (Hunk n r a)) (File ?fl') = (File ?fl'')"
by (simp only: invert.simps, simp only: apphunk)
then have LHS: "?lhs = (File ?fl'')" by (simp only: LHSI)
then show "?lhs = (File fl)" by (simp only: FL)
qed
qed
qed
consts
commute :: "'a filepatch => 'a filepatch => (('a filepatch) * ('a filepatch)) option"
commuteHunks :: "nat => 'a list => 'a list => nat => 'a list => 'a list => (('a filepatch) * ('a filepatch)) option"
can_commute :: "'a filepatch => 'a filepatch => bool"
com :: "'a filepatch => 'a filepatch => ('a filepatch) * ('a filepatch)"
primrec
"commute AddFile p = None"
"commute RmFile p = None"
"commute (Hunk n r a) p =
(case p of AddFile => None
| RmFile => None
| Hunk n2 r2 a2 => commuteHunks n r a n2 r2 a2)"
defs
commuteHunks_def [simp] : "commuteHunks n1 r1 a1 n2 r2 a2 ==
(if (n1 + length a1) < n2
then Some ((Hunk (n2 - length a1 + length r1) r2 a2), (Hunk n1 r1 a1))
else if n2 + length r2 < n1
then Some ((Hunk n2 r2 a2), (Hunk (n1 - length r2 + length a2) r1 a1))
else None)"
can_commute_def [simp] : "can_commute p q == commute p q ~= None"
com_def [simp] : "com p q == the (commute p q)"
consts
app2 :: "'a filepatch => 'a filepatch => 'a file => 'a file"
defs
app2_def [simp] : "app2 p q f == app q (app p f)"
theorem "can_commute p q --> (p,q) = split com (com p q)"
proof (induct p)
case AddFile show ?case by simp
case RmFile show ?case by simp
case (Hunk n1 r1 a1) show ?case
proof (induct q)
case AddFile show ?case by simp
case RmFile show ?case by simp
case (Hunk n2 r2 a2)
let ?order12 = "n1 + length a1 < n2"
let ?order21 = "n2 + length r2 < n1"
let ?overlap = "~ (?order12 | ?order21)"
have "(~ ?order12) | (~ ?order21)" by arith
then show ?case
proof (cases "?overlap")
assume "~ ?overlap"
show ?case
proof (cases "?order12")
assume "?order12"
have "?order12" .
then have "~ ?order21" by arith
then show ?case by (simp, arith)
next
assume "~ ?order12"
have "~ ~ (?order12 | ?order21)" .
then have O1: "?order12 | ?order21" by simp
have "~ ?order12" .
with O1 have "?order21" by simp
then show ?case by (simp, arith)
qed
next
assume "?overlap"
let ?mid1 = "(~ n1 < n2) & (~ n2 + length r2 < n1)"
let ?mid2 = "(~ n2 < n1) & (~ n1 + length a1 < n2)"
have "?overlap" .
then have M12: "?mid1 | ?mid2" by arith
then show ?case
proof (cases ?mid1)
assume "~ ?mid1"
with M12 have "?mid2" by simp
then show ?case by (simp, arith)
next
assume "?mid1"
then show ?case by (simp, arith)
qed
qed
qed
qed
lemma comhunk_12: "n1 + length a1 < n2 --> com (Hunk n1 r1 a1) (Hunk n2 r2 a2) = (Hunk (n2 - length a1 + length r1) r2 a2, Hunk n1 r1 a1)"
by (simp)
lemma comhunk_21: "n2 + length r2 < n1 --> com (Hunk n1 r1 a1) (Hunk n2 r2 a2) = (Hunk n2 r2 a2, Hunk (n1 - length r2 + length a2) r1 a1)"
by (simp)
consts
mid_n :: "nat list => 'a list => 'a list list"
append_n :: "'a list list => 'a list"
primrec
"mid_n [] x = [x]"
"mid_n (h#t) x = (take h x)#(mid_n t (drop h x))"
primrec
"append_n [] = []"
"append_n (h#t) = h @ (append_n t)"
lemma hunked_file_append_l: "n + length r <= length x --> hunked_file n r a (x@y) = (hunked_file n r a x)@y" by simp
lemma hunked_file_append_r: "length x <= n --> hunked_file n r a (x@y) = x@(hunked_file (n - length x) r a y)" by simp
lemma rearrange_le_minus:
assumes a1: "(a::int) <= b - c"
shows "a + c <= b"
proof -
from a1 have "a + c <= (b - c) + c"
by (arith)
also have "... = b"
by (arith)
finally show "a + c <= b"
by (this)
qed
theorem "invertible_patch (| apply_patch = %p f. applypatch f p, inverse = invert |)"
proof (rule simple_patch_def)
lemma commute_hunked_file: "n1 + length r1 < length fl --> n1 + length a1 < n2 --> n2 + length r2 + length r1 <= length fl + length a1 --> hunked_file n1 r1 a1 (hunked_file n2 r2 a2 fl) = hunked_file (n2 + length r1 - length a1) r2 a2 (hunked_file n1 r1 a1 fl)"
proof (rule impI, rule impI, rule impI)
assume "n1 + length r1 <= length fl"
have ass_n1_fl: "n1 + length r1 <= length fl" .
assume "n1 + length a1 < n2"
have ass_n1_n2: "n1 + length a1 < n2" .
assume "n2 + length r2 + length r1 <= length fl + length a1"
have ass_n2_fl: "n2 + length r2 + length r1 <= length fl + length a1" .
let ?n2' = "n2 + length r1 - length a1"
let ?p1 = "hunked_file n1 r1 a1"
let ?p2a = "hunked_file n2 r2 a2"
let ?p2b = "hunked_file ?n2' r2 a2"
let ?lhs = "?p1 (?p2a fl)"
let ?rhs = "?p2b (?p1 fl)"
let ?d2 = "?n2' - n1"
let ?first = "take ?n2' fl"
let ?second = "drop ?n2' fl"
let ?beg = "take n1 ?first"
let ?x1 = "take (length r1) (drop n1 ?first)"
let ?mid = "drop (length r1) (drop n1 ?first)"
let ?x2 = "take (length r2) ?second"
let ?end = "drop (length r2) ?second"
let ?mhs = "?beg @ a1 @ ?mid @ a2 @ ?end"
have "(?beg @ (?x1 @ ?mid)) @ (?x2 @ ?end) = fl"
by (simp only: append_take_drop_id)
then have splitfl: "?beg @ ?x1 @ ?mid @ ?x2 @ ?end = fl" by simp
from ass_n2_fl have "n2 + length r2 + length r1 <= length fl + length a1" .
then have "n2 + length r1 <= length fl + length a1" by arith
then have a1: "?n2' <= length fl" by arith
from ass_n2_fl have "length ?first = ?n2'" by arith
from ass_n1_fl have "length ?beg + length ?x1 <= n1 + length r1" by simp
with hunked_file_append_l have "?p1 fl = (?p1 (?beg@?x1))@(?mid@?x2@?end)"
by (simp)
have "?beg @ ?r1' @ ?mid @ ?r2' @ ?end = fl"
assume "n1 + length r1 < length fl"
assume "n2 + length r2 <= length fl - length r1 + length a1"
theorem "applies p f --> applies q (app p f) --> can_commute p q --> app2 p q f = split app2 (com p q) f"
proof (induct p)
case AddFile show ?case by (induct q, auto)
case RmFile show ?case by (induct q, auto)
case (Hunk n1 r1 a1) show ?case
proof (induct q)
case AddFile show ?case by (simp)
case RmFile show ?case by (simp)
case (Hunk n2 r2 a2) show ?case
proof (induct f)
case NoFile show ?case by (simp)
case (File fl)
let ?f' = "app (Hunk n1 r1 a1) (File fl)"
let ?f'' = "app (Hunk n2 r2 a2) ?f'"
show ?case
proof (simp only: can_commute_def, rule impI, simp only: apphunk, rule impI, rule impI)
let ?fl' = "hunked_file n1 r1 a1 fl"
let ?fl'' = "hunked_file n2 r2 a2 ?fl'"
let ?lhs = "app2 (Hunk n1 r1 a1) (Hunk n2 r2 a2) (File fl)"
assume "applies (Hunk n1 r1 a1) (File fl)"
then have F1: "?f' = File ?fl'" by (simp only: apphunk)
assume "applies (Hunk n2 r2 a2) (File ?fl')"
with F1 have "?f'' = File ?fl''" by (simp only: apphunk)
then have LHS: "?lhs = File ?fl''" by (simp only: app2_def)
let ?rhs = "split app2 (com (Hunk n1 r1 a1) (Hunk n2 r2 a2)) (File fl)"
let ?first1 = "n1 + (length a1) < n2"
let ?first2 = "n2 + (length r2) < n1"
let ?com = "com (Hunk n1 r1 a1) (Hunk n2 r2 a2)"
assume "commute (Hunk n1 r1 a1) (Hunk n2 r2 a2) ~= None"
then have "?first1 | ?first2"
by (cases "~ ?first1", cases "~ ?first2", auto)
then have RHS: "?rhs = File ?fl''"
proof (cases "~ ?first1")
assume "~ ?first1"
assume "?first1 | ?first2"
let ?p2' = "Hunk n2 r2 a2"
let ?p1' = "Hunk (n1 - length r2 + length a2) r1 a1"
let ?flx' = "hunked_file n2 r2 a2 fl"
let ?flx'' = "hunked_file (n1 - length r2 + length a2) r1 a1 ?flx'"
have "(~ ?first1) & (?first1 | ?first2)" ..
then have F2: "?first2" by (cases "?first2", auto)
with comhunk_21 have "?com = (?p2', ?p1')" ..
then have "?rhs = app ?p1' (app ?p2' (File fl))"
by (simp)
have "applies (Hunk n2 r2 a2) (File (hunked_file n1 r1 a1 fl))" .
with apphunksubprop have "take (length r2) (drop n2 (hunked_file n1 r1 a1 fl)) = r2" ..
then have "drop n2 (take (length r2 + n2) (hunked_file n1 r1 a1 fl)) = r2" by (simp only: take_drop)
then have "drop n2 (take (length r2 + n2) fl) = r2"
proof -
let ?lh = "take (length r2 + n2) (hunked_file n1 r1 a1 fl)"
let ?rh = "take (length r2 + n2) fl"
assume "drop n2 ?lh = r2"
have LH: "drop n2 ?lh = r2" .
have "applies (Hunk n1 r1 a1) (File fl)" .
with apphunksizeprop have "n1 + length r1 <= length fl" ..
then have "n1 <= length fl" by arith
with F2 have "?rh = ?lh" by (simp add: min_def)
then have "drop n2 (?rh) = drop n2 (?lh)" by (simp)
with LH show "drop n2 ?rh = r2" by simp
qed
then have APPP21: "take (length r2) (drop n2 fl) = r2"
by (simp only: take_drop)
have "applies (Hunk n1 r1 a1) (File fl)" .
with apphunksizeprop have "n1 + length r1 <= length fl" ..
with F2 have "n2 + length r2 + length r1 <= length fl" by arith
then have "n2 + length r2 <= length fl" by arith
with APPP21 and apphunkwhen have APPP2: "applies ?p2' (File fl)"
by simp
with apphunk have FLX1: "app ?p2' (File fl) = (File ?flx')" ..
let ?flmid = "drop (n2 + length r2) (take n1 fl)"
let ?flend = "drop (n1 + length r1) fl"
let ?flfin = "take n2 fl @ a2 @ ?flmid @ a1 @ ?flend"
from F2 have "?flx'' = ?flfin"
proof (simp only: hunked_file_def, simp only: mid_def, simp only: replacemid_def, simp only: append3_def, simp only: snd_conv, simp only: fst_conv, simp, simp only: min_def)
thus "?rhs = File ?fl''"
by simp
have "applies ?p2' (File fl)"
have "app ?p1' (app ?p2' (File fl)) = File ?fl''"
proof (simp only: app_def)
have "applies ?p1' (File fl)"
proof (simp)
have "app ?p2' (app ?p1' (File fl)) = File ?fl''"
by (simp only: apphunk)
next
let ?p2' = "Hunk (n2 - length a1 + length r1) r2 a2"
let ?p1' = "Hunk n1 r1 a1"
assume "?first1"
with comhunk_12 have "?com = (?p2', ?p1')" ..
then have "split app2 ?com (File fl) = app ?p2' (app ?p1' (File fl))"
by simp
qed
have "?papp" .
with apphunk have "?f' =unked
sorry