Yutaka Ng
Yutaka Ng
Done for now in 4e50b0c8add2e1138bc4ccfd3717a073357671fa. But we can make it more stable using `SeLFiE`.
An example would be line 193 in `Applicative_Lifting/Idiomatic_Terms.thy`.
Replace free variables with schematic variables(?)
Probably, two variables should be separated when they appear in different meta-conjuncts.
It is often better to apply mathematical induction on variables that appear in all (or multiple) meta-conjuncts in the goal, especially when using "rule: *.inducts". --> a mutually recursive function...
I think PSL does not even support "rule: *.inducts".
The file `Rep_Fin_Groups.thy` has nice examples of how these are used. (about 130 proofs by induction) - [x] `list_all2_induct` - [x] `rev_nonempty_induct` -> `as ≠ [ ] ⟹... ` -...
- [ ] `dec_induct` in `Nat.thy` -> Not used often. 6 cases are found in `Architectural_Design_Patterns.RF_LTL.thy`. `xs ≥ ys` -> `induct xs`. `xs ≤ ys` -> `induct ys` but only...
Maybe detecting function types would be good when proof goals have variables that are functions.
Producing this structural proof script is too much work for little gain. ``` lemma "itrev xs [] = rev xs" (* apply (subgoal_tac "⋀Nil. itrev xs Nil = rev xs...