feat(model): prove optimiser idempotence and scope weakening

1 files changed, +16 −0

@@ -94,4 +94,20 @@ lemma fold_cond_nodes: "nodes (fold_cond c a b) \<le> Suc (nodes c + nodes a + n
94	94	theorem optimise_size: "nodes (optimise e) \<le> nodes e"
95	95	by (induction e) (auto intro: order_trans[OF fold_binary_nodes] order_trans[OF fold_cond_nodes])
96	96
	97	+lemma fold_binary_idempotent:
	98	+ "optimise a = a \<Longrightarrow> optimise b = b \<Longrightarrow>
	99	+ optimise (fold_binary op a b) = fold_binary op a b"
	100	+ by (cases a; cases b) auto
	101	+
	102	+lemma fold_cond_idempotent:
	103	+ "optimise c = c \<Longrightarrow> optimise a = a \<Longrightarrow> optimise b = b \<Longrightarrow>
	104	+ optimise (fold_cond c a b) = fold_cond c a b"
	105	+ by (cases c) auto
	106	+
	107	+theorem optimise_idempotent: "optimise (optimise e) = optimise e"
	108	+ by (induction e) (auto intro: fold_binary_idempotent fold_cond_idempotent)
	109	+
	110	+theorem scoped_weaken: "scoped n e \<Longrightarrow> n \<le> m \<Longrightarrow> scoped m e"
	111	+ by (induction e arbitrary: n m) auto
	112	+
97	113	end

~james/remy