{- |
module: $Header$
description: Higher order logic terms modulo alpha-equivalence
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.TermAlpha
where

import Data.Set (Set)
import qualified Data.Set as Set
import qualified HOL.Const as Const
import HOL.Data
import HOL.Name
import qualified HOL.Subst as Subst
import qualified HOL.Term as Term
import qualified HOL.Type as Type
import qualified HOL.TypeOp as TypeOp
import qualified HOL.TypeVar as TypeVar
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Terms modulo alpha-equivalence
-------------------------------------------------------------------------------

newtype TermAlpha = TermAlpha Term
  deriving Int -> TermAlpha -> ShowS
[TermAlpha] -> ShowS
TermAlpha -> String
(Int -> TermAlpha -> ShowS)
-> (TermAlpha -> String)
-> ([TermAlpha] -> ShowS)
-> Show TermAlpha
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TermAlpha] -> ShowS
$cshowList :: [TermAlpha] -> ShowS
show :: TermAlpha -> String
$cshow :: TermAlpha -> String
showsPrec :: Int -> TermAlpha -> ShowS
$cshowsPrec :: Int -> TermAlpha -> ShowS
Show

instance Eq TermAlpha where
  (TermAlpha Term
tm1) == :: TermAlpha -> TermAlpha -> Bool
== (TermAlpha Term
tm2) = Term -> Term -> Bool
Term.alphaEqual Term
tm1 Term
tm2

instance Ord TermAlpha where
  compare :: TermAlpha -> TermAlpha -> Ordering
compare (TermAlpha Term
tm1) (TermAlpha Term
tm2) = Term -> Term -> Ordering
Term.alphaCompare Term
tm1 Term
tm2

-------------------------------------------------------------------------------
-- Constructors and destructors
-------------------------------------------------------------------------------

mk :: Term -> TermAlpha
mk :: Term -> TermAlpha
mk = Term -> TermAlpha
TermAlpha

dest :: TermAlpha -> Term
dest :: TermAlpha -> Term
dest (TermAlpha Term
tm) = Term
tm

-------------------------------------------------------------------------------
-- Type
-------------------------------------------------------------------------------

typeOf :: TermAlpha -> Type
typeOf :: TermAlpha -> Type
typeOf = Term -> Type
Term.typeOf (Term -> Type) -> (TermAlpha -> Term) -> TermAlpha -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Term
dest

isBool :: TermAlpha -> Bool
isBool :: TermAlpha -> Bool
isBool = Type -> Bool
Type.isBool (Type -> Bool) -> (TermAlpha -> Type) -> TermAlpha -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Type
typeOf

-------------------------------------------------------------------------------
-- Type variables
-------------------------------------------------------------------------------

instance TypeVar.HasVars TermAlpha where
  vars :: TermAlpha -> Set TypeVar
vars = Term -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars (Term -> Set TypeVar)
-> (TermAlpha -> Term) -> TermAlpha -> Set TypeVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Term
dest

-------------------------------------------------------------------------------
-- Type operators
-------------------------------------------------------------------------------

instance TypeOp.HasOps TermAlpha where
  ops :: TermAlpha -> Set TypeOp
ops = Term -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops (Term -> Set TypeOp)
-> (TermAlpha -> Term) -> TermAlpha -> Set TypeOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Term
dest

-------------------------------------------------------------------------------
-- Constants
-------------------------------------------------------------------------------

instance Const.HasConsts TermAlpha where
  consts :: TermAlpha -> Set Const
consts = Term -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts (Term -> Set Const)
-> (TermAlpha -> Term) -> TermAlpha -> Set Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Term
dest

-------------------------------------------------------------------------------
-- Free variables
-------------------------------------------------------------------------------

instance Var.HasFree TermAlpha where
  free :: TermAlpha -> Set Var
free = Term -> Set Var
forall a. HasFree a => a -> Set Var
Var.free (Term -> Set Var) -> (TermAlpha -> Term) -> TermAlpha -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Term
dest

