98 (Free (Long_Name.base_name name ^ "P", T)) |
100 (Free (Long_Name.base_name name ^ "P", T)) |
99 else |
101 else |
100 (Free (Long_Name.base_name name ^ "P", pred_type T)) |
102 (Free (Long_Name.base_name name ^ "P", pred_type T)) |
101 end |
103 end |
102 |
104 |
103 fun mk_param lookup_pred (t as Free (v, _)) = lookup_pred t |
105 fun mk_param thy lookup_pred (t as Free (v, _)) = lookup_pred t |
104 | mk_param lookup_pred t = |
106 | mk_param thy lookup_pred t = |
105 let |
107 let |
106 val (vs, body) = strip_abs t |
108 val _ = tracing ("called param with " ^ (Syntax.string_of_term_global thy t)) |
107 val names = Term.add_free_names body [] |
109 in if Predicate_Compile_Aux.is_predT (fastype_of t) then |
108 val vs_names = Name.variant_list names (map fst vs) |
110 t |
109 val vs' = map2 (curry Free) vs_names (map snd vs) |
111 else |
110 val body' = subst_bounds (rev vs', body) |
112 let |
111 val (f, args) = strip_comb body' |
113 val (vs, body) = strip_abs t |
112 val resname = Name.variant (vs_names @ names) "res" |
114 val names = Term.add_free_names body [] |
113 val resvar = Free (resname, body_type (fastype_of body')) |
115 val vs_names = Name.variant_list names (map fst vs) |
114 val P = lookup_pred f |
116 val vs' = map2 (curry Free) vs_names (map snd vs) |
115 val pred_body = list_comb (P, args @ [resvar]) |
117 val body' = subst_bounds (rev vs', body) |
116 val param = fold_rev lambda (vs' @ [resvar]) pred_body |
118 val (f, args) = strip_comb body' |
117 in param end; |
119 val resname = Name.variant (vs_names @ names) "res" |
118 |
120 val resvar = Free (resname, body_type (fastype_of body')) |
119 |
121 (*val P = case try lookup_pred f of SOME P => P | NONE => error "mk_param" |
|
122 val pred_body = list_comb (P, args @ [resvar]) |
|
123 *) |
|
124 val pred_body = HOLogic.mk_eq (body', resvar) |
|
125 val param = fold_rev lambda (vs' @ [resvar]) pred_body |
|
126 in param end |
|
127 end |
120 (* creates the list of premises for every intro rule *) |
128 (* creates the list of premises for every intro rule *) |
121 (* theory -> term -> (string list, term list list) *) |
129 (* theory -> term -> (string list, term list list) *) |
122 |
130 |
123 fun dest_code_eqn eqn = let |
131 fun dest_code_eqn eqn = let |
124 val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn)) |
132 val (lhs, rhs) = Logic.dest_equals (Logic.unvarify (Thm.prop_of eqn)) |