39 fun mutual_induct_Pnames n = |
39 fun mutual_induct_Pnames n = |
40 if n < 5 then fst (chop n ["P","Q","R","S"]) |
40 if n < 5 then fst (chop n ["P","Q","R","S"]) |
41 else map (fn i => "P" ^ string_of_int i) (1 upto n) |
41 else map (fn i => "P" ^ string_of_int i) (1 upto n) |
42 |
42 |
43 |
43 |
44 fun check_head fs t = |
|
45 if (case t of |
|
46 (Free (n, _)) => n mem (map fst fs) |
|
47 | _ => false) |
|
48 then dest_Free t |
|
49 else raise ERROR "Head symbol of every left hand side must be the new function." (* FIXME: Output the equation here *) |
|
50 |
|
51 |
|
52 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) |
44 fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) |
53 | open_all_all t = ([], t) |
45 | open_all_all t = ([], t) |
54 |
46 |
55 |
47 |
56 |
48 |
57 (* Builds a curried clause description in abstracted form *) |
49 (* Builds a curried clause description in abstracted form *) |
58 fun split_def fs geq arities = |
50 fun split_def ctxt fnames geq arities = |
59 let |
51 let |
|
52 fun input_error msg = error (cat_lines [msg, ProofContext.string_of_term ctxt geq]) |
|
53 |
60 val (qs, imp) = open_all_all geq |
54 val (qs, imp) = open_all_all geq |
61 |
55 |
62 val gs = Logic.strip_imp_prems imp |
56 val gs = Logic.strip_imp_prems imp |
63 val eq = Logic.strip_imp_concl imp |
57 val eq = Logic.strip_imp_concl imp |
64 |
58 |
65 val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
59 val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq) |
66 val (fc, args) = strip_comb f_args |
60 val (head, args) = strip_comb f_args |
67 val f as (fname, _) = check_head fs fc |
61 |
68 |
62 val invalid_head_msg = "Head symbol of left hand side must be " ^ plural "" "one out of " fnames ^ commas_quote fnames |
|
63 val fname = fst (dest_Free head) |
|
64 handle TERM _ => input_error invalid_head_msg |
|
65 |
|
66 val _ = if fname mem fnames then () |
|
67 else input_error invalid_head_msg |
|
68 |
69 fun add_bvs t is = add_loose_bnos (t, 0, is) |
69 fun add_bvs t is = add_loose_bnos (t, 0, is) |
70 val rhs_only = (add_bvs rhs [] \\ fold add_bvs args []) |
70 val rvs = (add_bvs rhs [] \\ fold add_bvs args []) |
71 |> print |
71 |> map (fst o nth (rev qs)) |
72 |> map (fst o nth (rev qs)) |
72 |
73 val _ = if null rhs_only then () |
73 val _ = if null rvs then () |
74 else raise ERROR "Variables occur on right hand side only." (* FIXME: Output vars *) |
74 else input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs |
|
75 ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:") |
|
76 |
|
77 val _ = (fold o fold_aterms) |
|
78 (fn Free (n, _) => if n mem fnames |
|
79 then input_error "Recursive Calls not allowed in premises:" |
|
80 else I |
|
81 | _ => I) gs () |
75 |
82 |
76 val k = length args |
83 val k = length args |
77 |
84 |
78 val arities' = case Symtab.lookup arities fname of |
85 val arities' = case Symtab.lookup arities fname of |
79 NONE => Symtab.update (fname, k) arities |
86 NONE => Symtab.update (fname, k) arities |
80 | SOME i => if (i <> k) |
87 | SOME i => if (i <> k) |
81 then raise ERROR ("Function " ^ fname ^ " has different numbers of arguments in different equations") |
88 then input_error ("Function " ^ quote fname ^ " has different numbers of arguments in different equations") |
82 else arities |
89 else arities |
83 in |
90 in |
84 ((fname, qs, gs, args, rhs), arities') |
91 ((fname, qs, gs, args, rhs), arities') |
85 end |
92 end |
86 |
93 |
99 |
106 |
100 |
107 |
101 fun analyze_eqs ctxt fs eqs = |
108 fun analyze_eqs ctxt fs eqs = |
102 let |
109 let |
103 val fnames = map fst fs |
110 val fnames = map fst fs |
104 val (fqgars, arities) = fold_map (split_def fs) eqs Symtab.empty |
111 val (fqgars, arities) = fold_map (split_def ctxt fnames) eqs Symtab.empty |
105 |
|
106 val check_rcs = exists_subterm (fn Free (n, _) => if n mem fnames |
|
107 then raise ERROR "Recursive Calls not allowed in premises." else false |
|
108 | _ => false) |
|
109 |
|
110 val _ = forall (fn (_, _, gs, _, _) => forall check_rcs gs) fqgars |
|
111 |
112 |
112 fun curried_types (fname, fT) = |
113 fun curried_types (fname, fT) = |
113 let |
114 let |
114 val k = the_default 1 (Symtab.lookup arities fname) |
115 val k = the_default 1 (Symtab.lookup arities fname) |
115 val (caTs, uaTs) = chop k (binder_types fT) |
116 val (caTs, uaTs) = chop k (binder_types fT) |