-------------------------------------------------------------------------------
-- Substitutions
-------------------------------------------------------------------------------

instance Subst.CanSubst TermAlpha where
  basicSubst :: TermAlpha -> Subst -> (Maybe TermAlpha, Subst)
basicSubst (TermAlpha Term
tm) Subst
sub =
      (Maybe TermAlpha
atm',Subst
sub')
    where
      (Maybe Term
tm',Subst
sub') = Term -> Subst -> (Maybe Term, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
Subst.basicSubst Term
tm Subst
sub
      atm' :: Maybe TermAlpha
atm' = (Term -> TermAlpha) -> Maybe Term -> Maybe TermAlpha
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> TermAlpha
TermAlpha Maybe Term
tm'

-------------------------------------------------------------------------------
-- Standard axioms
-------------------------------------------------------------------------------

axiomOfExtensionality :: TermAlpha
axiomOfExtensionality :: TermAlpha
axiomOfExtensionality =
    case Maybe Term
axiom of
      Just Term
tm -> Term -> TermAlpha
mk Term
tm
      Maybe Term
Nothing -> String -> TermAlpha
forall a. HasCallStack => String -> a
error String
"HOL.TermAlpha.axiomOfExtensionality"
  where
    axiom :: Maybe Term
axiom = do
        let ty0 :: Type
ty0 = Type
Type.alpha
        let ty1 :: Type
ty1 = Type
Type.beta
        let ty2 :: Type
ty2 = Type -> Type -> Type
Type.mkFun Type
ty0 Type
ty1
        let ty3 :: Type
ty3 = Type
Type.bool
        let ty4 :: Type
ty4 = Type -> Type -> Type
Type.mkFun Type
ty2 Type
ty3
        let v0 :: Var
v0 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"a") Type
ty4
        let v1 :: Var
v1 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"b") Type
ty2
        let v2 :: Var
v2 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"c") Type
ty3
        let v3 :: Var
v3 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"d") Type
ty2
        let v4 :: Var
v4 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"e") Type
ty0
        let tm0 :: Term
tm0 = Var -> Term
Term.mkVar Var
v0
        let tm1 :: Term
tm1 = Var -> Term
Term.mkVar Var
v2
        let tm2 :: Term
tm2 = Var -> Term -> Term
Term.mkAbs Var
v2 Term
tm1
        let tm3 :: Term
tm3 = Term -> Term
Term.mkRefl Term
tm2
        let tm4 :: Term
tm4 = Var -> Term -> Term
Term.mkAbs Var
v1 Term
tm3
        Term
tm5 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm0 Term
tm4
        let tm6 :: Term
tm6 = Var -> Term -> Term
Term.mkAbs Var
v0 Term
tm5
        let tm7 :: Term
tm7 = Var -> Term
Term.mkVar Var
v3
        let tm8 :: Term
tm8 = Var -> Term
Term.mkVar Var
v4
        Term
tm9 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm7 Term
tm8
        let tm10 :: Term
tm10 = Var -> Term -> Term
Term.mkAbs Var
v4 Term
tm9
        Term
tm11 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm10 Term
tm7
        let tm12 :: Term
tm12 = Var -> Term -> Term
Term.mkAbs Var
v3 Term
tm11
        Term
tm13 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm6 Term
tm12
        Term -> Maybe Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm13

axiomOfChoice :: TermAlpha
axiomOfChoice :: TermAlpha
axiomOfChoice =
    case Maybe Term
axiom of
      Just Term
tm -> Term -> TermAlpha
mk Term
tm
      Maybe Term
Nothing -> String -> TermAlpha
forall a. HasCallStack => String -> a
error String
"HOL.TermAlpha.axiomOfChoice"
  where
    axiom :: Maybe Term
axiom = do
        let ty0 :: Type
ty0 = Type
Type.alpha
        let ty1 :: Type
ty1 = Type
Type.bool
        let ty2 :: Type
ty2 = Type -> Type -> Type
Type.mkFun Type
ty0 Type
ty1
        let ty3 :: Type
