17 and trm = |
15 and trm = |
18 Const "ident" |
16 Const "ident" |
19 | Var "name" |
17 | Var "name" |
20 | App "trm" "trm" |
18 | App "trm" "trm" |
21 | Lam "ty" n::"name" t::"trm" bind n in t |
19 | Lam "ty" n::"name" t::"trm" bind n in t |
22 |
|
23 lemma supports: |
|
24 "{} supports Type" |
|
25 "(supp (atom i)) supports (TConst i)" |
|
26 "(supp A \<union> supp M) supports (TApp A M)" |
|
27 "(supp (atom i)) supports (Const i)" |
|
28 "(supp (atom x)) supports (Var x)" |
|
29 "(supp M \<union> supp N) supports (App M N)" |
|
30 "(supp ty \<union> supp (atom na) \<union> supp ki) supports (KPi ty na ki)" |
|
31 "(supp ty \<union> supp (atom na) \<union> supp ty2) supports (TPi ty na ty2)" |
|
32 "(supp ty \<union> supp (atom na) \<union> supp trm) supports (Lam ty na trm)" |
|
33 apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh kind_ty_trm_perm) |
|
34 apply(rule_tac [!] allI)+ |
|
35 apply(rule_tac [!] impI) |
|
36 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
|
37 apply(simp_all add: fresh_atom) |
|
38 done |
|
39 |
|
40 lemma kind_ty_trm_fs: |
|
41 "finite (supp (x\<Colon>kind)) \<and> finite (supp (y\<Colon>ty)) \<and> finite (supp (z\<Colon>trm))" |
|
42 apply(induct rule: kind_ty_trm_induct) |
|
43 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
|
44 apply(simp_all add: supp_atom) |
|
45 done |
|
46 |
|
47 instance kind and ty and trm :: fs |
|
48 apply(default) |
|
49 apply(simp_all only: kind_ty_trm_fs) |
|
50 done |
|
51 |
20 |
52 lemma ex_out: |
21 lemma ex_out: |
53 "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))" |
22 "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))" |
54 "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))" |
23 "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))" |
55 "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |
24 "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))" |