69 let |
69 let |
70 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
70 val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt |
71 val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)] |
71 val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)] |
72 in |
72 in |
73 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
73 Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct)) |
74 |> apply (Tactic.rtac @{thm injI}) |
74 |> apply (rtac @{thm injI}) |
75 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
75 |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}]) |
76 |> Goal.norm_result o Goal.finish ctxt' |
76 |> Goal.norm_result o Goal.finish ctxt' |
77 |> singleton (Variable.export ctxt' ctxt) |
77 |> singleton (Variable.export ctxt' ctxt) |
78 end |
78 end |
79 |
79 |
80 fun prove_rhs ctxt def lhs = |
80 fun prove_rhs ctxt def lhs = |
81 Z3_Proof_Tools.by_tac ( |
81 Z3_Proof_Tools.by_tac ( |
82 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
82 CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt) |
83 THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI}) |
83 THEN' REPEAT_ALL_NEW (match_tac @{thms allI}) |
84 THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) |
84 THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) |
85 |
85 |
86 |
86 |
87 fun expand thm ct = |
87 fun expand thm ct = |
88 let |
88 let |
89 val cpat = Thm.dest_arg (Thm.rhs_of thm) |
89 val cpat = Thm.dest_arg (Thm.rhs_of thm) |