ty3 = Type -> Type -> Type
Type.mkFun Type
ty2 Type
ty1
        let ty4 :: Type
ty4 = Type -> Type -> Type
Type.mkFun Type
ty1 Type
ty1
        let ty5 :: Type
ty5 = Type -> Type -> Type
Type.mkFun Type
ty1 Type
ty4
        let v0 :: Var
v0 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"a") Type
ty3
        let v1 :: Var
v1 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"b") Type
ty2
        let v2 :: Var
v2 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"c") Type
ty1
        let v3 :: Var
v3 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"d") Type
ty2
        let v4 :: Var
v4 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"e") Type
ty2
        let v5 :: Var
v5 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"f") Type
ty0
        let v6 :: Var
v6 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"g") Type
ty0
        let v7 :: Var
v7 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"h") Type
ty1
        let v8 :: Var
v8 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"i") Type
ty1
        let v9 :: Var
v9 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"j") Type
ty1
        let v10 :: Var
v10 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"k") Type
ty1
        let v11 :: Var
v11 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"l") Type
ty5
        let v12 :: Var
v12 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"m") Type
ty5
        let tm0 :: Term
tm0 = Var -> Term
Term.mkVar Var
v0
        let tm1 :: Term
tm1 = Var -> Term
Term.mkVar Var
v2
        let tm2 :: Term
tm2 = Var -> Term -> Term
Term.mkAbs Var
v2 Term
tm1
        let tm3 :: Term
tm3 = Term -> Term
Term.mkRefl Term
tm2
        let tm4 :: Term
tm4 = Var -> Term -> Term
Term.mkAbs Var
v1 Term
tm3
        Term
tm5 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm0 Term
tm4
        let tm6 :: Term
tm6 = Var -> Term -> Term
Term.mkAbs Var
v0 Term
tm5
        let tm7 :: Term
tm7 = Var -> Term
Term.mkVar Var
v4
        let tm8 :: Term
tm8 = Var -> Term -> Term
Term.mkAbs Var
v5 Term
tm3
        Term
tm9 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm7 Term
tm8
        let tm10 :: Term
tm10 = Var -> Term -> Term
Term.mkAbs Var
v4 Term
tm9
        let tm11 :: Term
tm11 = Var -> Term
Term.mkVar Var
v11
        let tm12 :: Term
tm12 = Var -> Term
Term.mkVar Var
v9
        Term
tm13 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm11 Term
tm12
        let tm14 :: Term
tm14 = Var -> Term
Term.mkVar Var
v10
        Term
tm15 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm13 Term
tm14
        let tm16 :: Term
tm16 = Var -> Term -> Term
Term.mkAbs Var
v11 Term
tm15
        let tm17 :: Term
tm17 = Var -> Term
Term.mkVar Var
v12
        Term
tm18 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm17 Term
tm3
        Term
tm19 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm18 Term
tm3
        let tm20 :: Term
tm20 = Var -> Term -> Term
Term.mkAbs Var
v12 Term
tm19
        Term
tm21 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm16 Term
tm20
        let tm22 :: Term
tm22 = Var -> Term -> Term
Term.mkAbs Var
v10 Term
tm21
        let tm23 :: Term
tm23 = Var -> Term -> Term
Term.mkAbs Var
v9 Term
tm22
        let tm24 :: Term
tm24 = Var -> Term
Term.mkVar Var
v7
        Term
tm25 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm23 Term
tm24
        let tm26 :: Term
tm26 = Var -> Term
Term.mkVar Var
v8
        Term
tm27 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm25 Term
tm26
        Term
tm28 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm27 Term
tm24
        let tm29 :: Term
tm29 = Var -> Term -> Term
Term.mkAbs Var
v8 Term
tm28
        let tm30 :: Term
tm30 = Var -> Term -> Term
Term.mkAbs Var
v7 Term
tm29
        let tm31 :: Term
tm31 = Var -> Term
Term.mkVar Var
v3
        let tm32 :: Term
tm32 = Var -> Term
Term.mkVar Var
v6
        Term
