equal
deleted
inserted
replaced
16 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
16 lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)" |
17 apply (induct_tac ts rule: rev_induct) |
17 apply (induct_tac ts rule: rev_induct) |
18 apply auto |
18 apply auto |
19 done |
19 done |
20 |
20 |
21 lemma Var_eq_apps_conv [rule_format, iff]: |
21 lemma Var_eq_apps_conv [iff]: |
22 "\<forall>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" |
22 "\<And>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])" |
23 apply (induct_tac ss) |
23 apply (induct ss) |
24 apply auto |
24 apply auto |
25 done |
25 done |
26 |
26 |
27 lemma Var_apps_eq_Var_apps_conv [rule_format, iff]: |
27 lemma Var_apps_eq_Var_apps_conv [iff]: |
28 "\<forall>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" |
28 "\<And>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)" |
29 apply (induct_tac rs rule: rev_induct) |
29 apply (induct rs rule: rev_induct) |
30 apply simp |
30 apply simp |
31 apply blast |
31 apply blast |
32 apply (rule allI) |
|
33 apply (induct_tac ss rule: rev_induct) |
32 apply (induct_tac ss rule: rev_induct) |
34 apply auto |
33 apply auto |
35 done |
34 done |
36 |
35 |
37 lemma App_eq_foldl_conv: |
36 lemma App_eq_foldl_conv: |
52 apply (induct_tac ss rule: rev_induct) |
51 apply (induct_tac ss rule: rev_induct) |
53 apply auto |
52 apply auto |
54 done |
53 done |
55 |
54 |
56 lemma Abs_apps_eq_Abs_apps_conv [iff]: |
55 lemma Abs_apps_eq_Abs_apps_conv [iff]: |
57 "\<forall>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)" |
56 "\<And>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)" |
58 apply (induct_tac rs rule: rev_induct) |
57 apply (induct rs rule: rev_induct) |
59 apply simp |
58 apply simp |
60 apply blast |
59 apply blast |
61 apply (rule allI) |
|
62 apply (induct_tac ss rule: rev_induct) |
60 apply (induct_tac ss rule: rev_induct) |
63 apply auto |
61 apply auto |
64 done |
62 done |
65 |
63 |
66 lemma Abs_App_neq_Var_apps [iff]: |
64 lemma Abs_App_neq_Var_apps [iff]: |
67 "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss" |
65 "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss" |
68 apply (induct_tac ss rule: rev_induct) |
66 apply (induct_tac ss rule: rev_induct) |
69 apply auto |
67 apply auto |
70 done |
68 done |
71 |
69 |
72 lemma Var_apps_neq_Abs_apps [rule_format, iff]: |
70 lemma Var_apps_neq_Abs_apps [iff]: |
73 "\<forall>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss" |
71 "\<And>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss" |
74 apply (induct_tac ss rule: rev_induct) |
72 apply (induct ss rule: rev_induct) |
75 apply simp |
73 apply simp |
76 apply (rule allI) |
|
77 apply (induct_tac ts rule: rev_induct) |
74 apply (induct_tac ts rule: rev_induct) |
78 apply auto |
75 apply auto |
79 done |
76 done |
80 |
77 |
81 lemma ex_head_tail: |
78 lemma ex_head_tail: |