68 ags: thm list, |
68 ags: thm list, |
69 case_hyp : thm} |
69 case_hyp : thm} |
70 |
70 |
71 |
71 |
72 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = |
72 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = |
73 ClauseContext { ctxt = ProofContext.transfer thy ctxt, |
73 ClauseContext { ctxt = Proof_Context.transfer thy ctxt, |
74 qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } |
74 qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } |
75 |
75 |
76 |
76 |
77 datatype clause_info = ClauseInfo of |
77 datatype clause_info = ClauseInfo of |
78 {no: int, |
78 {no: int, |
200 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = |
200 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = |
201 let |
201 let |
202 val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |
202 val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |
203 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
203 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
204 |
204 |
205 val thy = ProofContext.theory_of ctxt' |
205 val thy = Proof_Context.theory_of ctxt' |
206 |
206 |
207 fun inst t = subst_bounds (rev qs, t) |
207 fun inst t = subst_bounds (rev qs, t) |
208 val gs = map inst pre_gs |
208 val gs = map inst pre_gs |
209 val lhs = inst pre_lhs |
209 val lhs = inst pre_lhs |
210 val rhs = inst pre_rhs |
210 val rhs = inst pre_rhs |
238 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = |
238 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = |
239 let |
239 let |
240 val Globals {h, ...} = globals |
240 val Globals {h, ...} = globals |
241 |
241 |
242 val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata |
242 val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata |
243 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
243 val cert = Thm.cterm_of (Proof_Context.theory_of ctxt) |
244 |
244 |
245 (* Instantiate the GIntro thm with "f" and import into the clause context. *) |
245 (* Instantiate the GIntro thm with "f" and import into the clause context. *) |
246 val lGI = GIntro_thm |
246 val lGI = GIntro_thm |
247 |> Thm.forall_elim (cert f) |
247 |> Thm.forall_elim (cert f) |
248 |> fold Thm.forall_elim cqs |
248 |> fold Thm.forall_elim cqs |
258 |
258 |
259 val h_assum = |
259 val h_assum = |
260 HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |
260 HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |
261 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
261 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
262 |> fold_rev (Logic.all o Free) rcfix |
262 |> fold_rev (Logic.all o Free) rcfix |
263 |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] |
263 |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] [] |
264 |> abstract_over_list (rev qs) |
264 |> abstract_over_list (rev qs) |
265 in |
265 in |
266 RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} |
266 RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} |
267 end |
267 end |
268 |
268 |
530 |
530 |
531 (* nominal *) |
531 (* nominal *) |
532 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = |
532 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim G_eqvt invariant f_def = |
533 let |
533 let |
534 val Globals {h, domT, ranT, x, ...} = globals |
534 val Globals {h, domT, ranT, x, ...} = globals |
535 val thy = ProofContext.theory_of ctxt |
535 val thy = Proof_Context.theory_of ctxt |
536 |
536 |
537 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
537 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
538 val ihyp = Term.all domT $ Abs ("z", domT, |
538 val ihyp = Term.all domT $ Abs ("z", domT, |
539 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
539 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
540 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
540 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
603 [] (* no parameters *) |
603 [] (* no parameters *) |
604 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
604 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
605 [] (* no special monos *) |
605 [] (* no special monos *) |
606 ||> Local_Theory.restore_naming lthy |
606 ||> Local_Theory.restore_naming lthy |
607 |
607 |
608 val cert = cterm_of (ProofContext.theory_of lthy) |
608 val cert = cterm_of (Proof_Context.theory_of lthy) |
609 fun requantify orig_intro thm = |
609 fun requantify orig_intro thm = |
610 let |
610 let |
611 val (qs, t) = dest_all_all orig_intro |
611 val (qs, t) = dest_all_all orig_intro |
612 val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) |
612 val frees = Variable.add_frees lthy t [] |> remove (op =) (Binding.name_of R, T) |
613 val vars = Term.add_vars (prop_of thm) [] |
613 val vars = Term.add_vars (prop_of thm) [] |
850 |
850 |
851 |
851 |
852 (* FIXME: broken by design *) |
852 (* FIXME: broken by design *) |
853 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
853 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
854 let |
854 let |
855 val thy = ProofContext.theory_of ctxt |
855 val thy = Proof_Context.theory_of ctxt |
856 val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, |
856 val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, |
857 qglr = (oqs, _, _, _), ...} = clause |
857 qglr = (oqs, _, _, _), ...} = clause |
858 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
858 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
859 |> fold_rev (curry Logic.mk_implies) gs |
859 |> fold_rev (curry Logic.mk_implies) gs |
860 |> cterm_of thy |
860 |> cterm_of thy |
1012 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
1012 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
1013 |
1013 |
1014 val ((f, (_, f_defthm)), lthy) = |
1014 val ((f, (_, f_defthm)), lthy) = |
1015 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
1015 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
1016 |
1016 |
1017 val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
1017 val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss |
1018 val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
1018 val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees |
1019 |
1019 |
1020 val ((R, RIntro_thmss, R_elim), lthy) = |
1020 val ((R, RIntro_thmss, R_elim), lthy) = |
1021 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
1021 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
1022 |
1022 |
1023 val (_, lthy) = |
1023 val (_, lthy) = |
1024 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
1024 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
1025 |
1025 |
1026 val newthy = ProofContext.theory_of lthy |
1026 val newthy = Proof_Context.theory_of lthy |
1027 val clauses = map (transfer_clause_ctx newthy) clauses |
1027 val clauses = map (transfer_clause_ctx newthy) clauses |
1028 |
1028 |
1029 val cert = cterm_of (ProofContext.theory_of lthy) |
1029 val cert = cterm_of (Proof_Context.theory_of lthy) |
1030 |
1030 |
1031 val xclauses = PROFILE "xclauses" |
1031 val xclauses = PROFILE "xclauses" |
1032 (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees |
1032 (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees |
1033 RCss GIntro_thms) RIntro_thmss |
1033 RCss GIntro_thms) RIntro_thmss |
1034 |
1034 |