src/Cube/Cube.ML
 changeset 3771 ede66fb99880 parent 420 1e0f1973536d child 3884 5423e06b9fe6
equal 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 `