tm33 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm31 Term
tm32
        Term
tm34 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm30 Term
tm33
        let tm35 :: Term
tm35 = Type -> Term
Term.mkSelectConst Type
ty0
        Term
tm36 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm35 Term
tm31
        Term
tm37 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm31 Term
tm36
        Term
tm38 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm34 Term
tm37
        let tm39 :: Term
tm39 = Var -> Term -> Term
Term.mkAbs Var
v6 Term
tm38
        Term
tm40 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm10 Term
tm39
        let tm41 :: Term
tm41 = Var -> Term -> Term
Term.mkAbs Var
v3 Term
tm40
        Term
tm42 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm6 Term
tm41
        Term -> Maybe Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm42

axiomOfInfinity :: TermAlpha
axiomOfInfinity :: TermAlpha
axiomOfInfinity =
    case Maybe Term
axiom of
      Just Term
tm -> Term -> TermAlpha
mk Term
tm
      Maybe Term
Nothing -> String -> TermAlpha
forall a. HasCallStack => String -> a
error String
"HOL.TermAlpha.axiomOfInfinity"
  where
    axiom :: Maybe Term
axiom = do
        let ty0 :: Type
ty0 = Type
Type.ind
        let ty1 :: Type
ty1 = Type -> Type -> Type
Type.mkFun Type
ty0 Type
ty0
        let ty2 :: Type
ty2 = Type
Type.bool
        let ty3 :: Type
ty3 = Type -> Type -> Type
Type.mkFun Type
ty1 Type
ty2
        let ty4 :: Type
ty4 = Type -> Type -> Type
Type.mkFun Type
ty2 Type
ty2
        let ty5 :: Type
ty5 = Type -> Type -> Type
Type.mkFun Type
ty2 Type
ty4
        let ty6 :: Type
ty6 = Type -> Type -> Type
Type.mkFun Type
ty0 Type
ty2
        let v0 :: Var
v0 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"a") Type
ty3
        let v1 :: Var
v1 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"b") Type
ty4
        let v2 :: Var
v2 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"c") Type
ty2
        let v3 :: Var
v3 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"d") Type
ty2
        let v4 :: Var
v4 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"e") Type
ty2
        let v5 :: Var
v5 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"f") Type
ty2
        let v6 :: Var
v6 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"g") Type
ty2
        let v7 :: Var
v7 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"h") Type
ty2
        let v8 :: Var
v8 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"i") Type
ty2
        let v9 :: Var
v9 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"j") Type
ty5
        let v10 :: Var
v10 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"k") Type
ty5
        let v11 :: Var
v11 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"l") Type
ty3
        let v12 :: Var
v12 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"m") Type
ty1
        let v13 :: Var
v13 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"n") Type
ty1
        let v14 :: Var
v14 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"p") Type
ty1
        let v15 :: Var
v15 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"q") Type
ty6
        let v16 :: Var
v16 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"r") Type
ty0
        let v17 :: Var
v17 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"s") Type
ty0
        let v18 :: Var
v18 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"t") Type
ty0
        let v19 :: Var
v19 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"u") Type
ty2
        let v20 :: Var
v20 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"v") Type
ty0
        let v21 :: Var
v21 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"w") Type
ty6
        let v22 :: Var
v22 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"x") Type
ty2
        let v23 :: Var
v23 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"y") Type
ty0
        let v24 :: Var
v24 = Name -> Type -> Var
Var.mk (String -> Name
mkGlobal String
"z") Type
ty0
        let tm0 :: Term
tm0 = Var -> Term
Term.mkVar Var
v1
        let tm1 :: Term
tm1 = Var -> Term
Term.mkVar Var
v3
        let tm2 :: Term
tm2 = Var -> Term -> Term
Term.mkAbs Var
v3 Term
tm1
        let tm3 :: Term
tm3 = Term -> Term
Term.mkRefl Term
tm2
        let tm4 :: Term
tm4 = Var -> Term -> Term
Term.mkAbs Var
v2 Term
tm3
        Term
