equal
deleted
inserted
replaced
22 |
22 |
23 structure FundefPackage : FUNDEF_PACKAGE = |
23 structure FundefPackage : FUNDEF_PACKAGE = |
24 struct |
24 struct |
25 |
25 |
26 open FundefCommon |
26 open FundefCommon |
27 |
|
28 val True_implies = thm "True_implies" |
|
29 |
27 |
30 |
28 |
31 fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy = |
29 fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy = |
32 let |
30 let |
33 val psimpss = Library.unflat (map snd spec_part) psimps |
31 val psimpss = Library.unflat (map snd spec_part) psimps |
110 val totality = hd (hd thmss) |
108 val totality = hd (hd thmss) |
111 |
109 |
112 val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec) |
110 val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec) |
113 = the (get_fundef_data name thy) |
111 = the (get_fundef_data name thy) |
114 |
112 |
115 val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies]) |
113 val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals]) |
116 |
114 |
117 val tsimps = map (map remove_domain_condition) psimps |
115 val tsimps = map (map remove_domain_condition) psimps |
118 val tinduct = map remove_domain_condition simple_pinducts |
116 val tinduct = map remove_domain_condition simple_pinducts |
119 |
117 |
120 val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps) |
118 val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) (flat tsimps) |