header {* \isaheader{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 op= op=) hashcode"}
This cannot be discharged by the rule
@{text [display] "is_hashcode op= 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"
"op <-> ::⇩i i_bool ->⇩i i_bool ->⇩i i_bool"
"op --> ::⇩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"
"(op <->, op <->)∈bool_rel->bool_rel->bool_rel"
"(op -->, op -->)∈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]:
"op < ::⇩i I ->⇩i I ->⇩i i_bool"
"op ≤ ::⇩i I ->⇩i I ->⇩i i_bool"
"op = ::⇩i I ->⇩i I ->⇩i i_bool"
"op + ::⇩i I ->⇩i I ->⇩i I"
"op - ::⇩i I ->⇩i I ->⇩i I"
"op div ::⇩i I ->⇩i I ->⇩i I"
"op mod ::⇩i I ->⇩i I ->⇩i I"
"op * ::⇩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 "(op <, op <) ∈ Id->Id->bool_rel"
and "(op ≤, op ≤) ∈ Id->Id->bool_rel"
and "(op =, op =) ∈ 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 "op o"
lemma [autoref_itype]: "op o ::⇩i (Ia->⇩iIb) ->⇩i (Ic ->⇩i Ia) ->⇩i Ic ->⇩i Ib"
by simp
lemma autoref_comp[autoref_rules]:
"(op o, op 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[autoref_rules]:
"(Let,Let)∈Ra -> (Ra->Rr) -> Rr"
by (auto dest: fun_relD)
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"
"(op <, op <::nat => _) ∈ nat_rel -> nat_rel -> bool_rel"
"(op ≤, op ≤::nat => _) ∈ nat_rel -> nat_rel -> bool_rel"
"(op =, op =::nat => _) ∈ nat_rel -> nat_rel -> bool_rel"
"(op +::nat=>_,op +)∈nat_rel->nat_rel->nat_rel"
"(op -::nat=>_,op -)∈nat_rel->nat_rel->nat_rel"
"(op div::nat=>_,op div)∈nat_rel->nat_rel->nat_rel"
"(op *, op *)∈nat_rel->nat_rel->nat_rel"
"(op mod, op 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 -
case (goal1 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)"
"(neg_numeral x)::int ≡ (OP (neg_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"
"(op <, op <::int => _) ∈ int_rel -> int_rel -> bool_rel"
"(op ≤, op ≤::int => _) ∈ int_rel -> int_rel -> bool_rel"
"(op =, op =::int => _) ∈ int_rel -> int_rel -> bool_rel"
"(op +::int=>_,op +)∈int_rel->int_rel->int_rel"
"(op -::int=>_,op -)∈int_rel->int_rel->int_rel"
"(op div::int=>_,op div)∈int_rel->int_rel->int_rel"
"(uminus,uminus)∈int_rel->int_rel"
"(op *, op *)∈int_rel->int_rel->int_rel"
"(op mod, op 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 op = (Ra->Ra->Id); GEN_OP eqb op = (Rb->Rb->Id)|]
==> (prod_eq eqa eqb,op =) ∈ ⟨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]: "op = = prod_eq op= op="
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[autoref_rules]:
"(is_None,is_None)∈⟨R⟩option_rel -> Id"
by (auto split: option.splits)
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 op = (R->R->Id)|]
==> (option_eq eq,op =) ∈ ⟨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]:
"op = = option_eq op="
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 op = (Rl->Rl->Id); GEN_OP eqr op = (Rr->Rr->Id)|]
==> (sum_eq eql eqr,op =) ∈ ⟨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]: "op = = sum_eq op= op="
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)
case (goal1 a a' f f' l l')
from goal1(3) show ?case
using goal1(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_lemma autoref_take[autoref_rules]: "(take,take)∈(?R::(_×_) set)"
unfolding take_def by autoref
schematic_lemma autoref_drop[autoref_rules]: "(drop,drop)∈(?R::(_×_) set)"
unfolding drop_def by autoref
schematic_lemma 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)
case (goal1 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]: "(op =) = (list_eq op =)"
proof (intro ext)
fix l1 l2 :: "'a list"
show "(l1 = l2) <-> list_eq op = l1 l2"
apply (induct "op = :: 'a => _" l1 l2 rule: list_eq.induct)
apply simp_all
done
qed
lemma autoref_list_eq[autoref_rules (overloaded)]:
"GEN_OP eq op = (R->R->Id) ==> (list_eq eq, op =)
∈ ⟨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)
end
subsection "Examples"
text {* Be careful to make the concrete type a schematic type variable.
The default behaviour of @{text "schematic_lemma"} makes it a fixed variable,
that will not unify with the infered term! *}
schematic_lemma
"(?f::?'c,[1,2,3]@[4::nat])∈?R"
by autoref
schematic_lemma
"(?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_lemma
"(?f::?'c,[1,2,3] = [])∈?R"
by autoref
text {*
When specifying custom refinement rules on the fly, be careful with
the type-inference between @{text "notes"} and @{text "shows"}. It's
too easy to ,,decouple'' the type @{text "'a"} in the autoref-rule and
the actual goal, as shown below!
*}
schematic_lemma
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 @{text "'a::typ"}, while
the goal statement has @{text "'a::numeral"}! *}
apply (autoref (keep_goal))
txt {* We get an unsolved goal, as it finds no rule to translate
@{text "a"} *}
oops
text {* Here comes the correct version. Note the duplicate sort annotation
of type @{text "'a"}: *}
schematic_lemma
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_lemma
assumes [autoref_rules]: "(ai,a)∈⟨R⟩option_rel"
shows "(?f::?'c, a = None)∈?R"
apply (autoref (keep_goal))
done
schematic_lemma
assumes [autoref_rules]: "(ai,a)∈⟨R⟩list_rel"
shows "(?f::?'c, [] = a)∈?R"
apply (autoref (keep_goal))
done
schematic_lemma
shows "(?f::?'c, [1,2] = [2,3::nat])∈?R"
apply (autoref (keep_goal))
done
end