tm5 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm0 Term
tm4
        let tm6 :: Term
tm6 = Var -> Term -> Term
Term.mkAbs Var
v1 Term
tm5
        let tm7 :: Term
tm7 = Var -> Term
Term.mkVar Var
v9
        let tm8 :: Term
tm8 = Var -> Term
Term.mkVar Var
v7
        Term
tm9 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm7 Term
tm8
        let tm10 :: Term
tm10 = Var -> Term
Term.mkVar Var
v8
        Term
tm11 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm9 Term
tm10
        let tm12 :: Term
tm12 = Var -> Term -> Term
Term.mkAbs Var
v9 Term
tm11
        let tm13 :: Term
tm13 = Var -> Term
Term.mkVar Var
v10
        Term
tm14 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm13 Term
tm3
        Term
tm15 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm14 Term
tm3
        let tm16 :: Term
tm16 = Var -> Term -> Term
Term.mkAbs Var
v10 Term
tm15
        Term
tm17 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm12 Term
tm16
        let tm18 :: Term
tm18 = Var -> Term -> Term
Term.mkAbs Var
v8 Term
tm17
        let tm19 :: Term
tm19 = Var -> Term -> Term
Term.mkAbs Var
v7 Term
tm18
        let tm20 :: Term
tm20 = Var -> Term
Term.mkVar Var
v5
        Term
tm21 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm19 Term
tm20
        let tm22 :: Term
tm22 = Var -> Term
Term.mkVar Var
v6
        Term
tm23 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm21 Term
tm22
        Term
tm24 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm23 Term
tm20
        let tm25 :: Term
tm25 = Var -> Term -> Term
Term.mkAbs Var
v6 Term
tm24
        let tm26 :: Term
tm26 = Var -> Term -> Term
Term.mkAbs Var
v5 Term
tm25
        let tm27 :: Term
tm27 = Var -> Term
Term.mkVar Var
v11
        let tm28 :: Term
tm28 = Var -> Term -> Term
Term.mkAbs Var
v12 Term
tm3
        Term
tm29 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm27 Term
tm28
        let tm30 :: Term
tm30 = Var -> Term -> Term
Term.mkAbs Var
v11 Term
tm29
        let tm31 :: Term
tm31 = Var -> Term
Term.mkVar Var
v0
        let tm32 :: Term
tm32 = Var -> Term
Term.mkVar Var
v13
        Term
tm33 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm31 Term
tm32
        Term
tm34 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm26 Term
tm33
        let tm35 :: Term
tm35 = Var -> Term
Term.mkVar Var
v4
        Term
tm36 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm34 Term
tm35
        let tm37 :: Term
tm37 = Var -> Term -> Term
Term.mkAbs Var
v13 Term
tm36
        Term
tm38 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm30 Term
tm37
        Term
tm39 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm26 Term
tm38
        Term
tm40 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm39 Term
tm35
        let tm41 :: Term
tm41 = Var -> Term -> Term
Term.mkAbs Var
v4 Term
tm40
        Term
tm42 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm6 Term
tm41
        let tm43 :: Term
tm43 = Var -> Term -> Term
Term.mkAbs Var
v0 Term
tm42
        let tm44 :: Term
tm44 = Var -> Term
Term.mkVar Var
v15
        let tm45 :: Term
tm45 = Var -> Term -> Term
Term.mkAbs Var
v16 Term
tm3
        Term
tm46 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm44 Term
tm45
        let tm47 :: Term
tm47 = Var -> Term -> Term
Term.mkAbs Var
v15 Term
tm46
        let tm48 :: Term
tm48 = Var -> Term
Term.mkVar Var
v14
        let tm49 :: Term
tm49 = Var -> Term
Term.mkVar Var
v17
        Term
tm50 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm48 Term
tm49
        let tm51 :: Term
tm51 = Var -> Term
Term.mkVar Var
v18
        Term
tm52 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm48 Term
tm51
        Term
tm53 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm50 Term
tm52
        Term
