42 fun strip thm = case (prem_inclass o Thm.prop_of) thm |
41 fun strip thm = case (prem_inclass o Thm.prop_of) thm |
43 of SOME (_, class) => thm |> strip_ofclass class |> strip |
42 of SOME (_, class) => thm |> strip_ofclass class |> strip |
44 | NONE => thm; |
43 | NONE => thm; |
45 in strip end; |
44 in strip end; |
46 |
45 |
47 fun subclass_rule thy (class1, class2) = |
46 fun subclass_rule thy (sub, sup) = |
48 let |
47 let |
49 val ctxt = ProofContext.init thy; |
48 val ctxt = Locale.init sub thy; |
50 fun mk_axioms class = |
49 val ctxt_thy = ProofContext.init thy; |
51 let |
50 val params = Class.these_params thy [sup]; |
52 val params = Class.these_params thy [class]; |
51 val props = |
53 in |
52 Locale.global_asms_of thy sup |
54 Locale.global_asms_of thy class |
53 |> maps snd |
55 |> maps snd |
54 |> map (ObjectLogic.ensure_propT thy); |
56 |> (map o map_aterms) (fn Free (v, _) => (Const o the o AList.lookup (op =) params) v | t => t) |
55 fun tac { prems, context } = |
57 |> (map o map_types o map_atyps) (fn TFree _ => TFree (Name.aT, [class1]) | ty => ty) |
56 Locale.intro_locales_tac true context prems |
58 |> map (ObjectLogic.ensure_propT thy) |
57 ORELSE ALLGOALS assume_tac; |
59 end; |
|
60 val (prems, concls) = pairself mk_axioms (class1, class2); |
|
61 in |
58 in |
62 Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls) |
59 Goal.prove_multi ctxt [] [] props tac |
63 (Locale.intro_locales_tac true ctxt) |
60 |> map (Assumption.export false ctxt ctxt_thy) |
|
61 |> Variable.export ctxt ctxt_thy |
64 end; |
62 end; |
|
63 |
|
64 fun prove_single_subclass (sub, sup) thms ctxt thy = |
|
65 let |
|
66 val ctxt_thy = ProofContext.init thy; |
|
67 val subclass_rule = Conjunction.intr_balanced thms |
|
68 |> Assumption.export false ctxt ctxt_thy |
|
69 |> singleton (Variable.export ctxt ctxt_thy); |
|
70 val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub])); |
|
71 val sub_ax = #axioms (AxClass.get_info thy sub); |
|
72 val classrel = |
|
73 #intro (AxClass.get_info thy sup) |
|
74 |> Drule.instantiate' [SOME sub_inst] [] |
|
75 |> OF_LAST (subclass_rule OF sub_ax) |
|
76 |> strip_all_ofclass thy (Sign.super_classes thy sup) |
|
77 |> Thm.strip_shyps |
|
78 in |
|
79 thy |
|
80 |> AxClass.add_classrel classrel |
|
81 |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac thms)) |
|
82 I (sub, Locale.Locale sup) |
|
83 end; |
|
84 |
|
85 fun prove_subclass (sub, sup) thms ctxt thy = |
|
86 let |
|
87 val supclasses = Sign.complete_sort thy [sup] |
|
88 |> filter_out (fn class => Sign.subsort thy ([sub], [class])); |
|
89 fun transform sup' = subclass_rule thy (sup, sup') |> map (fn thm => thm OF thms); |
|
90 in |
|
91 thy |
|
92 |> fold_rev (fn sup' => prove_single_subclass (sub, sup') |
|
93 (transform sup') ctxt) supclasses |
|
94 end; |
65 |
95 |
66 |
96 |
67 (** subclassing **) |
97 (** subclassing **) |
68 |
98 |
69 local |
99 local |
70 |
100 |
71 fun gen_subclass prep_class do_proof raw_sup lthy = |
101 fun gen_subclass prep_class do_proof raw_sup lthy = |
72 let |
102 let |
|
103 (*FIXME make more use of local context; drop redundancies*) |
73 val ctxt = LocalTheory.target_of lthy; |
104 val ctxt = LocalTheory.target_of lthy; |
74 val thy = ProofContext.theory_of ctxt; |
105 val thy = ProofContext.theory_of ctxt; |
75 val ctxt_thy = ProofContext.init thy; |
|
76 val sup = prep_class thy raw_sup; |
106 val sup = prep_class thy raw_sup; |
77 val sub = case TheoryTarget.peek lthy |
107 val sub = case TheoryTarget.peek lthy |
78 of {is_class = false, ...} => error "No class context" |
108 of {is_class = false, ...} => error "No class context" |
79 | {target, ...} => target; |
109 | {target, ...} => target; |
80 val sub_params = map fst (Class.these_params thy [sub]); |
110 val sub_params = map fst (Class.these_params thy [sub]); |
85 commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); |
115 commas_quote err_params ^ " of " ^ Sign.string_of_sort thy [sup]); |
86 val sublocale_prop = |
116 val sublocale_prop = |
87 Locale.global_asms_of thy sup |
117 Locale.global_asms_of thy sup |
88 |> maps snd |
118 |> maps snd |
89 |> map (ObjectLogic.ensure_propT thy); |
119 |> map (ObjectLogic.ensure_propT thy); |
90 val supclasses = Sign.complete_sort thy [sup] |
|
91 |> filter_out (fn class => Sign.subsort thy ([sub], [class])); |
|
92 val supclasses' = remove (op =) sup supclasses; |
|
93 val _ = if null supclasses' then () else |
|
94 error ("The following superclasses of " ^ sup |
|
95 ^ " are no superclass of " ^ sub ^ ": " |
|
96 ^ commas supclasses'); |
|
97 (*FIXME*) |
|
98 val sub_ax = #axioms (AxClass.get_info thy sub); |
|
99 val sub_inst = Thm.ctyp_of thy (TVar ((Name.aT, 0), [sub])); |
|
100 fun prove_classrel subclass_rule = |
|
101 let |
|
102 fun add_classrel sup' thy = |
|
103 let |
|
104 val classrel = |
|
105 #intro (AxClass.get_info thy sup') |
|
106 |> Drule.instantiate' [SOME sub_inst] [] |
|
107 |> OF_LAST (subclass_rule OF sub_ax) |
|
108 |> strip_all_ofclass thy (Sign.super_classes thy sup'); |
|
109 in |
|
110 AxClass.add_classrel classrel thy |
|
111 end; |
|
112 in |
|
113 fold_rev add_classrel supclasses |
|
114 end; |
|
115 fun prove_interpretation sublocale_rule = |
|
116 prove_interpretation_in (ProofContext.fact_tac [sublocale_rule] 1) |
|
117 I (sub, Locale.Locale sup) |
|
118 fun after_qed thms = |
120 fun after_qed thms = |
119 let |
121 LocalTheory.theory (prove_subclass (sub, sup) thms ctxt) |
120 val sublocale_rule = Conjunction.intr_balanced thms; |
122 (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*); |
121 val subclass_rule = sublocale_rule |
|
122 |> Assumption.export false ctxt ctxt_thy |
|
123 |> singleton (Variable.export ctxt ctxt_thy); |
|
124 in |
|
125 LocalTheory.theory (prove_classrel subclass_rule |
|
126 #> prove_interpretation sublocale_rule) |
|
127 (*#> (fn lthy => LocalTheory.reinit lthy thy) FIXME does not work as expected*) |
|
128 end; |
|
129 in |
123 in |
130 do_proof after_qed sublocale_prop lthy |
124 do_proof after_qed sublocale_prop lthy |
131 end; |
125 end; |
132 |
126 |
133 fun user_proof after_qed props = |
127 fun user_proof after_qed props = |