blob: b88a8fcdd7ef0976b35a01516475183826a944e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
theory scratch
imports HoTT
begin
abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)"
schematic_goal "?a : (pred`0) =\<^sub>\<nat> 0"
apply (subst comp)
apply (rule Nat_form)
prefer 4 apply (subst comp)
apply (rule Nat_form)
apply assumption
apply (rule Nat_intro1)
apply (rule Equal_intro)
apply (rule Nat_intro1)
prefer 2 apply (rule Nat_elim)
apply (rule Nat_form)
apply assumption
apply (rule Nat_intro1)
apply assumption
apply (rule Nat_form)
done
schematic_goal "?a : \<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n"
apply (rule Prod_intro)
apply (rule Nat_form)
apply (subst comp)
apply (rule Nat_form)
prefer 2 apply (rule Nat_elim)
apply (rule Nat_form)
apply assumption
apply (rule Nat_intro1)
apply assumption
apply (rule Nat_form)
apply (rule Nat_intro2, assumption)
apply (rule Equal_form)
apply (rule Nat_form)
apply (rule Nat_elim)
apply (rule Nat_form)
apply assumption
apply (rule Nat_rules)+
apply assumption+
apply (subst comp)
apply (rule Nat_form)
prefer 2 apply (rule Nat_elim)
defer
apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+
apply (subst Nat_comps)
apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+
apply (rule Equal_intro)
apply assumption
apply (rule Nat_form)
done
schematic_goal "?a : \<Sum>p:\<nat>\<rightarrow>\<nat>. \<Prod>n:\<nat>. (p`(succ n)) =\<^sub>\<nat> n"
apply (rule Sum_intro)
apply (rule Prod_form)
apply (rule Nat_form)+
apply (rule Prod_form)
apply (rule Nat_form)
apply (rule Equal_form)
apply (rule Nat_form)
apply (rule Prod_elim)
apply assumption
apply (elim Nat_intro2)
apply assumption
prefer 2 apply (rule Prod_intro)
apply (rule Nat_form)
prefer 3 apply (rule Prod_intro)
apply (rule Nat_form)+
prefer 3 apply (rule Nat_elim)
back
oops
(* Now try to derive pred directly *)
schematic_goal "?a : \<Sum>pred:?A . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)"
(* At some point need to perform induction *)
apply (rule Sum_intro)
defer
apply (rule Sum_form)
apply (rule Equal_form)
apply (rule Nat_form)
apply (rule Prod_elim)
defer
apply (rule Nat_intro1)+
prefer 5 apply assumption
prefer 4 apply (rule Prod_form)
apply (rule Nat_form)+
apply (rule Prod_form)
apply (rule Nat_form)
apply (rule Equal_form)
apply (rule Nat_form)
apply (rule Prod_elim)
apply assumption
apply (rule Nat_intro2)
apply assumption+
(* Now begins the hard part *)
prefer 2 apply (rule Sum_rules)
prefer 2 apply (rule Prod_rules)
end
|
