Theory Automatic_Refinement.Autoref_Bindings_HOL
section ‹Standard HOL Bindings›
theory Autoref_Bindings_HOL
imports "Tool/Autoref_Tool"
begin
subsection "Structural Expansion"
text ‹
In some situations, autoref imitates the operations on typeclasses and
the typeclass hierarchy. This may result in structural mismatches, e.g.,
a hashcode side-condition may look like:
@{text [display] "is_hashcode (prod_eq (=) (=)) hashcode"}
This cannot be discharged by the rule
@{text [display] "is_hashcode (=) hashcode"}
In order to handle such cases, we introduce a set of simplification lemmas
that expand the structure of an operator as far as possible.
These lemmas are integrated into a tagged solver, that can prove equality
between operators modulo structural expansion.
›
definition [simp]: "STRUCT_EQ_tag x y ≡ x = y"
lemma STRUCT_EQ_tagI: "x=y ⟹ STRUCT_EQ_tag x y" by simp
ML ‹
structure Autoref_Struct_Expand = struct
structure autoref_struct_expand = Named_Thms (
val name = @{binding autoref_struct_expand}
val description = "Autoref: Structural expansion lemmas"
)
fun expand_tac ctxt = let
val ss = put_simpset HOL_basic_ss ctxt addsimps autoref_struct_expand.get ctxt
in
SOLVED' (asm_simp_tac ss)
end
val setup = autoref_struct_expand.setup
val decl_setup = fn phi =>
Tagged_Solver.declare_solver @{thms STRUCT_EQ_tagI} @{binding STRUCT_EQ}
"Autoref: Equality modulo structural expansion"
(expand_tac) phi
end
›
setup Autoref_Struct_Expand.setup
declaration Autoref_Struct_Expand.decl_setup
text ‹Sometimes, also relators must be expanded. Usually to check them to be the identity relator›
definition [simp]: "REL_IS_ID R ≡ R=Id"
definition [simp]: "REL_FORCE_ID R ≡ R=Id"
lemma REL_IS_ID_trigger: "R=Id ⟹ REL_IS_ID R" by simp
lemma REL_FORCE_ID_trigger: "R=Id ⟹ REL_FORCE_ID R" by simp
declaration ‹Tagged_Solver.add_triggers
"Relators.relator_props_solver" @{thms REL_IS_ID_trigger}›
declaration ‹Tagged_Solver.add_triggers
"Relators.force_relator_props_solver" @{thms REL_FORCE_ID_trigger}›
abbreviation "PREFER_id R ≡ PREFER REL_IS_ID R"
lemmas [autoref_rel_intf] = REL_INTFI[of fun_rel i_fun]
subsection "Booleans"
consts
i_bool :: interface
lemmas [autoref_rel_intf] = REL_INTFI[of bool_rel i_bool]
lemma [autoref_itype]:
"True ::⇩i i_bool"
"False ::⇩i i_bool"
"conj ::⇩i i_bool →⇩i i_bool →⇩i i_bool"
"(⟷) ::⇩i i_bool →⇩i i_bool →⇩i i_bool"
"(⟶) ::⇩i i_bool →⇩i i_bool →⇩i i_bool"
"disj ::⇩i i_bool →⇩i i_bool →⇩i i_bool"
"Not ::⇩i i_bool →⇩i i_bool"
"case_bool ::⇩i I →⇩i I →⇩i i_bool →⇩i I"
"old.rec_bool ::⇩i I →⇩i I →⇩i i_bool →⇩i I"
by auto
lemma autoref_bool[autoref_rules]:
"(x,x)∈bool_rel"
"(conj,conj)∈bool_rel→bool_rel→bool_rel"
"(disj,disj)∈bool_rel→bool_rel→bool_rel"
"(Not,Not)∈bool_rel→bool_rel"
"(case_bool,case_bool)∈R→R→bool_rel→R"
"(old.rec_bool,old.rec_bool)∈R→R→bool_rel→R"
"((⟷), (⟷))∈bool_rel→bool_rel→bool_rel"
"((⟶), (⟶))∈bool_rel→bool_rel→bool_rel"
by (auto split: bool.split simp: rec_bool_is_case)
subsection "Standard Type Classes"
context begin interpretation autoref_syn .
text ‹
We allow these operators for all interfaces.
›
lemma [autoref_itype]:
"(<) ::⇩i I →⇩i I →⇩i i_bool"
"(≤) ::⇩i I →⇩i I →⇩i i_bool"
"(=) ::⇩i I →⇩i I →⇩i i_bool"
"(+) ::⇩i I →⇩i I →⇩i I"
"(-) ::⇩i I →⇩i I →⇩i I"
"(div) ::⇩i I →⇩i I →⇩i I"
"(mod) ::⇩i I →⇩i I →⇩i I"
"(*) ::⇩i I →⇩i I →⇩i I"
"0 ::⇩i I"
"1 ::⇩i I"
"numeral x ::⇩i I"
"uminus ::⇩i I →⇩i I"
by auto
lemma pat_num_generic[autoref_op_pat]:
"0 ≡ OP 0 :::⇩i I"
"1 ≡ OP 1 :::⇩i I"
"numeral x ≡ (OP (numeral x) :::⇩i I)"
by simp_all
lemma [autoref_rules]:
assumes "PRIO_TAG_GEN_ALGO"
shows "((<), (<)) ∈ Id→Id→bool_rel"
and "((≤), (≤)) ∈ Id→Id→bool_rel"
and "((=), (=)) ∈ Id→Id→bool_rel"
and "(numeral x,OP (numeral x) ::: Id) ∈ Id"
and "(uminus,uminus) ∈ Id → Id"
and "(0,0) ∈ Id"
and "(1,1) ∈ Id"
by auto
subsection "Functional Combinators"
lemma [autoref_itype]: "id ::⇩i I →⇩i I" by simp
lemma autoref_id[autoref_rules]: "(id,id)∈R→R" by auto
term "(o)"
lemma [autoref_itype]: "(∘) ::⇩i (Ia→⇩iIb) →⇩i (Ic →⇩i Ia) →⇩i Ic →⇩i Ib"
by simp
lemma autoref_comp[autoref_rules]:
"((o), (o)) ∈ (Ra → Rb) → (Rc → Ra) → Rc → Rb"
by (auto dest: fun_relD)
lemma [autoref_itype]: "If ::⇩i i_bool →⇩i I →⇩i I →⇩i I" by simp
lemma autoref_If[autoref_rules]: "(If,If)∈Id→R→R→R" by auto
lemma autoref_If_cong[autoref_rules]:
assumes "(c',c)∈Id"
assumes "REMOVE_INTERNAL c ⟹ (t',t)∈R"
assumes "¬ REMOVE_INTERNAL c ⟹ (e',e)∈R"
shows "(If c' t' e',(OP If ::: Id→R→R→R)$c$t$e)∈R"
using assms by (auto)
lemma [autoref_itype]: "Let ::⇩i Ix →⇩i (Ix→⇩iIy) →⇩i Iy" by auto
lemma autoref_Let:
"(Let,Let)∈Ra → (Ra→Rr) → Rr"
by (auto dest: fun_relD)
lemma autoref_Let_cong[autoref_rules]:
assumes "(x',x)∈Ra"
assumes "⋀y y'. REMOVE_INTERNAL (x=y) ⟹ (y',y)∈Ra ⟹ (f' y', f$y)∈Rr"
shows "(Let x' f',(OP Let ::: Ra → (Ra → Rr) → Rr)$x$f)∈Rr"
using assms by (auto)
end
subsection "Unit"
consts i_unit :: interface
lemmas [autoref_rel_intf] = REL_INTFI[of unit_rel i_unit]
lemma [autoref_rules]: "((),())∈unit_rel" by simp
subsection "Nat"
consts i_nat :: interface
lemmas [autoref_rel_intf] = REL_INTFI[of nat_rel i_nat]
context begin interpretation autoref_syn .
lemma pat_num_nat[autoref_op_pat]:
"0::nat ≡ OP 0 :::⇩i i_nat"
"1::nat ≡ OP 1 :::⇩i i_nat"
"(numeral x)::nat ≡ (OP (numeral x) :::⇩i i_nat)"
by simp_all
lemma autoref_nat[autoref_rules]:
"(0, 0::nat) ∈ nat_rel"
"(Suc, Suc) ∈ nat_rel → nat_rel"
"(1, 1::nat) ∈ nat_rel"
"(numeral n::nat,numeral n::nat) ∈ nat_rel"
"((<), (<) ::nat ⇒ _) ∈ nat_rel → nat_rel → bool_rel"
"((≤), (≤) ::nat ⇒ _) ∈ nat_rel → nat_rel → bool_rel"
"((=), (=) ::nat ⇒ _) ∈ nat_rel → nat_rel → bool_rel"
"((+) ::nat⇒_,(+))∈nat_rel→nat_rel→nat_rel"
"((-) ::nat⇒_,(-))∈nat_rel→nat_rel→nat_rel"
"((div) ::nat⇒_,(div))∈nat_rel→nat_rel→nat_rel"
"((*), (*))∈nat_rel→nat_rel→nat_rel"
"((mod), (mod))∈nat_rel→nat_rel→nat_rel"
by auto
lemma autoref_case_nat[autoref_rules]:
"(case_nat,case_nat)∈Ra → (Id → Ra) → Id → Ra"
apply (intro fun_relI)
apply (auto split: nat.split dest: fun_relD)
done
lemma autoref_rec_nat: "(rec_nat,rec_nat) ∈ R → (Id → R → R) → Id → R"
apply (intro fun_relI)
proof goal_cases
case (1 s s' f f' n n') thus ?case
apply (induct n' arbitrary: n s s')
apply (fastforce simp: fun_rel_def)+
done
qed
end
subsection "Int"
consts i_int :: interface
lemmas [autoref_rel_intf] = REL_INTFI[of int_rel i_int]
context begin interpretation autoref_syn .
lemma pat_num_int[autoref_op_pat]:
"0::int ≡ OP 0 :::⇩i i_int"
"1::int ≡ OP 1 :::⇩i i_int"
"(numeral x)::int ≡ (OP (numeral x) :::⇩i i_int)"
by simp_all
lemma autoref_int[autoref_rules (overloaded)]:
"(0, 0::int) ∈ int_rel"
"(1, 1::int) ∈ int_rel"
"(numeral n::int,numeral n::int) ∈ int_rel"
"((<), (<) ::int ⇒ _) ∈ int_rel → int_rel → bool_rel"
"((≤), (≤) ::int ⇒ _) ∈ int_rel → int_rel → bool_rel"
"((=), (=) ::int ⇒ _) ∈ int_rel → int_rel → bool_rel"
"((+) ::int⇒_,(+))∈int_rel→int_rel→int_rel"
"((-) ::int⇒_,(-))∈int_rel→int_rel→int_rel"
"((div) ::int⇒_,(div))∈int_rel→int_rel→int_rel"
"(uminus,uminus)∈int_rel→int_rel"
"((*), (*))∈int_rel→int_rel→int_rel"
"((mod), (mod))∈int_rel→int_rel→int_rel"
by auto
end
subsection "Product"
consts i_prod :: "interface ⇒ interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of prod_rel i_prod]
context begin interpretation autoref_syn .
lemma prod_refine[autoref_rules]:
"(Pair,Pair)∈Ra → Rb → ⟨Ra,Rb⟩prod_rel"
"(case_prod,case_prod) ∈ (Ra → Rb → Rr) → ⟨Ra,Rb⟩prod_rel → Rr"
"(old.rec_prod,old.rec_prod) ∈ (Ra → Rb → Rr) → ⟨Ra,Rb⟩prod_rel → Rr"
"(fst,fst)∈⟨Ra,Rb⟩prod_rel → Ra"
"(snd,snd)∈⟨Ra,Rb⟩prod_rel → Rb"
by (auto dest: fun_relD split: prod.split
simp: prod_rel_def rec_prod_is_case)
definition "prod_eq eqa eqb x1 x2 ≡
case x1 of (a1,b1) ⇒ case x2 of (a2,b2) ⇒ eqa a1 a2 ∧ eqb b1 b2"
lemma prod_eq_autoref[autoref_rules (overloaded)]:
"⟦GEN_OP eqa (=) (Ra→Ra→Id); GEN_OP eqb (=) (Rb→Rb→Id)⟧
⟹ (prod_eq eqa eqb,(=)) ∈ ⟨Ra,Rb⟩prod_rel → ⟨Ra,Rb⟩prod_rel → Id"
unfolding prod_eq_def[abs_def]
by (fastforce dest: fun_relD)
lemma prod_eq_expand[autoref_struct_expand]: "(=) = prod_eq (=) (=)"
unfolding prod_eq_def[abs_def]
by (auto intro!: ext)
end
subsection "Option"
consts i_option :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of option_rel i_option]
context begin interpretation autoref_syn .
lemma autoref_opt[autoref_rules]:
"(None,None)∈⟨R⟩option_rel"
"(Some,Some)∈R → ⟨R⟩option_rel"
"(case_option,case_option)∈Rr→(R → Rr)→⟨R⟩option_rel → Rr"
"(rec_option,rec_option)∈Rr→(R → Rr)→⟨R⟩option_rel → Rr"
by (auto split: option.split
simp: option_rel_def case_option_def[symmetric]
dest: fun_relD)
lemma autoref_the[autoref_rules]:
assumes "SIDE_PRECOND (x≠None)"
assumes "(x',x)∈⟨R⟩option_rel"
shows "(the x', (OP the ::: ⟨R⟩option_rel → R)$x) ∈ R"
using assms
by (auto simp: option_rel_def)
lemma autoref_the_default[autoref_rules]:
"(the_default, the_default) ∈ R → ⟨R⟩option_rel → R"
by parametricity
definition [simp]: "is_None a ≡ case a of None ⇒ True | _ ⇒ False"
lemma pat_isNone[autoref_op_pat]:
"a=None ≡ (OP is_None :::⇩i ⟨I⟩⇩ii_option →⇩i i_bool)$a"
"None=a ≡ (OP is_None :::⇩i ⟨I⟩⇩ii_option →⇩i i_bool)$a"
by (auto intro!: eq_reflection split: option.splits)
lemma autoref_is_None[param,autoref_rules]:
"(is_None,is_None)∈⟨R⟩option_rel → Id"
by (auto split: option.splits)
lemma fold_is_None: "x=None ⟷ is_None x" by (cases x) auto
definition "option_eq eq v1 v2 ≡
case (v1,v2) of
(None,None) ⇒ True
| (Some x1, Some x2) ⇒ eq x1 x2
| _ ⇒ False"
lemma option_eq_autoref[autoref_rules (overloaded)]:
"⟦GEN_OP eq (=) (R→R→Id)⟧
⟹ (option_eq eq,(=)) ∈ ⟨R⟩option_rel → ⟨R⟩option_rel → Id"
unfolding option_eq_def[abs_def]
by (auto dest: fun_relD split: option.splits elim!: option_relE)
lemma option_eq_expand[autoref_struct_expand]:
"(=) = option_eq (=)"
by (auto intro!: ext simp: option_eq_def split: option.splits)
end
subsection "Sum-Types"
consts i_sum :: "interface ⇒ interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of sum_rel i_sum]
context begin interpretation autoref_syn .
lemma autoref_sum[autoref_rules]:
"(Inl,Inl) ∈ Rl → ⟨Rl,Rr⟩sum_rel"
"(Inr,Inr) ∈ Rr → ⟨Rl,Rr⟩sum_rel"
"(case_sum,case_sum) ∈ (Rl → R) → (Rr → R) → ⟨Rl,Rr⟩sum_rel → R"
"(old.rec_sum,old.rec_sum) ∈ (Rl → R) → (Rr → R) → ⟨Rl,Rr⟩sum_rel → R"
by (fastforce split: sum.split dest: fun_relD
simp: rec_sum_is_case)+
definition "sum_eq eql eqr s1 s2 ≡
case (s1,s2) of
(Inl x1, Inl x2) ⇒ eql x1 x2
| (Inr x1, Inr x2) ⇒ eqr x1 x2
| _ ⇒ False"
lemma sum_eq_autoref[autoref_rules (overloaded)]:
"⟦GEN_OP eql (=) (Rl→Rl→Id); GEN_OP eqr (=) (Rr→Rr→Id)⟧
⟹ (sum_eq eql eqr,(=)) ∈ ⟨Rl,Rr⟩sum_rel → ⟨Rl,Rr⟩sum_rel → Id"
unfolding sum_eq_def[abs_def]
by (fastforce dest: fun_relD elim!: sum_relE)
lemma sum_eq_expand[autoref_struct_expand]: "(=) = sum_eq (=) (=)"
by (auto intro!: ext simp: sum_eq_def split: sum.splits)
lemmas [autoref_rules] = is_Inl_param is_Inr_param
lemma autoref_sum_Projl[autoref_rules]:
"⟦SIDE_PRECOND (is_Inl s); (s',s)∈⟨Ra,Rb⟩sum_rel⟧
⟹ (Sum_Type.sum.projl s', (OP Sum_Type.sum.projl ::: ⟨Ra,Rb⟩sum_rel → Ra)$s)∈Ra"
by simp parametricity
lemma autoref_sum_Projr[autoref_rules]:
"⟦SIDE_PRECOND (is_Inr s); (s',s)∈⟨Ra,Rb⟩sum_rel⟧
⟹ (Sum_Type.sum.projr s', (OP Sum_Type.sum.projr ::: ⟨Ra,Rb⟩sum_rel → Rb)$s)∈Rb"
by simp parametricity
end
subsection "List"
consts i_list :: "interface ⇒ interface"
lemmas [autoref_rel_intf] = REL_INTFI[of list_rel i_list]
context begin interpretation autoref_syn .
lemma autoref_append[autoref_rules]:
"(append, append)∈⟨R⟩list_rel → ⟨R⟩list_rel → ⟨R⟩list_rel"
by (auto simp: list_rel_def list_all2_appendI)
lemma refine_list[autoref_rules]:
"(Nil,Nil)∈⟨R⟩list_rel"
"(Cons,Cons)∈R → ⟨R⟩list_rel → ⟨R⟩list_rel"
"(case_list,case_list)∈Rr→(R→⟨R⟩list_rel→Rr)→⟨R⟩list_rel→Rr"
apply (force dest: fun_relD split: list.split)+
done
lemma autoref_rec_list[autoref_rules]: "(rec_list,rec_list)
∈ Ra → (Rb → ⟨Rb⟩list_rel → Ra → Ra) → ⟨Rb⟩list_rel → Ra"
proof (intro fun_relI, goal_cases)
case prems: (1 a a' f f' l l')
from prems(3) show ?case
using prems(1,2)
apply (induct arbitrary: a a')
apply simp
apply (fastforce dest: fun_relD)
done
qed
lemma refine_map[autoref_rules]:
"(map,map)∈(R1→R2) → ⟨R1⟩list_rel → ⟨R2⟩list_rel"
using [[autoref_sbias = -1]]
unfolding map_rec[abs_def]
by autoref
lemma refine_fold[autoref_rules]:
"(fold,fold)∈(Re→Rs→Rs) → ⟨Re⟩list_rel → Rs → Rs"
"(foldl,foldl)∈(Rs→Re→Rs) → Rs → ⟨Re⟩list_rel → Rs"
"(foldr,foldr)∈(Re→Rs→Rs) → ⟨Re⟩list_rel → Rs → Rs"
unfolding List.fold_def List.foldr_def List.foldl_def
by (autoref)+
schematic_goal autoref_take[autoref_rules]: "(take,take)∈(?R::(_×_) set)"
unfolding take_def by autoref
schematic_goal autoref_drop[autoref_rules]: "(drop,drop)∈(?R::(_×_) set)"
unfolding drop_def by autoref
schematic_goal autoref_length[autoref_rules]:
"(length,length)∈(?R::(_×_) set)"
unfolding size_list_overloaded_def size_list_def
by (autoref)
lemma autoref_nth[autoref_rules]:
assumes "(l,l')∈⟨R⟩list_rel"
assumes "(i,i')∈Id"
assumes "SIDE_PRECOND (i' < length l')"
shows "(nth l i,(OP nth ::: ⟨R⟩list_rel → Id → R)$l'$i')∈R"
unfolding ANNOT_def
using assms
apply (induct arbitrary: i i')
apply simp
apply (case_tac i')
apply auto
done
fun list_eq :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
"list_eq eq [] [] ⟷ True"
| "list_eq eq (a#l) (a'#l')
⟷ (if eq a a' then list_eq eq l l' else False)"
| "list_eq _ _ _ ⟷ False"
lemma autoref_list_eq_aux: "
(list_eq,list_eq) ∈
(R → R → Id) → ⟨R⟩list_rel → ⟨R⟩list_rel → Id"
proof (intro fun_relI, goal_cases)
case (1 eq eq' l1 l1' l2 l2')
thus ?case
apply -
apply (induct eq' l1' l2' arbitrary: l1 l2 rule: list_eq.induct)
apply simp
apply (case_tac l1)
apply simp
apply (case_tac l2)
apply (simp)
apply (auto dest: fun_relD) []
apply (case_tac l1)
apply simp
apply simp
apply (case_tac l2)
apply simp
apply simp
done
qed
lemma list_eq_expand[autoref_struct_expand]: "(=) = (list_eq (=))"
proof (intro ext)
fix l1 l2 :: "'a list"
show "(l1 = l2) ⟷ list_eq (=) l1 l2"
apply (induct "(=) :: 'a ⇒ _" l1 l2 rule: list_eq.induct)
apply simp_all
done
qed
lemma autoref_list_eq[autoref_rules (overloaded)]:
"GEN_OP eq (=) (R→R→Id) ⟹ (list_eq eq, (=))
∈ ⟨R⟩list_rel → ⟨R⟩list_rel → Id"
unfolding autoref_tag_defs
apply (subst list_eq_expand)
apply (parametricity add: autoref_list_eq_aux)
done
lemma autoref_hd[autoref_rules]:
"⟦ SIDE_PRECOND (l'≠[]); (l,l') ∈ ⟨R⟩list_rel ⟧ ⟹
(hd l,(OP hd ::: ⟨R⟩list_rel → R)$l') ∈ R"
apply (simp add: ANNOT_def)
apply (cases l')
apply simp
apply (cases l)
apply auto
done
lemma autoref_tl[autoref_rules]:
"(tl,tl) ∈ ⟨R⟩list_rel → ⟨R⟩list_rel"
unfolding tl_def[abs_def]
by autoref
definition [simp]: "is_Nil a ≡ case a of [] ⇒ True | _ ⇒ False"
lemma is_Nil_pat[autoref_op_pat]:
"a=[] ≡ (OP is_Nil :::⇩i ⟨I⟩⇩ii_list →⇩i i_bool)$a"
"[]=a ≡ (OP is_Nil :::⇩i ⟨I⟩⇩ii_list →⇩i i_bool)$a"
by (auto intro!: eq_reflection split: list.splits)
lemma autoref_is_Nil[param,autoref_rules]:
"(is_Nil,is_Nil)∈⟨R⟩list_rel → bool_rel"
by (auto split: list.splits)
lemma conv_to_is_Nil:
"l=[] ⟷ is_Nil l"
"[]=l ⟷ is_Nil l"
unfolding is_Nil_def by (auto split: list.split)
lemma autoref_butlast[param, autoref_rules]:
"(butlast,butlast) ∈ ⟨R⟩list_rel → ⟨R⟩list_rel"
unfolding butlast_def conv_to_is_Nil
by parametricity
definition [simp]: "op_list_singleton x ≡ [x]"
lemma op_list_singleton_pat[autoref_op_pat]:
"[x] ≡ (OP op_list_singleton :::⇩i I →⇩i ⟨I⟩⇩ii_list)$x" by simp
lemma autoref_list_singleton[autoref_rules]:
"(λa. [a],op_list_singleton) ∈ R → ⟨R⟩list_rel"
by auto
definition [simp]: "op_list_append_elem s x ≡ s@[x]"
lemma pat_list_append_elem[autoref_op_pat]:
"s@[x] ≡ (OP op_list_append_elem :::⇩i ⟨I⟩⇩ii_list →⇩i I →⇩i ⟨I⟩⇩ii_list)$s$x"
by (simp add: relAPP_def)
lemma autoref_list_append_elem[autoref_rules]:
"(λs x. s@[x], op_list_append_elem) ∈ ⟨R⟩list_rel → R → ⟨R⟩list_rel"
unfolding op_list_append_elem_def[abs_def] by parametricity
declare param_rev[autoref_rules]
declare param_all_interval_nat[autoref_rules]
lemma [autoref_op_pat]:
"(∀i<u. P i) ≡ OP List.all_interval_nat P 0 u"
"(∀i≤u. P i) ≡ OP List.all_interval_nat P 0 (Suc u)"
"(∀i<u. l≤i ⟶ P i) ≡ OP List.all_interval_nat P l u"
"(∀i≤u. l≤i ⟶ P i) ≡ OP List.all_interval_nat P l (Suc u)"
by (auto intro!: eq_reflection simp: List.all_interval_nat_def)
lemmas [autoref_rules] = param_dropWhile param_takeWhile
end
subsection "Examples"
text ‹Be careful to make the concrete type a schematic type variable.
The default behaviour of ‹schematic_lemma› makes it a fixed variable,
that will not unify with the infered term!›
schematic_goal
"(?f::?'c,[1,2,3]@[4::nat])∈?R"
by autoref
schematic_goal
"(?f::?'c,[1::nat,
2,3,4,5,6,7,8,9,0,1,43,5,5,435,5,1,5,6,5,6,5,63,56
]
)∈?R"
apply (autoref)
done
schematic_goal
"(?f::?'c,[1,2,3] = [])∈?R"
by autoref
text ‹
When specifying custom refinement rules on the fly, be careful with
the type-inference between ‹notes› and ‹shows›. It's
too easy to ,,decouple'' the type ‹'a› in the autoref-rule and
the actual goal, as shown below!
›
schematic_goal
notes [autoref_rules] = IdI[where 'a="'a"]
notes [autoref_itype] = itypeI[where 't="'a::numeral" and I=i_std]
shows "(?f::?'c, hd [a,b,c::'a::numeral])∈?R"
txt ‹The autoref-rule is bound with type ‹'a::typ›, while
the goal statement has ‹'a::numeral›!›
apply (autoref (keep_goal))
txt ‹We get an unsolved goal, as it finds no rule to translate
‹a››
oops
text ‹Here comes the correct version. Note the duplicate sort annotation
of type ‹'a›:›
schematic_goal
notes [autoref_rules_raw] = IdI[where 'a="'a::numeral"]
notes [autoref_itype] = itypeI[where 't="'a::numeral" and I=i_std]
shows "(?f::?'c, hd [a,b,c::'a::numeral])∈?R"
by (autoref)
text ‹Special cases of equality: Note that we do not require equality
on the element type!›
schematic_goal
assumes [autoref_rules]: "(ai,a)∈⟨R⟩option_rel"
shows "(?f::?'c, a = None)∈?R"
apply (autoref (keep_goal))
done
schematic_goal
assumes [autoref_rules]: "(ai,a)∈⟨R⟩list_rel"
shows "(?f::?'c, [] = a)∈?R"
apply (autoref (keep_goal))
done
schematic_goal
shows "(?f::?'c, [1,2] = [2,3::nat])∈?R"
apply (autoref (keep_goal))
done
end