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"



  
  (* TODO: Most of these are parametricity theorems! *)

  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_relbool_relbool_rel"
    "(disj,disj)bool_relbool_relbool_rel"
    "(Not,Not)bool_relbool_rel"
    "(case_bool,case_bool)RRbool_relR"
    "(old.rec_bool,old.rec_bool)RRbool_relR"
    "((⟷), (⟷))bool_relbool_relbool_rel"
    "((⟶), (⟶))bool_relbool_relbool_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 "((<), (<))  IdIdbool_rel"
    and "((≤), (≤))  IdIdbool_rel"
    and "((=), (=))  IdIdbool_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)RR" by auto

  term "(o)"
  lemma [autoref_itype]: "(∘) ::i (IaiIb) 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)IdRRR" 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 ::: IdRRR)$c$t$e)R"
    using assms by (auto)

  lemma [autoref_itype]: "Let ::i Ix i (IxiIy) i Iy" by auto
  lemma autoref_Let: 
    "(Let,Let)Ra  (RaRr)  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_itype]: "(a::unit) ::i i_unit" by simp*)
  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_relnat_relnat_rel"
      "((-) ::nat_,(-))nat_relnat_relnat_rel"
      "((div) ::nat_,(div))nat_relnat_relnat_rel"
      "((*), (*))nat_relnat_relnat_rel"
      "((mod), (mod))nat_relnat_relnat_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_itype]:
      "((<) :: int ⇒ _) ::i i_int →i i_int →i i_bool"
      "((≤) :: int ⇒ _) ::i i_int →i i_int →i i_bool"
      "((=) :: int ⇒ _) ::i i_int →i i_int →i i_bool"
      "((+) :: int ⇒ _) ::i i_int →i i_int →i i_int"
      "((-) :: int ⇒ _) ::i i_int →i i_int →i i_int"
      "((div) :: int ⇒ _) ::i i_int →i i_int →i i_int"
      "(uminus :: int ⇒ _) ::i i_int →i i_int"
      by auto*)

    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_relint_relint_rel"
      "((-) ::int_,(-))int_relint_relint_rel"
      "((div) ::int_,(div))int_relint_relint_rel"
      "(uminus,uminus)int_relint_rel"
      "((*), (*))int_relint_relint_rel"
      "((mod), (mod))int_relint_relint_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 [autoref_itype]:
      "Pair ::i Ia →i Ib →i ⟨Ia,Ib⟩ii_prod"
      "case_prod ::i (Ia →i Ib →i I) →i ⟨Ia,Ib⟩ii_prod →i I"
      "old.rec_prod ::i (Ia →i Ib →i I) →i ⟨Ia,Ib⟩ii_prod →i I"
      "fst ::i ⟨Ia,Ib⟩ii_prod →i Ia"
      "snd ::i ⟨Ia,Ib⟩ii_prod →i Ib"
      "((=) :: _×_ ⇒ _) ::i ⟨Ia,Ib⟩ii_prod →i ⟨Ia,Ib⟩ii_prod →i i_bool"
      by auto
      *)

    lemma prod_refine[autoref_rules]:
      "(Pair,Pair)Ra  Rb  Ra,Rbprod_rel"
      "(case_prod,case_prod)  (Ra  Rb  Rr)  Ra,Rbprod_rel  Rr"
      "(old.rec_prod,old.rec_prod)  (Ra  Rb  Rr)  Ra,Rbprod_rel  Rr"
      "(fst,fst)Ra,Rbprod_rel  Ra"
      "(snd,snd)Ra,Rbprod_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 (=) (RaRaId); GEN_OP eqb (=) (RbRbId) 
       (prod_eq eqa eqb,(=))  Ra,Rbprod_rel  Ra,Rbprod_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_itype]:
      "None ::i ⟨I⟩ii_option"
      "Some ::i I →i ⟨I⟩ii_option"
      "the ::i ⟨I⟩ii_option →i I"
      "case_option ::i I →i (Iv→iI) →i ⟨Iv⟩ii_option →i I"
      "rec_option ::i I →i (Iv→iI) →i ⟨Iv⟩ii_option →i I"
      "((=) :: _ option ⇒ _) ::i ⟨I⟩ii_option →i ⟨I⟩ii_option →i i_bool"
      by auto
      *)

    lemma autoref_opt[autoref_rules]:
      "(None,None)Roption_rel"
      "(Some,Some)R  Roption_rel"
      "(case_option,case_option)Rr(R  Rr)Roption_rel  Rr"
      "(rec_option,rec_option)Rr(R  Rr)Roption_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 (xNone)"
      assumes "(x',x)Roption_rel"
      shows "(the x', (OP the ::: Roption_rel  R)$x)  R"
      using assms
      by (auto simp: option_rel_def)

    lemma autoref_the_default[autoref_rules]:
      "(the_default, the_default)  R  Roption_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 Iii_option i i_bool)$a"
      "None=a  (OP is_None :::i Iii_option i i_bool)$a"
      by (auto intro!: eq_reflection split: option.splits)
    lemma autoref_is_None[param,autoref_rules]: 
      "(is_None,is_None)Roption_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 (=) (RRId) 
       (option_eq eq,(=))  Roption_rel  Roption_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_itype]:
    "((=) :: _+_ ⇒ _) ::i ⟨Il,Ir⟩ii_sum →i ⟨Il,Ir⟩ii_sum →i i_bool"
    "Inl ::i Il →i ⟨Il,Ir⟩ii_sum"
    "Inr ::i Ir →i ⟨Il,Ir⟩ii_sum"
    "case_sum ::i (Il→iI) →i (Ir →i I) →i ⟨Il,Ir⟩ii_sum →i I"
    "old.rec_sum ::i (Il→iI) →i (Ir →i I) →i ⟨Il,Ir⟩ii_sum →i I"
    by auto*)

  lemma autoref_sum[autoref_rules]:
    "(Inl,Inl)  Rl  Rl,Rrsum_rel"
    "(Inr,Inr)  Rr  Rl,Rrsum_rel"
    "(case_sum,case_sum)  (Rl  R)  (Rr  R)  Rl,Rrsum_rel  R"
    "(old.rec_sum,old.rec_sum)  (Rl  R)  (Rr  R)  Rl,Rrsum_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 (=) (RlRlId); GEN_OP eqr (=) (RrRrId) 
     (sum_eq eql eqr,(=))  Rl,Rrsum_rel  Rl,Rrsum_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,Rbsum_rel 
     (Sum_Type.sum.projl s', (OP Sum_Type.sum.projl ::: Ra,Rbsum_rel  Ra)$s)Ra"
    by simp parametricity

  lemma autoref_sum_Projr[autoref_rules]: 
    "SIDE_PRECOND (is_Inr s); (s',s)Ra,Rbsum_rel 
     (Sum_Type.sum.projr s', (OP Sum_Type.sum.projr ::: Ra,Rbsum_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 .
  (*
  term nth
  lemma [autoref_itype]:
    "((=) :: _ list ⇒ _) ::i ⟨I⟩ii_list →i ⟨I⟩ii_list →i i_bool"
    "[] ::i ⟨I⟩ii_list"
    "(#) ::i I →i ⟨I⟩ii_list →i ⟨I⟩ii_list"
    "(@) ::i ⟨I⟩ii_list →i ⟨I⟩ii_list →i ⟨I⟩ii_list"
    "case_list ::i Ir →i (I→i⟨I⟩ii_list→iIr) →i ⟨I⟩ii_list →i Ir"
    "rec_list ::i Ir →i (I→i⟨I⟩ii_list→iIr→iIr) →i ⟨I⟩ii_list →i Ir"
    "map ::i (I1→iI2) →i ⟨I1⟩ii_list →i ⟨I2⟩ii_list"
    "foldl ::i (Ia→iIb→iIa) →i Ia →i ⟨Ib⟩ii_list →i Ia"
    "foldr ::i (Ia→iIb→iIb) →i ⟨Ia⟩ii_list →i Ib →i Ib"
    "fold ::i (Ia→iIb→iIb) →i ⟨Ia⟩ii_list →i Ib →i Ib"
    "take ::i i_nat →i ⟨I⟩ii_list →i ⟨I⟩ii_list"
    "drop ::i i_nat →i ⟨I⟩ii_list →i ⟨I⟩ii_list"
    "length ::i ⟨I⟩ii_list →i i_nat"
    "nth ::i ⟨I⟩ii_list →i i_nat →i I"
    "hd ::i ⟨I⟩ii_list →i I"
    "tl ::i ⟨I⟩ii_list →i ⟨I⟩ii_list"
    "last ::i ⟨I⟩ii_list →i I"
    "butlast ::i ⟨I⟩ii_list →i ⟨I⟩ii_list"
    by auto
    *)

  lemma autoref_append[autoref_rules]: 
    "(append, append)Rlist_rel  Rlist_rel  Rlist_rel"
    by (auto simp: list_rel_def list_all2_appendI)

  lemma refine_list[autoref_rules]:
    "(Nil,Nil)Rlist_rel"
    "(Cons,Cons)R  Rlist_rel  Rlist_rel"
    "(case_list,case_list)Rr(RRlist_relRr)Rlist_relRr"
    apply (force dest: fun_relD split: list.split)+
    done

  lemma autoref_rec_list[autoref_rules]: "(rec_list,rec_list) 
     Ra  (Rb  Rblist_rel  Ra  Ra)  Rblist_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)(R1R2)  R1list_rel  R2list_rel"
    using [[autoref_sbias = -1]]
    unfolding map_rec[abs_def]
    by autoref

  lemma refine_fold[autoref_rules]: 
    "(fold,fold)(ReRsRs)  Relist_rel  Rs  Rs"
    "(foldl,foldl)(RsReRs)  Rs  Relist_rel  Rs"
    "(foldr,foldr)(ReRsRs)  Relist_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')Rlist_rel"
    assumes "(i,i')Id"
    assumes "SIDE_PRECOND (i' < length l')"
    shows "(nth l i,(OP nth ::: Rlist_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)  Rlist_rel  Rlist_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 (=) (RRId)  (list_eq eq, (=)) 
     Rlist_rel  Rlist_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')  Rlist_rel  
      (hd l,(OP hd ::: Rlist_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)  Rlist_rel  Rlist_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 Iii_list i i_bool)$a"
    "[]=a  (OP is_Nil :::i Iii_list i i_bool)$a"
    by (auto intro!: eq_reflection split: list.splits)

  lemma autoref_is_Nil[param,autoref_rules]: 
    "(is_Nil,is_Nil)Rlist_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)  Rlist_rel  Rlist_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 Iii_list)$x" by simp
  lemma autoref_list_singleton[autoref_rules]: 
    "(λa. [a],op_list_singleton)  R  Rlist_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 Iii_list i I i Iii_list)$s$x" 
    by (simp add: relAPP_def)

  lemma autoref_list_append_elem[autoref_rules]: 
    "(λs x. s@[x], op_list_append_elem)  Rlist_rel  R  Rlist_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"
    "(iu. P i)  OP List.all_interval_nat P 0 (Suc u)"
    "(i<u. li  P i)  OP List.all_interval_nat P l u"
    "(iu. li  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 
  (*notes [autoref_itype] = itypeI[of a "⟨I⟩ii_option"]*)
  assumes [autoref_rules]: "(ai,a)Roption_rel"
  shows "(?f::?'c, a = None)?R"
  apply (autoref (keep_goal))
  done


schematic_goal 
  (*notes [autoref_itype] = itypeI[of a "⟨I⟩ii_list"]*)
  assumes [autoref_rules]: "(ai,a)Rlist_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