tm54 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm26 Term
tm53
        Term
tm55 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm49 Term
tm51
        Term
tm56 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm54 Term
tm55
        let tm57 :: Term
tm57 = Var -> Term -> Term
Term.mkAbs Var
v18 Term
tm56
        Term
tm58 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm47 Term
tm57
        let tm59 :: Term
tm59 = Var -> Term -> Term
Term.mkAbs Var
v17 Term
tm58
        Term
tm60 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm47 Term
tm59
        Term
tm61 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm19 Term
tm60
        let tm62 :: Term
tm62 = Var -> Term
Term.mkVar Var
v19
        Term
tm63 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm26 Term
tm62
        Term
tm64 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm6 Term
tm2
        Term
tm65 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm63 Term
tm64
        let tm66 :: Term
tm66 = Var -> Term -> Term
Term.mkAbs Var
v19 Term
tm65
        let tm67 :: Term
tm67 = Var -> Term
Term.mkVar Var
v21
        let tm68 :: Term
tm68 = Var -> Term
Term.mkVar Var
v23
        Term
tm69 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm67 Term
tm68
        Term
tm70 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm26 Term
tm69
        let tm71 :: Term
tm71 = Var -> Term
Term.mkVar Var
v22
        Term
tm72 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm70 Term
tm71
        let tm73 :: Term
tm73 = Var -> Term -> Term
Term.mkAbs Var
v23 Term
tm72
        Term
tm74 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm47 Term
tm73
        Term
tm75 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm26 Term
tm74
        Term
tm76 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm75 Term
tm71
        let tm77 :: Term
tm77 = Var -> Term -> Term
Term.mkAbs Var
v22 Term
tm76
        Term
tm78 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm6 Term
tm77
        let tm79 :: Term
tm79 = Var -> Term -> Term
Term.mkAbs Var
v21 Term
tm78
        let tm80 :: Term
tm80 = Var -> Term
Term.mkVar Var
v20
        let tm81 :: Term
tm81 = Var -> Term
Term.mkVar Var
v24
        Term
tm82 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm48 Term
tm81
        Term
tm83 <- Term -> Term -> Maybe Term
Term.mkEq Term
tm80 Term
tm82
        let tm84 :: Term
tm84 = Var -> Term -> Term
Term.mkAbs Var
v24 Term
tm83
        Term
tm85 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm79 Term
tm84
        let tm86 :: Term
tm86 = Var -> Term -> Term
Term.mkAbs Var
v20 Term
tm85
        Term
tm87 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm47 Term
tm86
        Term
tm88 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm66 Term
tm87
        Term
tm89 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm61 Term
tm88
        let tm90 :: Term
tm90 = Var -> Term -> Term
Term.mkAbs Var
v14 Term
tm89
        Term
tm91 <- Term -> Term -> Maybe Term
Term.mkApp Term
tm43 Term
tm90
        Term -> Maybe Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm91

standardAxioms :: Set TermAlpha
standardAxioms :: Set TermAlpha
standardAxioms =
    [TermAlpha] -> Set TermAlpha
forall a. Ord a => [a] -> Set a
Set.fromList
      [TermAlpha
axiomOfExtensionality,
       TermAlpha
axiomOfChoice,
       TermAlpha
axiomOfInfinity]

standardAxiomName :: TermAlpha -> String
standardAxiomName :: TermAlpha -> String
standardAxiomName TermAlpha
tm =
     if TermAlpha
tm TermAlpha -> TermAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== TermAlpha
axiomOfExtensionality then String
"AXIOM OF EXTENSIONALITY"
     else if TermAlpha
tm TermAlpha -> TermAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== TermAlpha
axiomOfChoice then String
"AXIOM OF CHOICE"
     else if TermAlpha
tm TermAlpha -> TermAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== TermAlpha
axiomOfInfinity then String
"AXIOM OF INFINITY"
     else ShowS
forall a. HasCallStack => String -> a
error String
"HOL.TermAlpha.standardAxiomName: not a standard axiom"