equal
deleted
inserted
replaced
70 |
70 |
71 val datatype_ss = @{simpset}; |
71 val datatype_ss = @{simpset}; |
72 |
72 |
73 fun proc sg ss old = |
73 fun proc sg ss old = |
74 let val _ = if !trace then writeln ("data_free: OLD = " ^ |
74 let val _ = if !trace then writeln ("data_free: OLD = " ^ |
75 string_of_cterm (cterm_of sg old)) |
75 Display.string_of_cterm (cterm_of sg old)) |
76 else () |
76 else () |
77 val (lhs,rhs) = FOLogic.dest_eq old |
77 val (lhs,rhs) = FOLogic.dest_eq old |
78 val (lhead, largs) = strip_comb lhs |
78 val (lhead, largs) = strip_comb lhs |
79 and (rhead, rargs) = strip_comb rhs |
79 and (rhead, rargs) = strip_comb rhs |
80 val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; |
80 val lname = #1 (dest_Const lhead) handle TERM _ => raise Match; |
88 andalso not (null (#free_iffs lcon_info)) then |
88 andalso not (null (#free_iffs lcon_info)) then |
89 if lname = rname then mk_new (largs, rargs) |
89 if lname = rname then mk_new (largs, rargs) |
90 else Const("False",FOLogic.oT) |
90 else Const("False",FOLogic.oT) |
91 else raise Match |
91 else raise Match |
92 val _ = if !trace then |
92 val _ = if !trace then |
93 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new)) |
93 writeln ("NEW = " ^ Display.string_of_cterm (Thm.cterm_of sg new)) |
94 else (); |
94 else (); |
95 val goal = Logic.mk_equals (old, new) |
95 val goal = Logic.mk_equals (old, new) |
96 val thm = Goal.prove (Simplifier.the_context ss) [] [] goal |
96 val thm = Goal.prove (Simplifier.the_context ss) [] [] goal |
97 (fn _ => rtac iff_reflection 1 THEN |
97 (fn _ => rtac iff_reflection 1 THEN |
98 simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) |
98 simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1) |