equal
deleted
inserted
replaced
106 val transitive: term -> typ -> proof -> proof -> proof |
106 val transitive: term -> typ -> proof -> proof -> proof |
107 val abstract_rule: term -> string -> proof -> proof |
107 val abstract_rule: term -> string -> proof -> proof |
108 val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof |
108 val combination: term -> term -> term -> term -> typ -> proof -> proof -> proof |
109 val equal_intr: term -> term -> proof -> proof -> proof |
109 val equal_intr: term -> term -> proof -> proof -> proof |
110 val equal_elim: term -> term -> proof -> proof -> proof |
110 val equal_elim: term -> term -> proof -> proof -> proof |
|
111 val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list -> |
|
112 sort list -> proof -> proof |
111 val axm_proof: string -> term -> proof |
113 val axm_proof: string -> term -> proof |
112 val oracle_proof: string -> term -> oracle * proof |
114 val oracle_proof: string -> term -> oracle * proof |
113 val promise_proof: theory -> serial -> term -> proof |
115 val promise_proof: theory -> serial -> term -> proof |
114 val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body |
116 val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body |
115 val thm_proof: theory -> string -> term list -> term -> |
117 val thm_proof: theory -> string -> term list -> term -> |
880 fun equal_intr A B prf1 prf2 = |
882 fun equal_intr A B prf1 prf2 = |
881 equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; |
883 equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; |
882 |
884 |
883 fun equal_elim A B prf1 prf2 = |
885 fun equal_elim A B prf1 prf2 = |
884 equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; |
886 equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; |
|
887 |
|
888 |
|
889 (**** sort hypotheses ****) |
|
890 |
|
891 fun strip_shyps_proof algebra present witnessed extra_sorts prf = |
|
892 let |
|
893 fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; |
|
894 val extra = map (fn S => (TFree (Name.aT, S), S)) extra_sorts; |
|
895 val replacements = present @ extra @ witnessed; |
|
896 fun replace T = |
|
897 if exists (fn (T', _) => T' = T) present then raise Same.SAME |
|
898 else |
|
899 (case get_first (get (Type.sort_of_atyp T)) replacements of |
|
900 SOME T' => T' |
|
901 | NONE => raise Fail "strip_shyps_proof: bad type variable in proof term"); |
|
902 in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end; |
885 |
903 |
886 |
904 |
887 (***** axioms and theorems *****) |
905 (***** axioms and theorems *****) |
888 |
906 |
889 val proofs = Unsynchronized.ref 2; |
907 val proofs = Unsynchronized.ref 2; |