adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: introduce fun_upd2 

fun_upd for functions with two arguments.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-06-16 16:33:58 +10:00 committed by Gerwin Klein
parent 30ba342a20
commit 639ebf7eed
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
lib/Lib.thy
View File

@ -199,6 +199,19 @@ abbreviation(input)
lemmas option_map_def = map_option_case
(* Function update for functions with two arguments. This is just nested normal function update,
but writing it out in goals leads to large annoying terms with if-s that get split etc, so we
introduce a constant for it. Syntax precedence is same as fun_upd, but we are only allowing
a single update, no sequences. *)
definition fun_upd2 ::
"('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c)" ("_ '(_, _ := _')" [1000, 0, 0] 900) where
"f (x, y := v) \<equiv> \<lambda>x'. if x' = x then (f x) (y := v) else f x'"
(* precedence same as MapUpd, only single updates as above, no general maplets. *)
abbreviation fun_upd2_Some :: "('a \<Rightarrow> 'b \<Rightarrow> 'c option) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c option)"
("_ '(_, _ \<mapsto> _')" [900, 0, 0] 900) where
"f (x, y \<mapsto> v) \<equiv> f (x, y := Some v)"
lemma False_implies_equals [simp]:
"((False \<Longrightarrow> P) \<Longrightarrow> PROP Q) \<equiv> PROP Q"
apply (rule equal_intr_rule)