40 structure ObjectLogicDataArgs = |
40 structure ObjectLogicDataArgs = |
41 struct |
41 struct |
42 val name = "Pure/object-logic"; |
42 val name = "Pure/object-logic"; |
43 type T = string option * (thm list * thm list); |
43 type T = string option * (thm list * thm list); |
44 |
44 |
45 val empty = (None, ([], [Drule.norm_hhf_eq])); |
45 val empty = (NONE, ([], [Drule.norm_hhf_eq])); |
46 val copy = I; |
46 val copy = I; |
47 val prep_ext = I; |
47 val prep_ext = I; |
48 |
48 |
49 fun merge_judgment (Some x, Some y) = |
49 fun merge_judgment (SOME x, SOME y) = |
50 if x = y then Some x else error "Attempt to merge different object-logics" |
50 if x = y then SOME x else error "Attempt to merge different object-logics" |
51 | 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; |
52 |
52 |
53 fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = |
53 fun merge ((judgment1, (atomize1, rulify1)), (judgment2, (atomize2, rulify2))) = |
54 (merge_judgment (judgment1, judgment2), |
54 (merge_judgment (judgment1, judgment2), |
55 (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); |
55 (Drule.merge_rules (atomize1, atomize2), Drule.merge_rules (rulify1, rulify2))); |
64 |
64 |
65 (* add_judgment(_i) *) |
65 (* add_judgment(_i) *) |
66 |
66 |
67 local |
67 local |
68 |
68 |
69 fun new_judgment name (None, rules) = (Some name, rules) |
69 fun new_judgment name (NONE, rules) = (SOME name, rules) |
70 | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment"; |
70 | new_judgment _ (SOME _, _) = error "Attempt to redeclare object-logic judgment"; |
71 |
71 |
72 fun add_final name thy = |
72 fun add_final name thy = |
73 let |
73 let |
74 val typ = case Sign.const_type (sign_of thy) name of |
74 val typ = case Sign.const_type (sign_of thy) name of |
75 Some T => T |
75 SOME T => T |
76 | None => error "Internal error in ObjectLogic.gen_add_judgment"; |
76 | NONE => error "Internal error in ObjectLogic.gen_add_judgment"; |
77 in |
77 in |
78 Theory.add_finals_i false [Const(name,typ)] thy |
78 Theory.add_finals_i false [Const(name,typ)] thy |
79 end; |
79 end; |
80 |
80 |
81 fun gen_add_judgment add_consts (name, T, syn) thy = |
81 fun gen_add_judgment add_consts (name, T, syn) thy = |
98 |
98 |
99 (* term operations *) |
99 (* term operations *) |
100 |
100 |
101 fun judgment_name sg = |
101 fun judgment_name sg = |
102 (case ObjectLogicData.get_sg sg of |
102 (case ObjectLogicData.get_sg sg of |
103 (Some name, _) => name |
103 (SOME name, _) => name |
104 | _ => raise TERM ("Unknown object-logic judgment", [])); |
104 | _ => raise TERM ("Unknown object-logic judgment", [])); |
105 |
105 |
106 fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg |
106 fun is_judgment sg (Const (c, _) $ _) = c = judgment_name sg |
107 | is_judgment _ _ = false; |
107 | is_judgment _ _ = false; |
108 |
108 |
164 |
164 |
165 fun full_atomize_tac i st = |
165 fun full_atomize_tac i st = |
166 rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st; |
166 rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st; |
167 |
167 |
168 fun atomize_goal i st = |
168 fun atomize_goal i st = |
169 (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st'); |
169 (case Seq.pull (atomize_tac i st) of NONE => st | SOME (st', _) => st'); |
170 |
170 |
171 |
171 |
172 (* rulify *) |
172 (* rulify *) |
173 |
173 |
174 fun gen_rulify full thm = |
174 fun gen_rulify full thm = |