27 |
25 |
28 fun message s = if !quiet_mode then () else writeln s; |
26 fun message s = if !quiet_mode then () else writeln s; |
29 fun trace s = if !trace_domain then tracing s else (); |
27 fun trace s = if !trace_domain then tracing s else (); |
30 |
28 |
31 open HOLCF_Library; |
29 open HOLCF_Library; |
32 infixr 0 ===>; |
|
33 infix 0 == ; |
|
34 infix 1 ===; |
|
35 infix 9 ` ; |
|
36 |
|
37 (* ----- general proof facilities ------------------------------------------- *) |
|
38 |
|
39 local |
|
40 |
|
41 fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) |
|
42 | map_typ f _ (TFree (x, S)) = TFree (x, map f S) |
|
43 | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); |
|
44 |
|
45 fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) |
|
46 | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) |
|
47 | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) |
|
48 | map_term _ _ _ (t as Bound _) = t |
|
49 | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) |
|
50 | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; |
|
51 |
|
52 in |
|
53 |
|
54 fun intern_term thy = |
|
55 map_term (Sign.intern_class thy) (Sign.intern_type thy) (Sign.intern_const thy); |
|
56 |
|
57 end; |
|
58 |
|
59 fun legacy_infer_term thy t = |
|
60 let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init_global thy) |
|
61 in singleton (Syntax.check_terms ctxt) (intern_term thy t) end; |
|
62 |
|
63 fun pg'' thy defs t tacs = |
|
64 let |
|
65 val t' = legacy_infer_term thy t; |
|
66 val asms = Logic.strip_imp_prems t'; |
|
67 val prop = Logic.strip_imp_concl t'; |
|
68 fun tac {prems, context} = |
|
69 rewrite_goals_tac defs THEN |
|
70 EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) |
|
71 in Goal.prove_global thy [] asms prop tac end; |
|
72 |
|
73 fun pg' thy defs t tacsf = |
|
74 let |
|
75 fun tacs {prems, context} = |
|
76 if null prems then tacsf context |
|
77 else cut_facts_tac prems 1 :: tacsf context; |
|
78 in pg'' thy defs t tacs end; |
|
79 |
30 |
80 (******************************************************************************) |
31 (******************************************************************************) |
81 (***************************** proofs about take ******************************) |
32 (***************************** proofs about take ******************************) |
82 (******************************************************************************) |
33 (******************************************************************************) |
83 |
34 |
133 in |
84 in |
134 fold_map prove_take_apps |
85 fold_map prove_take_apps |
135 (dbinds ~~ take_consts ~~ constr_infos) thy |
86 (dbinds ~~ take_consts ~~ constr_infos) thy |
136 end; |
87 end; |
137 |
88 |
138 (* ----- general proofs ----------------------------------------------------- *) |
89 (******************************************************************************) |
139 |
90 (****************************** induction rules *******************************) |
140 val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} |
91 (******************************************************************************) |
141 |
92 |
142 val case_UU_allI = |
93 val case_UU_allI = |
143 @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; |
94 @{lemma "(!!x. x ~= UU ==> P x) ==> P UU ==> ALL x. P x" by metis}; |
144 |
|
145 (******************************************************************************) |
|
146 (****************************** induction rules *******************************) |
|
147 (******************************************************************************) |
|
148 |
95 |
149 fun prove_induction |
96 fun prove_induction |
150 (comp_dbind : binding) |
97 (comp_dbind : binding) |
151 (constr_infos : Domain_Constructors.constr_info list) |
98 (constr_infos : Domain_Constructors.constr_info list) |
152 (take_info : Domain_Take_Proofs.take_induct_info) |
99 (take_info : Domain_Take_Proofs.take_induct_info) |