doc-src/Intro/intro.ind

New equivalence proofs

\begin{theindex}

  \item {\tt !!} symbol, 25
    \subitem in main goal, 46
  \item {\tt\%} symbol, 25
  \item {\tt ::} symbol, 25
  \item {\tt ==} symbol, 25
  \item {\tt ==>} symbol, 25
  \item {\tt =>} symbol, 25
  \item {\tt =?=} symbol, 25
  \item {\tt [} symbol, 25
  \item {\tt [|} symbol, 25
  \item {\tt ]} symbol, 25
  \item {\tt\ttlbrace} symbol, 25
  \item {\tt\ttrbrace} symbol, 25
  \item {\tt |]} symbol, 25

  \indexspace

  \item {\tt allI} theorem, 37
  \item arities
    \subitem declaring, 4, \bold{49}
  \item {\tt Asm_simp_tac}, 60
  \item {\tt assume_tac}, 30, 32, 37, 47
  \item assumptions
    \subitem deleting, 20
    \subitem discharge of, 7
    \subitem lifting over, 14
    \subitem of main goal, 41
    \subitem use of, 16, 28
  \item axioms
    \subitem Peano, 54

  \indexspace

  \item {\tt ba}, 31
  \item {\tt back}, 59, 62
  \item backtracking
    \subitem Prolog style, 62
  \item {\tt bd}, 31
  \item {\tt be}, 31
  \item {\tt Blast_tac}, 39
  \item {\tt br}, 31
  \item {\tt by}, 30

  \indexspace

  \item {\tt choplev}, 37, 64
  \item classes, 3
    \subitem built-in, \bold{25}
  \item classical reasoner, 39
  \item {\tt conjunct1} theorem, 28
  \item constants, 3
    \subitem clashes with variables, 9
    \subitem declaring, \bold{48}
    \subitem overloaded, 53
    \subitem polymorphic, 3
  \item {\tt CPure} theory, 47

  \indexspace

  \item definitions, 6, \bold{48}
    \subitem and derived rules, 43--46
  \item {\tt DEPTH_FIRST}, 64
  \item destruct-resolution, 22, 30
  \item {\tt disjE} theorem, 31
  \item {\tt dres_inst_tac}, 57
  \item {\tt dresolve_tac}, 30, 32, 33, 38

  \indexspace

  \item eigenvariables, \see{parameters}{8}
  \item elim-resolution, \bold{20}, 30
  \item equality
    \subitem polymorphic, 3
  \item {\tt eres_inst_tac}, 57
  \item {\tt eresolve_tac}, 30, 32, 33, 39, 47
  \item examples
    \subitem of deriving rules, 41
    \subitem of induction, 57, 58
    \subitem of simplification, 59
    \subitem of tacticals, 37
    \subitem of theories, 48, 50--55, 61
    \subitem propositional, 17, 31, 32
    \subitem with quantifiers, 18, 34, 35, 38
  \item {\tt exE} theorem, 38

  \indexspace

  \item {\tt FalseE} theorem, 45
  \item first-order logic, 1
  \item flex-flex constraints, 6, 25, \bold{28}
  \item {\tt flexflex_rule}, 29
  \item forward proof, 21, 24--30
  \item {\tt fun} type, 1, 4
  \item function applications, 1, 8

  \indexspace

  \item {\tt goal}, 30, 41, 46
  \item {\tt goalw}, 44--46

  \indexspace

  \item {\tt has_fewer_prems}, 64
  \item higher-order logic, 4

  \indexspace

  \item identifiers, 24
  \item {\tt impI} theorem, 31, 44
  \item infixes, 52
  \item instantiation, 57--60
  \item Isabelle
    \subitem object-logics supported, i
    \subitem overview, i
    \subitem release history, i

  \indexspace

  \item $\lambda$-abstractions, 1, 8, 25
  \item $\lambda$-calculus, 1
  \item LCF, i
  \item LCF system, 15, 27
  \item level of a proof, 31
  \item lifting, \bold{14}
  \item {\tt logic} class, 3, 6, 25

  \indexspace

  \item major premise, \bold{21}
  \item {\tt Match} exception, 42
  \item meta-assumptions
    \subitem syntax of, 22
  \item meta-equality, \bold{5}, 25
  \item meta-implication, \bold{5}, 7, 25
  \item meta-quantifiers, \bold{5}, 8, 25
  \item meta-rewriting, 43
  \item mixfix declarations, 52, 53, 56
  \item ML, i
  \item {\tt ML} section, 47
  \item {\tt mp} theorem, 27, 28

  \indexspace

  \item {\tt Nat} theory, 55
  \item {\tt nat} type, 3
  \item {\tt not_def} theorem, 44
  \item {\tt notE} theorem, \bold{45}, 57
  \item {\tt notI} theorem, \bold{44}, 57

  \indexspace

  \item {\tt o} type, 3, 4
  \item {\tt ORELSE}, 38
  \item overloading, \bold{4}, 53

  \indexspace

  \item parameters, \bold{8}, 34
    \subitem lifting over, 15
  \item {\tt Prolog} theory, 61
  \item Prolog interpreter, \bold{60}
  \item proof state, 16
  \item proofs
    \subitem commands for, 30
  \item {\tt PROP} symbol, 26
  \item {\tt prop} type, 6, 25, 26
  \item {\tt prth}, 27
  \item {\tt prthq}, 27, 29
  \item {\tt prths}, 27
  \item {\tt Pure} theory, 47

  \indexspace

  \item {\tt qed}, 31, 42, 46
  \item quantifiers, 5, 8, 34

  \indexspace

  \item {\tt read_instantiate}, 29
  \item {\tt refl} theorem, 29
  \item {\tt REPEAT}, 33, 38, 62, 64
  \item {\tt res_inst_tac}, 57, 59
  \item reserved words, 24
  \item resolution, 10, \bold{12}
    \subitem in backward proof, 15
    \subitem with instantiation, 57
  \item {\tt resolve_tac}, 30, 31, 46, 58
  \item {\tt result}, 31
  \item {\tt rewrite_goals_tac}, 44
  \item {\tt rewrite_rule}, 45, 46
  \item {\tt RL}, 29
  \item {\tt RLN}, 29
  \item {\tt RS}, 27, 29, 46
  \item {\tt RSN}, 27, 29
  \item rules
    \subitem declaring, 48
    \subitem derived, 13, \bold{22}, 41, 43
    \subitem destruction, 21
    \subitem elimination, 21
    \subitem propositional, 6
    \subitem quantifier, 8

  \indexspace

  \item search
    \subitem depth-first, 63
  \item signatures, \bold{9}
  \item {\tt Simp_tac}, 60
  \item simplification, 59
  \item simplification sets, 59
  \item sort constraints, 25
  \item sorts, \bold{5}
  \item {\tt spec} theorem, 28, 36, 37
  \item {\tt standard}, 27
  \item substitution, \bold{8}
  \item {\tt Suc_inject}, 58
  \item {\tt Suc_neq_0}, 58
  \item syntax
    \subitem of types and terms, 25

  \indexspace

  \item tacticals, \bold{19}, 37
  \item tactics, \bold{19}
    \subitem assumption, 30
    \subitem resolution, 30
  \item {\tt term} class, 3
  \item terms
    \subitem syntax of, 1, \bold{25}
  \item theorems
    \subitem basic operations on, \bold{27}
    \subitem printing of, 27
  \item theories, \bold{9}
    \subitem defining, 47--56
  \item {\tt thm} ML type, 27
  \item {\tt topthm}, 42
  \item {\tt Trueprop} constant, 6, 7, 25
  \item type constraints, 25
  \item type constructors, 1
  \item type identifiers, 24
  \item type synonyms, \bold{51}
  \item types
    \subitem declaring, \bold{49}
    \subitem function, 1
    \subitem higher, \bold{5}
    \subitem polymorphic, \bold{3}
    \subitem simple, \bold{1}
    \subitem syntax of, 1, \bold{25}

  \indexspace

  \item {\tt undo}, 30
  \item unification
    \subitem higher-order, \bold{11}, 58
    \subitem incompleteness of, 11
  \item unknowns, 10, 24, 34
    \subitem function, \bold{11}, 28, 34
  \item {\tt use_thy}, \bold{47, 48}

  \indexspace

  \item variables
    \subitem bound, 8

\end{theindex}