51 if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT) |
51 if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT) |
52 (descr ~~ pnames); |
52 (descr ~~ pnames); |
53 |
53 |
54 fun make_pred i T U r x = |
54 fun make_pred i T U r x = |
55 if i mem is then |
55 if i mem is then |
56 Free (nth_elem (i, pnames), T --> U --> HOLogic.boolT) $ r $ x |
56 Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x |
57 else Free (nth_elem (i, pnames), U --> HOLogic.boolT) $ x; |
57 else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x; |
58 |
58 |
59 fun mk_all i s T t = |
59 fun mk_all i s T t = |
60 if i mem is then list_all_free ([(s, T)], t) else t; |
60 if i mem is then list_all_free ([(s, T)], t) else t; |
61 |
61 |
62 val (prems, rec_fns) = split_list (flat (snd (foldl_map |
62 val (prems, rec_fns) = split_list (List.concat (snd (foldl_map |
63 (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) => |
63 (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) => |
64 let |
64 let |
65 val Ts = map (typ_of_dtyp descr sorts) cargs; |
65 val Ts = map (typ_of_dtyp descr sorts) cargs; |
66 val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames); |
66 val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames); |
67 val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); |
67 val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); |
68 val frees = tnames ~~ Ts; |
68 val frees = tnames ~~ Ts; |
69 |
69 |
70 fun mk_prems vs [] = |
70 fun mk_prems vs [] = |
71 let |
71 let |
72 val rT = nth_elem (i, rec_result_Ts); |
72 val rT = List.nth (rec_result_Ts, i); |
73 val vs' = filter_out is_unit vs; |
73 val vs' = filter_out is_unit vs; |
74 val f = mk_Free "f" (map fastype_of vs' ---> rT) j; |
74 val f = mk_Free "f" (map fastype_of vs' ---> rT) j; |
75 val f' = Pattern.eta_contract (list_abs_free |
75 val f' = Pattern.eta_contract (list_abs_free |
76 (map dest_Free vs, if i mem is then list_comb (f, vs') |
76 (map dest_Free vs, if i mem is then list_comb (f, vs') |
77 else HOLogic.unit)); |
77 else HOLogic.unit)); |
81 | mk_prems vs (((dt, s), T) :: ds) = |
81 | mk_prems vs (((dt, s), T) :: ds) = |
82 let |
82 let |
83 val k = body_index dt; |
83 val k = body_index dt; |
84 val (Us, U) = strip_type T; |
84 val (Us, U) = strip_type T; |
85 val i = length Us; |
85 val i = length Us; |
86 val rT = nth_elem (k, rec_result_Ts); |
86 val rT = List.nth (rec_result_Ts, k); |
87 val r = Free ("r" ^ s, Us ---> rT); |
87 val r = Free ("r" ^ s, Us ---> rT); |
88 val (p, f) = mk_prems (vs @ [r]) ds |
88 val (p, f) = mk_prems (vs @ [r]) ds |
89 in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies |
89 in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies |
90 (list_all (map (pair "x") Us, HOLogic.mk_Trueprop |
90 (list_all (map (pair "x") Us, HOLogic.mk_Trueprop |
91 (make_pred k rT U (app_bnds r i) |
91 (make_pred k rT U (app_bnds r i) |
105 val fTs = map fastype_of rec_fns; |
105 val fTs = map fastype_of rec_fns; |
106 val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T |
106 val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T |
107 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0))) |
107 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0))) |
108 (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); |
108 (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names); |
109 val r = if null is then Extraction.nullt else |
109 val r = if null is then Extraction.nullt else |
110 foldr1 HOLogic.mk_prod (mapfilter (fn (((((i, _), T), U), s), tname) => |
110 foldr1 HOLogic.mk_prod (List.mapPartial (fn (((((i, _), T), U), s), tname) => |
111 if i mem is then SOME |
111 if i mem is then SOME |
112 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) |
112 (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T)) |
113 else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); |
113 else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames)); |
114 val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") |
114 val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &") |
115 (map (fn ((((i, _), T), U), tname) => |
115 (map (fn ((((i, _), T), U), tname) => |
128 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => |
128 REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => |
129 REPEAT (etac allE i) THEN atac i)) 1)]); |
129 REPEAT (etac allE i) THEN atac i)) 1)]); |
130 |
130 |
131 val {path, ...} = Sign.rep_sg sg; |
131 val {path, ...} = Sign.rep_sg sg; |
132 val ind_name = Thm.name_of_thm induction; |
132 val ind_name = Thm.name_of_thm induction; |
133 val vs = map (fn i => nth_elem (i, pnames)) is; |
133 val vs = map (fn i => List.nth (pnames, i)) is; |
134 val (thy', thm') = thy |
134 val (thy', thm') = thy |
135 |> Theory.absolute_path |
135 |> Theory.absolute_path |
136 |> PureThy.store_thm |
136 |> PureThy.store_thm |
137 ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) |
137 ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), []) |
138 |>> Theory.add_path (NameSpace.pack (if_none path [])); |
138 |>> Theory.add_path (NameSpace.pack (getOpt (path,[]))); |
139 |
139 |
140 val ivs = Drule.vars_of_terms |
140 val ivs = Drule.vars_of_terms |
141 [Logic.varify (DatatypeProp.make_ind [descr] sorts)]; |
141 [Logic.varify (DatatypeProp.make_ind [descr] sorts)]; |
142 val rvs = Drule.vars_of_terms [prop_of thm']; |
142 val rvs = Drule.vars_of_terms [prop_of thm']; |
143 val ivs1 = map Var (filter_out (fn (_, T) => |
143 val ivs1 = map Var (filter_out (fn (_, T) => |
144 tname_of (body_type T) mem ["set", "bool"]) ivs); |
144 tname_of (body_type T) mem ["set", "bool"]) ivs); |
145 val ivs2 = map (fn (ixn, _) => Var (ixn, the (assoc (rvs, ixn)))) ivs; |
145 val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs; |
146 |
146 |
147 val prf = foldr forall_intr_prf (ivs2, |
147 val prf = Library.foldr forall_intr_prf (ivs2, |
148 foldr (fn ((f, p), prf) => |
148 Library.foldr (fn ((f, p), prf) => |
149 (case head_of (strip_abs_body f) of |
149 (case head_of (strip_abs_body f) of |
150 Free (s, T) => |
150 Free (s, T) => |
151 let val T' = Type.varifyT T |
151 let val T' = Type.varifyT T |
152 in Abst (s, SOME T', Proofterm.prf_abstract_over |
152 in Abst (s, SOME T', Proofterm.prf_abstract_over |
153 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf))) |
153 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf))) |
154 end |
154 end |
155 | _ => AbsP ("H", SOME p, prf))) |
155 | _ => AbsP ("H", SOME p, prf))) |
156 (rec_fns ~~ prems_of thm, Proofterm.proof_combP |
156 (rec_fns ~~ prems_of thm, Proofterm.proof_combP |
157 (prf_of thm', map PBound (length prems - 1 downto 0)))); |
157 (prf_of thm', map PBound (length prems - 1 downto 0)))); |
158 |
158 |
159 val r' = if null is then r else Logic.varify (foldr (uncurry lambda) |
159 val r' = if null is then r else Logic.varify (Library.foldr (uncurry lambda) |
160 (map Logic.unvarify ivs1 @ filter_out is_unit |
160 (map Logic.unvarify ivs1 @ filter_out is_unit |
161 (map (head_of o strip_abs_body) rec_fns), r)); |
161 (map (head_of o strip_abs_body) rec_fns), r)); |
162 |
162 |
163 in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; |
163 in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; |
164 |
164 |
182 HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ |
182 HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ |
183 list_comb (r, free_ts))))) |
183 list_comb (r, free_ts))))) |
184 end; |
184 end; |
185 |
185 |
186 val SOME (_, _, constrs) = assoc (descr, index); |
186 val SOME (_, _, constrs) = assoc (descr, index); |
187 val T = nth_elem (index, get_rec_types descr sorts); |
187 val T = List.nth (get_rec_types descr sorts, index); |
188 val (rs, prems) = split_list (map (make_casedist_prem T) constrs); |
188 val (rs, prems) = split_list (map (make_casedist_prem T) constrs); |
189 val r = Const (case_name, map fastype_of rs ---> T --> rT); |
189 val r = Const (case_name, map fastype_of rs ---> T --> rT); |
190 |
190 |
191 val y = Var (("y", 0), Type.varifyT T); |
191 val y = Var (("y", 0), Type.varifyT T); |
192 val y' = Free ("y", T); |
192 val y' = Free ("y", T); |
203 val {path, ...} = Sign.rep_sg sg; |
203 val {path, ...} = Sign.rep_sg sg; |
204 val exh_name = Thm.name_of_thm exhaustion; |
204 val exh_name = Thm.name_of_thm exhaustion; |
205 val (thy', thm') = thy |
205 val (thy', thm') = thy |
206 |> Theory.absolute_path |
206 |> Theory.absolute_path |
207 |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), []) |
207 |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), []) |
208 |>> Theory.add_path (NameSpace.pack (if_none path [])); |
208 |>> Theory.add_path (NameSpace.pack (getOpt (path,[]))); |
209 |
209 |
210 val P = Var (("P", 0), rT' --> HOLogic.boolT); |
210 val P = Var (("P", 0), rT' --> HOLogic.boolT); |
211 val prf = forall_intr_prf (y, forall_intr_prf (P, |
211 val prf = forall_intr_prf (y, forall_intr_prf (P, |
212 foldr (fn ((p, r), prf) => |
212 Library.foldr (fn ((p, r), prf) => |
213 forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), |
213 forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), |
214 prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm', |
214 prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm', |
215 map PBound (length prems - 1 downto 0))))); |
215 map PBound (length prems - 1 downto 0))))); |
216 val r' = Logic.varify (Abs ("y", Type.varifyT T, |
216 val r' = Logic.varify (Abs ("y", Type.varifyT T, |
217 list_abs (map dest_Free rs, list_comb (r, |
217 list_abs (map dest_Free rs, list_comb (r, |