equal
deleted
inserted
replaced
1 theory Rsp |
1 theory Rsp |
2 imports Abs Tacs |
2 imports Abs Tacs |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 fun const_rsp lthy const = |
6 fun const_rsp qtys lthy const = |
7 let |
7 let |
8 val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy) |
8 val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy) |
9 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
9 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
10 in |
10 in |
11 HOLogic.mk_Trueprop (rel $ const $ const) |
11 HOLogic.mk_Trueprop (rel $ const $ const) |
12 end |
12 end |
13 *} |
13 *} |
37 | SOME th => prepare_goal (term_of (cprem_of th 1)) |
37 | SOME th => prepare_goal (term_of (cprem_of th 1)) |
38 end |
38 end |
39 *} |
39 *} |
40 |
40 |
41 ML {* |
41 ML {* |
42 fun prove_const_rsp bind consts tac ctxt = |
42 fun prove_const_rsp qtys bind consts tac ctxt = |
43 let |
43 let |
44 val rsp_goals = map (const_rsp ctxt) consts |
44 val rsp_goals = map (const_rsp qtys ctxt) consts |
45 val thy = ProofContext.theory_of ctxt |
45 val thy = ProofContext.theory_of ctxt |
46 val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals) |
46 val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals) |
47 val fixed' = distinct (op =) (flat fixed) |
47 val fixed' = distinct (op =) (flat fixed) |
48 val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
48 val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals) |
49 val user_thm = Goal.prove ctxt fixed' [] user_goal tac |
49 val user_thm = Goal.prove ctxt fixed' [] user_goal tac |