12 val judgment_name: theory -> string |
12 val judgment_name: theory -> string |
13 val is_judgment: theory -> term -> bool |
13 val is_judgment: theory -> term -> bool |
14 val drop_judgment: theory -> term -> term |
14 val drop_judgment: theory -> term -> term |
15 val fixed_judgment: theory -> string -> term |
15 val fixed_judgment: theory -> string -> term |
16 val ensure_propT: theory -> term -> term |
16 val ensure_propT: theory -> term -> term |
|
17 val dest_judgment: cterm -> cterm |
17 val judgment_conv: conv -> conv |
18 val judgment_conv: conv -> conv |
18 val is_elim: thm -> bool |
19 val is_elim: thm -> bool |
19 val declare_atomize: attribute |
20 val declare_atomize: attribute |
20 val declare_rulify: attribute |
21 val declare_rulify: attribute |
21 val atomize_term: theory -> term -> term |
22 val atomize_term: theory -> term -> term |
44 val empty = (NONE, ([], [])); |
45 val empty = (NONE, ([], [])); |
45 val copy = I; |
46 val copy = I; |
46 val extend = I; |
47 val extend = I; |
47 |
48 |
48 fun merge_judgment (SOME x, SOME y) = |
49 fun merge_judgment (SOME x, SOME y) = |
49 if x = y then SOME x else error "Attempt to merge different object-logics" |
50 if (x: string) = y then SOME x else error "Attempt to merge different object-logics" |
50 | merge_judgment (j1, j2) = if is_some j1 then j1 else j2; |
51 | merge_judgment (j1, j2) = if is_some j1 then j1 else j2; |
51 |
52 |
52 fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = |
53 fun merge _ ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = |
53 (merge_judgment (judgment1, judgment2), |
54 (merge_judgment (judgment1, judgment2), |
54 (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); |
55 (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); |
108 |
109 |
109 fun ensure_propT thy t = |
110 fun ensure_propT thy t = |
110 let val T = Term.fastype_of t |
111 let val T = Term.fastype_of t |
111 in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end; |
112 in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end; |
112 |
113 |
|
114 fun dest_judgment ct = |
|
115 if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct) |
|
116 then Thm.dest_arg ct |
|
117 else raise CTERM ("dest_judgment", [ct]); |
|
118 |
113 fun judgment_conv cv ct = |
119 fun judgment_conv cv ct = |
114 if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct) |
120 if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct) |
115 then Conv.arg_conv cv ct |
121 then Conv.arg_conv cv ct |
116 else raise CTERM ("judgment_conv", [ct]); |
122 else raise CTERM ("judgment_conv", [ct]); |
117 |
123 |
146 |
152 |
147 |
153 |
148 (* atomize *) |
154 (* atomize *) |
149 |
155 |
150 fun rewrite_prems_tac rews = |
156 fun rewrite_prems_tac rews = |
151 CONVERSION (Conv.forall_conv ~1 (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true rews)))); |
157 CONVERSION (Conv.forall_conv ~1 (Conv.prems_conv ~1 (MetaSimplifier.rewrite true rews))); |
152 |
158 |
153 fun atomize_term thy = |
159 fun atomize_term thy = |
154 drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; |
160 drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; |
155 |
161 |
156 fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; |
162 fun atomize_cterm ct = MetaSimplifier.rewrite true (get_atomize (Thm.theory_of_cterm ct)) ct; |