34 fun mk_inv_into T U = |
31 fun mk_inv_into T U = |
35 Const (@{const_name inv_into}, [T --> B, T --> U, U] ---> T) |
32 Const (@{const_name inv_into}, [T --> B, T --> U, U] ---> T) |
36 |
33 |
37 fun mk_inv_of ctxt ct = |
34 fun mk_inv_of ctxt ct = |
38 let |
35 let |
39 val (dT, rT) = Term.dest_funT (U.typ_of ct) |
36 val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct) |
40 val inv = U.certify ctxt (mk_inv_into dT rT) |
37 val inv = SMT_Utils.certify ctxt (mk_inv_into dT rT) |
41 val univ = U.certify ctxt (mk_univ dT) |
38 val univ = SMT_Utils.certify ctxt (mk_univ dT) |
42 in Thm.mk_binop inv univ ct end |
39 in Thm.mk_binop inv univ ct end |
43 |
40 |
44 fun mk_inj_prop ctxt ct = |
41 fun mk_inj_prop ctxt ct = |
45 let |
42 let |
46 val (dT, rT) = Term.dest_funT (U.typ_of ct) |
43 val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct) |
47 val inj = U.certify ctxt (mk_inj_on dT rT) |
44 val inj = SMT_Utils.certify ctxt (mk_inj_on dT rT) |
48 val univ = U.certify ctxt (mk_univ dT) |
45 val univ = SMT_Utils.certify ctxt (mk_univ dT) |
49 in U.mk_cprop (Thm.mk_binop inj ct univ) end |
46 in SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end |
50 |
47 |
51 |
48 |
52 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
49 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast} |
53 |
50 |
54 fun prove_inj_prop ctxt def lhs = |
51 fun prove_inj_prop ctxt def lhs = |
55 let |
52 let |
56 val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt |
53 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
57 val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)] |
54 val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)] |
58 in |
55 in |
59 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
56 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
60 |> apply (Tactic.rtac @{thm injI}) |
57 |> apply (Tactic.rtac @{thm injI}) |
61 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
58 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
62 |> Goal.norm_result o Goal.finish ctxt' |
59 |> Goal.norm_result o Goal.finish ctxt' |
63 |> singleton (Variable.export ctxt' ctxt) |
60 |> singleton (Variable.export ctxt' ctxt) |
64 end |
61 end |
65 |
62 |
66 fun prove_rhs ctxt def lhs = |
63 fun prove_rhs ctxt def lhs = |
67 T.by_tac ( |
64 Z3_Proof_Tools.by_tac ( |
68 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
65 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
69 THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI}) |
66 THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI}) |
70 THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #> |
67 THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #> |
71 Thm.elim_implies def |
68 Thm.elim_implies def |
72 |
69 |
80 in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end |
77 in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end |
81 |
78 |
82 fun prove_lhs ctxt rhs = |
79 fun prove_lhs ctxt rhs = |
83 let |
80 let |
84 val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs))) |
81 val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs))) |
|
82 val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt |
85 in |
83 in |
86 T.by_tac ( |
84 Z3_Proof_Tools.by_tac ( |
87 CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt)) |
85 CONVERSION (SMT_Utils.prop_conv conv) |
88 THEN' Simplifier.simp_tac HOL_ss) |
86 THEN' Simplifier.simp_tac HOL_ss) |
89 end |
87 end |
90 |
88 |
91 |
89 |
92 fun mk_inv_def ctxt rhs = |
90 fun mk_inv_def ctxt rhs = |
93 let |
91 let |
94 val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt |
92 val (ct, ctxt') = |
|
93 SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt |
95 val (cl, cv) = Thm.dest_binop ct |
94 val (cl, cv) = Thm.dest_binop ct |
96 val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last |
95 val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last |
97 val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf)) |
96 val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf)) |
98 in Thm.assume (U.mk_cequals cg cu) end |
97 in Thm.assume (SMT_Utils.mk_cequals cg cu) end |
99 |
98 |
100 fun prove_inj_eq ctxt ct = |
99 fun prove_inj_eq ctxt ct = |
101 let |
100 let |
102 val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct)) |
101 val (lhs, rhs) = |
|
102 pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct)) |
103 val lhs_thm = prove_lhs ctxt rhs lhs |
103 val lhs_thm = prove_lhs ctxt rhs lhs |
104 val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs |
104 val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs |
105 in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end |
105 in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end |
106 |
106 |
107 |
107 |
108 val swap_eq_thm = mk_meta_eq @{thm eq_commute} |
108 val swap_eq_thm = mk_meta_eq @{thm eq_commute} |
109 val swap_disj_thm = mk_meta_eq @{thm disj_commute} |
109 val swap_disj_thm = mk_meta_eq @{thm disj_commute} |
110 |
110 |
111 fun swap_conv dest eq = |
111 fun swap_conv dest eq = |
112 U.if_true_conv ((op <) o pairself Term.size_of_term o dest) |
112 SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest) |
113 (Conv.rewr_conv eq) |
113 (Conv.rewr_conv eq) |
114 |
114 |
115 val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm |
115 val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm |
116 val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm |
116 val swap_disj_conv = swap_conv SMT_Utils.dest_disj swap_disj_thm |
117 |
117 |
118 fun norm_conv ctxt = |
118 fun norm_conv ctxt = |
119 swap_eq_conv then_conv |
119 swap_eq_conv then_conv |
120 Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv |
120 Conv.arg1_conv (SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv |
121 Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt) |
121 Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt) |
122 |
122 |
123 in |
123 in |
124 |
124 |
125 fun prove_injectivity ctxt = |
125 fun prove_injectivity ctxt = |
126 T.by_tac ( |
126 Z3_Proof_Tools.by_tac ( |
127 CONVERSION (U.prop_conv (norm_conv ctxt)) |
127 CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt)) |
128 THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt))) |
128 THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt))) |
129 |
129 |
130 end |
130 end |
131 |
131 |
132 end |
132 end |