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
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
mk :: Term -> TermAlpha
mk :: Term -> TermAlpha
mk = Term -> TermAlpha
TermAlpha
dest :: TermAlpha -> Term
dest :: TermAlpha -> Term
dest (TermAlpha Term
tm) = Term
tm
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
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
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
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
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
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'
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"