equal
deleted
inserted
replaced
17 axioms |
17 axioms |
18 F_strict: "F(UU) = UU" |
18 F_strict: "F(UU) = UU" |
19 K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" |
19 K: "K = (%h x y. P(x) => y | F(h(G(x),y)))" |
20 H: "H = FIX(K)" |
20 H: "H = FIX(K)" |
21 |
21 |
22 ML {* use_legacy_bindings (the_context ()) *} |
22 declare F_strict [simp] K [simp] |
|
23 |
|
24 lemma example: "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))" |
|
25 apply (simplesubst H) |
|
26 apply (tactic {* induct_tac "K:: ('a=>'b=>'b) => ('a=>'b=>'b)" 1 *}) |
|
27 apply (simp (no_asm)) |
|
28 apply (simp (no_asm_simp) split: COND_cases_iff) |
|
29 done |
23 |
30 |
24 end |
31 end |