src/Cube/Cube.ML
changeset 3771 ede66fb99880
parent 420 1e0f1973536d
child 3884 5423e06b9fe6
equal deleted inserted replaced
3770:294b5905f4eb 3771:ede66fb99880
    10 
    10 
    11 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
    11 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
    12 
    12 
    13 val L2_thy =
    13 val L2_thy =
    14   Cube.thy
    14   Cube.thy
    15   |> add_axioms
    15   |> Theory.add_axioms
    16    [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
    16    [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
    17     ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
    17     ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
    18      \  ==> Abs(A,f) : Prod(A,B)")]
    18      \  ==> Abs(A,f) : Prod(A,B)")]
    19   |> add_thyname "L2";
    19   |> Theory.add_name "L2";
    20 
    20 
    21 val lam_bs = get_axiom L2_thy "lam_bs";
    21 val lam_bs = get_axiom L2_thy "lam_bs";
    22 val pi_bs = get_axiom L2_thy "pi_bs";
    22 val pi_bs = get_axiom L2_thy "pi_bs";
    23 
    23 
    24 val L2 = simple @ [lam_bs,pi_bs];
    24 val L2 = simple @ [lam_bs,pi_bs];
    25 
    25 
    26 val Lomega_thy =
    26 val Lomega_thy =
    27   Cube.thy
    27   Cube.thy
    28   |> add_axioms
    28   |> Theory.add_axioms
    29    [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    29    [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    30     ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    30     ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    31      \  ==> Abs(A,f) : Prod(A,B)")]
    31      \  ==> Abs(A,f) : Prod(A,B)")]
    32   |> add_thyname "Lomega";
    32   |> Theory.add_name "Lomega";
    33 
    33 
    34 val lam_bb = get_axiom Lomega_thy "lam_bb";
    34 val lam_bb = get_axiom Lomega_thy "lam_bb";
    35 val pi_bb = get_axiom Lomega_thy "pi_bb";
    35 val pi_bb = get_axiom Lomega_thy "pi_bb";
    36 val Lomega = simple @ [lam_bb,pi_bb];
    36 val Lomega = simple @ [lam_bb,pi_bb];
    37 
    37 
    38 val LOmega_thy = merge_theories(L2_thy,Lomega_thy);
    38 val LOmega_thy = merge_theories(L2_thy,Lomega_thy);
    39 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
    39 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
    40 
    40 
    41 val LP_thy =
    41 val LP_thy =
    42   Cube.thy
    42   Cube.thy
    43   |> add_axioms
    43   |> Theory.add_axioms
    44    [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    44    [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
    45     ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    45     ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
    46      \  ==> Abs(A,f) : Prod(A,B)")]
    46      \  ==> Abs(A,f) : Prod(A,B)")]
    47   |> add_thyname "LP";
    47   |> Theory.add_name "LP";
    48 
    48 
    49 val lam_sb = get_axiom LP_thy "lam_sb";
    49 val lam_sb = get_axiom LP_thy "lam_sb";
    50 val pi_sb = get_axiom LP_thy "pi_sb";
    50 val pi_sb = get_axiom LP_thy "pi_sb";
    51 val LP = simple @ [lam_sb,pi_sb];
    51 val LP = simple @ [lam_sb,pi_sb];
    52 
    52