isabelle: comparison src/HOL/Import/HOLLight/HOLLight.thy

equal deleted inserted replaced

-:ae634fad947e
+:18b41bba42b5
 lemma ARITH_ADD: "(op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (All::(nat => bool) => bool)
 (%xa::nat.
-(op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
+(op =::nat => nat => bool) ((plus::nat => nat => nat) x xa)
-((HOL.plus::nat => nat => nat) x xa))))
+((plus::nat => nat => nat) x xa))))
 ((op &::bool => bool => bool)
-((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
+((op =::nat => nat => bool) ((plus::nat => nat => nat) (0::nat) (0::nat))
 (0::nat))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat) (0::nat)
+((plus::nat => nat => nat) (0::nat)
 ((NUMERAL_BIT0::nat => nat) x))
 ((NUMERAL_BIT0::nat => nat) x)))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat) (0::nat)
+((plus::nat => nat => nat) (0::nat)
 ((NUMERAL_BIT1::nat => nat) x))
 ((NUMERAL_BIT1::nat => nat) x)))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
+((plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
 (0::nat))
 ((NUMERAL_BIT0::nat => nat) x)))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
+((plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
 (0::nat))
 ((NUMERAL_BIT1::nat => nat) x)))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (All::(nat => bool) => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT0::nat => nat) x)
 ((NUMERAL_BIT0::nat => nat) xa))
 ((NUMERAL_BIT0::nat => nat)
-((HOL.plus::nat => nat => nat) x xa)))))
+((plus::nat => nat => nat) x xa)))))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (All::(nat => bool) => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT0::nat => nat) x)
 ((NUMERAL_BIT1::nat => nat) xa))
 ((NUMERAL_BIT1::nat => nat)
-((HOL.plus::nat => nat => nat) x xa)))))
+((plus::nat => nat => nat) x xa)))))
 ((op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%x::nat.
 (All::(nat => bool) => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT1::nat => nat) x)
 ((NUMERAL_BIT0::nat => nat) xa))
 ((NUMERAL_BIT1::nat => nat)
-((HOL.plus::nat => nat => nat) x xa)))))
+((plus::nat => nat => nat) x xa)))))
 ((All::(nat => bool) => bool)
 (%x::nat.
 (All::(nat => bool) => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT1::nat => nat) x)
 ((NUMERAL_BIT1::nat => nat) xa))
 ((NUMERAL_BIT0::nat => nat)
 ((Suc::nat => nat)
-((HOL.plus::nat => nat => nat) x
+((plus::nat => nat => nat) x
 xa))))))))))))))"
 by (import hollight ARITH_ADD)
 lemma ARITH_MULT: "(op &::bool => bool => bool)
 ((All::(nat => bool) => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
 ((op *::nat => nat => nat)
 ((NUMERAL_BIT0::nat => nat) x)
 ((NUMERAL_BIT1::nat => nat) xa))
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT0::nat => nat) x)
 ((NUMERAL_BIT0::nat => nat)
 ((NUMERAL_BIT0::nat => nat)
 ((op *::nat => nat => nat) x xa)))))))
 ((op &::bool => bool => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
 ((op *::nat => nat => nat)
 ((NUMERAL_BIT1::nat => nat) x)
 ((NUMERAL_BIT0::nat => nat) xa))
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT0::nat => nat) xa)
 ((NUMERAL_BIT0::nat => nat)
 ((NUMERAL_BIT0::nat => nat)
 ((op *::nat => nat => nat) x xa)))))))
 ((All::(nat => bool) => bool)
 (%xa::nat.
 (op =::nat => nat => bool)
 ((op *::nat => nat => nat)
 ((NUMERAL_BIT1::nat => nat) x)
 ((NUMERAL_BIT1::nat => nat) xa))
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT1::nat => nat) x)
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((NUMERAL_BIT0::nat => nat) xa)
 ((NUMERAL_BIT0::nat => nat)
 ((NUMERAL_BIT0::nat => nat)
 ((op *::nat => nat => nat) x
 xa))))))))))))))))"
 (%u::('A::type, ('M::type, 'N::type) finite_sum) cart.
 (lambda::(nat => 'A::type) => ('A::type, 'N::type) cart)
 (%i::nat.
 ($::('A::type, ('M::type, 'N::type) finite_sum) cart
 => nat => 'A::type)
-u ((HOL.plus::nat => nat => nat) i
+u ((plus::nat => nat => nat) i
 ((dimindex::('M::type => bool) => nat)
 (hollight.UNIV::'M::type => bool)))))"
 lemma DEF_sndcart: "(op =::(('A::type, ('M::type, 'N::type) finite_sum) cart
 => ('A::type, 'N::type) cart)
 (%u::('A::type, ('M::type, 'N::type) finite_sum) cart.
 (lambda::(nat => 'A::type) => ('A::type, 'N::type) cart)
 (%i::nat.
 ($::('A::type, ('M::type, 'N::type) finite_sum) cart
 => nat => 'A::type)
-u ((HOL.plus::nat => nat => nat) i
+u ((plus::nat => nat => nat) i
 ((dimindex::('M::type => bool) => nat)
 (hollight.UNIV::'M::type => bool)))))"
 by (import hollight DEF_sndcart)
 lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
 (hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
 ((dimindex::('N::type => bool) => nat)
 (hollight.UNIV::'N::type => bool)))"
 by (import hollight DIMINDEX_HAS_SIZE_FINITE_SUM)
 lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
 ((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
 (hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
-((HOL.plus::nat => nat => nat)
+((plus::nat => nat => nat)
 ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
 ((dimindex::('N::type => bool) => nat)
 (hollight.UNIV::'N::type => bool)))"
 by (import hollight DIMINDEX_FINITE_SUM)
 => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
 => prop)
 (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
 ((iterate::(nat => nat => nat)
 => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
-(HOL.plus::nat => nat => nat))"
+(plus::nat => nat => nat))"
 lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
 => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
 => bool)
 (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
 ((iterate::(nat => nat => nat)
 => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
-(HOL.plus::nat => nat => nat))"
+(plus::nat => nat => nat))"
 by (import hollight DEF_nsum)
 lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
-((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
+((neutral::(nat => nat => nat) => nat) (plus::nat => nat => nat)) (0::nat)"
 by (import hollight NEUTRAL_ADD)
 lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
 by (import hollight NEUTRAL_MUL)
-lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
+lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (plus::nat => nat => nat)"
 by (import hollight MONOIDAL_ADD)
 lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
 by (import hollight MONOIDAL_MUL)
 t::'q_51175::type => bool.
 FINITE s & SUBSET t s --> nsum (DIFF s t) f = nsum s f - nsum t f"
 by (import hollight NSUM_DIFF)
 lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
-FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
+FINITE (support plus x xa) --> nsum (support plus x xa) x = nsum xa x"
 by (import hollight NSUM_SUPPORT)
 lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)
 s::'q_51260::type => bool.
 FINITE s --> nsum s (%x::'q_51260::type. f x + g x) = nsum s f + nsum s g"

changeset 34974	18b41bba42b5
parent 19233	77ca20b0ed77
child 35416	d8d7d1b785af