35 (** constants for theorems and axioms **) |
35 (** constants for theorems and axioms **) |
36 |
36 |
37 fun add_proof_atom_consts names thy = |
37 fun add_proof_atom_consts names thy = |
38 thy |
38 thy |
39 |> Sign.absolute_path |
39 |> Sign.absolute_path |
40 |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names); |
40 |> Sign.add_consts_i (map (fn name => (Binding.name name, proofT, NoSyn)) names); |
41 |
41 |
42 (** constants for application and abstraction **) |
42 (** constants for application and abstraction **) |
43 |
43 |
44 fun add_proof_syntax thy = |
44 fun add_proof_syntax thy = |
45 thy |
45 thy |
46 |> Theory.copy |
46 |> Theory.copy |
47 |> Sign.root_path |
47 |> Sign.root_path |
48 |> Sign.add_defsort_i [] |
48 |> Sign.add_defsort_i [] |
49 |> Sign.add_types [("proof", 0, NoSyn)] |
49 |> Sign.add_types [(Binding.name "proof", 0, NoSyn)] |
50 |> Sign.add_consts_i |
50 |> Sign.add_consts_i |
51 [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), |
51 [(Binding.name "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)), |
52 ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), |
52 (Binding.name "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)), |
53 ("Abst", (aT --> proofT) --> proofT, NoSyn), |
53 (Binding.name "Abst", (aT --> proofT) --> proofT, NoSyn), |
54 ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), |
54 (Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn), |
55 ("Hyp", propT --> proofT, NoSyn), |
55 (Binding.name "Hyp", propT --> proofT, NoSyn), |
56 ("Oracle", propT --> proofT, NoSyn), |
56 (Binding.name "Oracle", propT --> proofT, NoSyn), |
57 ("MinProof", proofT, Delimfix "?")] |
57 (Binding.name "MinProof", proofT, Delimfix "?")] |
58 |> Sign.add_nonterminals ["param", "params"] |
58 |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"] |
59 |> Sign.add_syntax_i |
59 |> Sign.add_syntax_i |
60 [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), |
60 [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), |
61 ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
61 ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
62 ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
62 ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), |
63 ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)), |
63 ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)), |